OAI/GroupTheory/PolycyclicRecognition/Algebra/UniformOccupationAverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.integral_tendsto_zero_of_uniformly_zero line 16

   Source documentation

   Uniform convergence to zero passes to every probability average. The norm estimate also covers any nonintegrable early terms.

   theorem integral_tendsto_zero_of_uniformly_zero
       {ι Z V : Type*} [MeasurableSpace Z] [NormedAddCommGroup V] [NormedSpace ℝ V]
       (μ : Measure Z) [IsProbabilityMeasure μ] {l : Filter ι}
       (f : ι → Z → V) (hf : TendstoUniformly f (fun _ => 0) l) :
       Tendsto (fun i => ∫ z, f i z ∂μ) l (𝓝 0) := by
   …

2. theorem OAI.PolycyclicRecognition.integral_tendsto_zero_of_uniformly_supported_zero line 32

   Source documentation

   Uniform control is needed only on a set carrying the sampling measure. This is the form used for a compactly supported chart density.

   theorem integral_tendsto_zero_of_uniformly_supported_zero
       {ι Z V : Type*} [MeasurableSpace Z] [NormedAddCommGroup V] [NormedSpace ℝ V]
       (μ : Measure Z) [IsProbabilityMeasure μ] {l : Filter ι}
       (K : Set Z) (hK : ∀ᵐ z ∂μ, z ∈ K) (f : ι → Z → V)
       (hf : TendstoUniformly (fun i (z : K) => f i z) (fun _ => 0) l) :
       Tendsto (fun i => ∫ z, f i z ∂μ) l (𝓝 0) := by
   …

3. theorem OAI.PolycyclicRecognition.averaged_model_cell_error_tendsto_zero line 49

   Source documentation

   The normalized cell average remains asymptotically invariant after any independent probability sampling of the chart parameter.

   theorem averaged_model_cell_error_tendsto_zero
       {E G L ι Z : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       [FiniteDimensional ℝ E] [TopologicalSpace G] [ChartedSpace E G] [Group G]
       [LieGroup (𝓘(ℝ, E)) ⊤ G] [T2Space G] [SimplyConnectedSpace G]
       [MeasurableSpace G] [BorelSpace G] [LieRing L] [LieAlgebra ℝ L]
       [MeasurableSpace Z] (ν : Measure Z) [IsProbabilityMeasure ν]
       (haar : NilpotentExponentialHaarInput E G)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
       (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G))
       {n c : ℕ} (b : ι → Basis (Fin n) ℝ L)
       (a : DynkinCoefficients c 2)
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.DynkinCoefficients