RationalTraceMassControl.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Shrinking trace intervals have vanishing nonatomic mass. This gives local oscillation control and continuous extension from rational times.

theorem OAI.SLEExactGauge.trace_interval_mass_small line 22

Source documentation

Continuity and null singleton mass control every sufficiently short trace interval around any fixed time. It applies to a finite compact restriction of the terminal measure.

theorem trace_interval_mass_small (ν : Measure X) [ν.OuterRegular]
    [NullSingletonClass ν] (γ : ℝ → X) (hγ : Continuous γ)
    (t : ℝ) (ε : ℝ≥0∞) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ a b : ℝ, dist a t < δ → dist b t < δ →
      ν (γ '' Icc a b) < ε := by
…

theorem OAI.SLEExactGauge.exists_continuous_rational_extension line 41

Source documentation

A rational-time real observable with arbitrarily small local oscillation has a unique continuous extension to all real times.

theorem exists_continuous_rational_extension
    (f : ℚ → ℝ)
    (hosc : ∀ t : ℝ, ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
      ∀ p q : ℚ, dist (p:ℝ) t < δ → dist (q:ℝ) t < δ → dist (f p) (f q) < ε) :
    ∃ F : ℝ → ℝ, Continuous F ∧ (∀ q : ℚ, F q=f q) ∧
      ∀ G : ℝ → ℝ, Continuous G → (∀ q : ℚ, G q=f q) → G=F := by
…

theorem OAI.SLEExactGauge.continuous_rational_extension_of_trace_control line 67

Source documentation

The trace-support estimate for increments supplies the local oscillation hypothesis of the rational extension theorem.

theorem continuous_rational_extension_of_trace_control
    (ν : Measure X) [ν.OuterRegular] [IsFiniteMeasure ν] [NullSingletonClass ν]
    (γ : ℝ → X) (hγ : Continuous γ) (f : ℚ → ℝ) (C : ℝ) (hC : 0 ≤ C)
    (hcontrol : ∀ p q : ℚ, dist (f p) (f q) ≤
      C*(ν (γ '' Icc (min (p:ℝ) q) (max (p:ℝ) q))).toReal) :
    ∃ F : ℝ → ℝ, Continuous F ∧ (∀ q : ℚ, F q=f q) ∧
      ∀ G : ℝ → ℝ, Continuous G → (∀ q : ℚ, G q=f q) → G=F := by
…