StationaryPathSampling.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Stationary sampling along controlled paths

A fixed finite mesh selects one normalized pair good for most independently sampled endpoints. The coarse metric bound extends that mesh estimate to the whole image path and retains the logarithmic error explicitly.

theorem OAI.PolycyclicRecognition.eventually_exists_pair_good_on_paths line 31

Source documentation

The finite-mesh bad set has mass less than one half; outside it every point of the image path has controlled height. No supremum-in-L² is used.

theorem eventually_exists_pair_good_on_paths
    (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
    (ν : Measure Y) [IsProbabilityMeasure ν]
    (π l : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) (hl : Continuous fun g => (l g).toAdd)
    (hsub : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
      ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd‖ ≤ ε * dist 1 g + B)
    {K C δ η : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) (hδ : 0 < δ) (hη : 0 < η)
    (hLip : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y)
    (endpoint : ℝ → Y → G)
    (γ : ∀ r y, Path (1 : G) (endpoint r y))
    (hγ : ∀ r t, Measurable (fun y => γ r y t))
…

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