TerminalGenericWindows.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Generic control on a fixed terminal fraction of a real orbit

Polynomial shearing changes uniformly little on a sufficiently short fixed terminal fraction. Prefix genericity controls that fraction with the explicit loss 2 / delta. The fraction is chosen after the finite test accuracy, and is independent of the pair and stopping time.

theorem OAI.DukePrimeDegree.terminal_window_average_error line 20

theorem OAI.DukePrimeDegree.terminal_window_control_of_prefix_control line 61

Source documentation

One prefix-generic set controls every sufficiently late terminal window, including a stopping time depending on both initial points.

theorem terminal_window_control_of_prefix_control
    {Y : Type*} (U : ℝ → Y → Y) (f : Y → ℝ)
    (hint : ∀ x a b, IntervalIntegrable (fun t => f (U t x)) volume a b)
    (G : Set Y) (c ε δ R : ℝ)
    (hε : 0 ≤ ε) (hδ : 0 < δ) (hδ1 : δ < 1) (hR : 0 < R)
    (hgood : ∀ x ∈ G, ∀ T ≥ R,
      |T⁻¹ * (∫ t in (0 : ℝ)..T, f (U t x)) - c| ≤ ε) :
    ∀ x ∈ G, ∀ T ≥ R / (1 - δ),
      |(δ * T)⁻¹ * (∫ t in ((1 - δ) * T)..T, f (U t x)) - c| ≤ 2 * ε / δ := by
…

theorem OAI.DukePrimeDegree.exists_uniform_terminal_flow_generic_set line 83

Source documentation

Actual full-real-flow ergodicity supplies the fixed good set. No ergodicity of an arbitrarily chosen discrete time is assumed.

theorem exists_uniform_terminal_flow_generic_set
    {Y : Type*} [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y]
    [MulAction (Multiplicative ℝ) Y] [ContinuousSMul (Multiplicative ℝ) Y]
    (μ : Measure Y) [IsProbabilityMeasure μ] [ErgodicSMul (Multiplicative ℝ) Y μ]
    (f : Y →ᵇ ℝ) (ε δ η : ℝ)
    (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ < 1) (hη : 0 < η) :
    ∃ G : Set Y, MeasurableSet G ∧ μ Gᶜ ≤ ENNReal.ofReal η ∧
      ∃ R : ℝ, 0 < R ∧ ∀ x ∈ G, ∀ T ≥ R,
        |(δ * T)⁻¹ * (∫ t in ((1 - δ) * T)..T,
          f (realActionTime t x)) - ∫ y, f y ∂μ| ≤ ε := by
…

Mentions: OAI.DukePrimeDegree.realActionTime