StationarySampling.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed-mesh sampling at large scale

A sublinear L² estimate on growing balls selects one actual pair with small errors for most endpoints of a fixed finite family of sampled paths. The finite mesh is chosen before the scale tends to infinity.

theorem OAI.PolycyclicRecognition.exists_mesh_tolerance line 21
Source documentation
The finite-union Chebyshev bound can be made smaller than one half by choosing a single positive L² tolerance, independently of scale.
```
theorem exists_mesh_tolerance (M : ℕ) {η : ℝ} (hη : 0 < η) :
    ∃ δ : ℝ, 0 < δ ∧ (M : ℝ≥0∞) *
      ((ENNReal.ofReal η)⁻¹ ^ 2 * ENNReal.ofReal δ ^ 2) < 1 / 2 := by
…
```

theorem OAI.PolycyclicRecognition.eventually_exists_pair_good_on_mesh line 39

Source documentation

For all sufficiently large scales there is a single normalized pair whose normalized errors are small at every mesh point for more than half the endpoints. No pointwise supremum over a path is used.

theorem eventually_exists_pair_good_on_mesh
    {G W I Y : Type*} [Group G] [MetricSpace G] [ProperSpace G]
    [IsTopologicalGroup G] [IsIsometricSMul G G] {Λ : ℝ≥0}
    [MeasurableSpace G] [BorelSpace G]
    [MeasurableSpace (NormalizedPair G Λ)] [BorelSpace (NormalizedPair G Λ)]
    [NormedAddCommGroup W] [NormedSpace ℝ W]
    [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W]
    [Fintype I] [MeasurableSpace Y]
    (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
    (ν : Measure Y) [IsProbabilityMeasure ν]
    (π l : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) (hl : Continuous fun g => (l g).toAdd)
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair