CoordinateStationaryPaths.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Independent coordinate sampling for nonnegative path families

This bridge normalizes coordinate volume once and extends a family from nonnegative scales. It separates finite-measure sampling from the Lie coordinate constructions that supply the paths.

theorem OAI.PolycyclicRecognition.coordinate_stationary_paths line 29

Source documentation

Continuous coding on a common coordinate ball supplies a good endpoint set of at least half its volume at every sufficiently large scale.

theorem coordinate_stationary_paths {n : ℕ} {ε C K : ℝ} (hε : 0 < ε) (hC : 0 ≤ C) (hK : 0 ≤ K)
    (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
    (π l : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) (hl : Continuous fun g => (l g).toAdd)
    (hLip : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y)
    (hsub : ∀ η : ℝ, 0 < η → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
      ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd‖ ≤ η * dist 1 g + B)
    (E : Set W)
    (endpoint : ℝ → ball (0 : Fin n → ℝ) ε → G)
    (hcode : ∀ r : ℝ, 0 ≤ r → ∃ γ : ∀ y, Path (1 : G) (endpoint r y),
      (∀ t, Continuous (fun y => γ y t)) ∧
      (∀ y, PathMetricBound (γ y) (C * r) (C * (1 + Real.log (2 + r)))) ∧
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeightL2, OAI.PolycyclicRecognition.PathMetricBound