StationaryMesh.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Selecting one map that is good on a finite mesh

The stationary volume comparison samples endpoints independently of the stationary map. Uniform L² bounds at finitely many sampled path points give a single map for which most endpoints have every sampled error small. The finite mesh is fixed before the scale tends to infinity.

theorem OAI.PolycyclicRecognition.measure_bad_mesh_le line 22

Source documentation

Chebyshev and the finite union bound for a fixed mesh.

theorem measure_bad_mesh_le
    {I Z E : Type*} [Fintype I] [MeasurableSpace Z] [NormedAddCommGroup E]
    (μ : Measure Z) (f : I → Z → E) {η a : ℝ≥0∞}
    (hη : η ≠ 0) (hηtop : η ≠ ∞)
    (hbound : ∀ i, eLpNorm (f i) 2 μ ≤ a) :
    μ {z | ∃ i, η ≤ ‖f i z‖ₑ} ≤ (Fintype.card I : ℝ≥0∞) * (η⁻¹ ^ 2 * a ^ 2) := by
…

theorem OAI.PolycyclicRecognition.exists_fiber_measure_lt line 48

Source documentation

A set of small product measure has a small fiber over some point of a probability space. This selects the map after endpoint averaging.

theorem exists_fiber_measure_lt
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (μ : Measure X) (ν : Measure Y) [IsProbabilityMeasure μ] [SFinite ν]
    (s : Set (X × Y)) (hs : MeasurableSet s) {t : ℝ≥0∞}
    (hsmall : (μ.prod ν) s < t) :
    ∃ x, ν {y | (x, y) ∈ s} < t := by
…

theorem OAI.PolycyclicRecognition.exists_good_mesh_fiber line 65

Source documentation

Uniform L² estimates at each sampled point provide one stationary map with an exceptional endpoint set of arbitrarily prescribed small measure.

theorem exists_good_mesh_fiber
    {I X Y E : Type*} [Fintype I] [MeasurableSpace X] [MeasurableSpace Y]
    [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure X) (ν : Measure Y) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (f : I → X × Y → E) (hf : ∀ i, Measurable (f i))
    {η a t : ℝ≥0∞} (hη : η ≠ 0) (hηtop : η ≠ ∞)
    (hbound : ∀ i y, eLpNorm (fun x => f i (x, y)) 2 μ ≤ a)
    (hsmall : (Fintype.card I : ℝ≥0∞) * (η⁻¹ ^ 2 * a ^ 2) < t) :
    ∃ x, ν {y | ∃ i, η ≤ ‖f i (x, y)‖ₑ} < t := by
…