OAI/GroupTheory/PolycyclicRecognition/Algebra/DensityOccupationError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.norm_integral_density_sub_le line 13

   Source documentation

   The total variation estimate needed after changing sampling density.

   theorem norm_integral_density_sub_le
       {X : Type*} [MeasurableSpace X] (μ : Measure X)
       (ρ σ f : X → ℝ) (hρ : Integrable ρ μ) (hσ : Integrable σ μ)
       (hf : AEStronglyMeasurable f μ) {C : ℝ} (_hC : 0 ≤ C)
       (hb : ∀ x, ‖f x‖ ≤ C) :
       ‖(∫ x, ρ x * f x ∂μ) - ∫ x, σ x * f x ∂μ‖ ≤
         C * ∫ x, |ρ x - σ x| ∂μ := by
   …

2. theorem OAI.PolycyclicRecognition.density_occupation_error_tendsto_zero line 33

   Source documentation

   Small measure-preserving coordinate translations change every bounded scale-dependent observable by a vanishing amount under a fixed density.

   theorem density_occupation_error_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]
       (e : ι → X ≃ᵐ X) (he : ∀ i, MeasurePreserving (e i) μ μ)
       (hlim : ∀ x, Tendsto (fun i => (e i).symm x) l (𝓝 x))
       (f : ι → X → ℝ) (hf : ∀ i, AEStronglyMeasurable (f i) μ)
       {C : ℝ} (hC : 0 ≤ C) (hb : ∀ i x, ‖f i x‖ ≤ C) :
       Tendsto (fun i => (∫ x, ρ x * f i (e i x) ∂μ) - ∫ x, ρ x * f i x ∂μ)
         l (𝓝 0) := by
   …