FlowSampleDomination.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Domination of all discrete microsteps by the fixed cutoff law

theorem OAI.PolycyclicRecognition.oneParameter_nat_mul line 15
theorem OAI.PolycyclicRecognition.microstep_time_mem_Icc line 24
Source documentation
All integer mesh starting times lie in the prescribed compact time interval, including when the final interval is shorter than a mesh step.
```
theorem microstep_time_mem_Icc {r T : ℝ} (hr : 0 < r) (hT : 0 ≤ T)
    (L : ℕ) (hL : 0 < L) (j : Fin ⌊r * T / (L : ℝ)⌋₊) :
    (j : ℝ) * L / r ∈ Icc 0 T := by
…
```

theorem OAI.PolycyclicRecognition.microstep_sample_laws_dominated line 41

Source documentation

Haar-preserving coordinate moves and the one fixed pair of cutoff densities imply every domination premise of the two-limit argument.

theorem microstep_sample_laws_dominated
    {A V G ι : Type*} [MeasurableSpace A] [MeasurableSpace V]
    [Group G] [MetricSpace G] [ProperSpace G] [IsTopologicalGroup G]
    [IsIsometricSMul G G] {Λ : ℝ≥0}
    [MeasurableSpace (NormalizedPair G Λ)] [BorelSpace (NormalizedPair G Λ)]
    {l : Filter ι} (m : Measure V) (samples : ι → ProbabilityMeasure A)
    (η ρ : V → ℝ) (hiη : Integrable η m) (hiρ : Integrable ρ m)
    (hpη : ∀ z, 0 ≤ η z) (hpρ : ∀ z, 0 ≤ ρ z)
    (hmη : ∫ z, η z ∂m = 1) (hmρ : ∫ z, ρ z ∂m = 1) (hρ : Measurable ρ)
    (r : ι → ℝ) (hr : ∀ᶠ i in l, 0 < r i) {T : ℝ} (hT : 0 ≤ T)
    (F : ι → V × ℝ → V)
    (hpres : ∀ i t, MeasurePreserving (fun z => F i (z, t)) m m)
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair