OAI/GroupTheory/PolycyclicRecognition/Algebra/OccupationMicrosteps.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.integral_comp_le_of_map_le line 20

   Source documentation

   Domination of a pushed sampling law controls every nonnegative continuous observable on the compact section.

   theorem integral_comp_le_of_map_le
       {X : Type*} [TopologicalSpace X] [CompactSpace X]
       [MeasurableSpace X] [BorelSpace X]
       (σ μ : Measure X) [IsFiniteMeasure σ] [IsFiniteMeasure μ]
       (T : X → X) (hT : Continuous T) {c : ℝ≥0}
       (hdom : Measure.map T σ ≤ c • μ)
       (f : X → ℝ) (hf : Continuous f) (hpos : ∀ x, 0 ≤ f x) :
       ∫ x, f (T x) ∂σ ≤ (c : ℝ) * ∫ x, f x ∂μ := by
   …

2. theorem OAI.PolycyclicRecognition.integral_normalized_microsteps_le line 43

   Source documentation

   The mean convex error of a long increment is bounded by one fixed-length occupation observable and the explicit final-step error.

   theorem integral_normalized_microsteps_le
       (σ μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure σ] [IsProbabilityMeasure μ]
       (π : G →* Multiplicative W) (hπ : LipschitzWith K (fun g => (π g).toAdd))
       (g h : G) (n : ℕ) {c : ℝ≥0}
       (hdom : ∀ j : Fin n, Measure.map (fun p : NormalizedPair G Λ => (g ^ (j : ℕ))⁻¹ • p) σ ≤ c • μ)
       {L t D : ℝ} (hL : 0 < L) (ht : 0 < t) (hD : 0 ≤ D)
       (hn : (n : ℝ) * L ≤ t) (hn' : t ≤ ((n : ℝ) + 1) * L)
       (hrem : dist 1 h ≤ D * L)
       {S : Set W} (hS : IsCompact S) {w₀ : W} (hw₀ : w₀ ∈ S) :
       ∫ p, infDist (t⁻¹ • pairHeight π (g ^ n * h) p) (convexHull ℝ S) ∂σ ≤
         (c : ℝ) * (∫ p, infDist (L⁻¹ • pairHeight π g p) S ∂μ) +
           (L / t) * ((K : ℝ) * Λ * D + ‖w₀‖) := by
   …

   Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight