Dominated convergence away from one point

This file packages the common application of dominated convergence in which a continuously parameterized family is controlled and converges pointwise away from one exceptional point. When singletons have measure zero, the pointwise hypotheses supply the almost-everywhere hypotheses of the dominated convergence theorem.

Main declarations

• TauCeti.tendsto_integral_mul_of_dominated_away: dominated convergence for a family multiplied by a fixed continuous weight, with domination and convergence away from one point.

theorem TauCeti.tendsto_integral_mul_of_dominated_away {α : Type u_1} {ι : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ] {l : Filter ι} [l.IsCountablyGenerated] (x₀ : α) {K : ι → α → ℝ} {K₀ w : α → ℝ} (hw : Continuous w) (hK : ∀ᶠ (i : ι) in l, Continuous (K i)) (hint : MeasureTheory.Integrable (fun (x : α) => K₀ x * w x) μ) (hle : ∀ᶠ (i : ι) in l, ∀ (x : α), x ≠ x₀ → |K i x| ≤ |K₀ x|) (hlim : ∀ (x : α), x ≠ x₀ → Filter.Tendsto (fun (i : ι) => K i x) l (nhds (K₀ x))) : Filter.Tendsto (fun (i : ι) => ∫ (x : α), K i x * w x ∂μ) l (nhds (∫ (x : α), K₀ x * w x ∂μ))

Dominated convergence away from one point. Suppose K i is eventually continuous, w is continuous, and K i is eventually dominated by K₀ and converges to it away from a point x₀. If K₀ * w is integrable and singletons are null, then the integrals of K i * w converge to the integral of K₀ * w.

The exceptional point is useful for regularizations of singular kernels. The statement is for an arbitrary countably generated filter and an arbitrary measured topological space.