DensityTranslationLimits.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Small measure-preserving moves of an integrable density

The minimum of the moved density and the original one is dominated by the original density. Thus dominated convergence gives L1 convergence without requiring a common compact support for all moved densities.

theorem OAI.PolycyclicRecognition.density_translation_l1_tendsto_zero line 21

Source documentation

A nonnegative continuous integrable density changes by a vanishing L1 amount under measure-preserving maps tending pointwise to the identity.

theorem density_translation_l1_tendsto_zero
    {X ι : Type*} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]
    (μ : Measure X) (ρ : X → ℝ) (hc : Continuous ρ) (hi : Integrable ρ μ)
    (hp : ∀ x, 0 ≤ ρ x)
    {l : Filter ι} [l.IsCountablyGenerated]
    (T : ι → X → X) (hT : ∀ i, MeasurePreserving (T i) μ μ)
    (hlim : ∀ x, Tendsto (fun i => T i x) l (𝓝 x)) :
    Tendsto (fun i => ∫ x, |ρ (T i x) - ρ x| ∂μ) l (𝓝 0) := by
…