theorem ae_tendsto_zero_of_distribution_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ} {F : ℕ → α → ℂ} (h : ∀ δ > 0, ∀ ε > 0, ∃ (N₀ : ℕ), MeasureTheory.distribution (fun (x : α) => ⨆ (N : ℕ), ⨆ (_ : N > N₀), ‖f x - F N x‖ₑ) (↑δ) μ ≤ ↑ε) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (x_1 : ℕ) => F x_1 x) Filter.atTop (nhds (f x))

theorem Function.Periodic.ae_of_ae_restrict {T : ℝ} (hT : 0 < T) {a : ℝ} {P : ℝ → Prop} (hP : Periodic P T) (h : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ico a (a + T)), P x) : ∀ᵐ (x : ℝ), P x