FrontSuccessMeasurability.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Measurable actual front passages. Local ribbon coordinates are extended from their closed patch only to construct an adapted stopping time; on every successful passage this stopping time is exactly the original first front.

def OAI.SLEExactGauge.FrontSuccessMeasurability.clampedPath line 21
Source documentation
Freeze a continuous path outside a finite time interval.
```
def clampedPath (f : C(ℝ≥0, ℂ)) (s t : ℝ≥0) : C(ℝ≥0, ℂ) :=
…
```
theorem OAI.SLEExactGauge.FrontSuccessMeasurability.measurable_clampedPath line 24
theorem OAI.SLEExactGauge.FrontSuccessMeasurability.sourceSausageSet_eq_clamped line 33

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.segmentSausageCharge_measurable line 48

Source documentation

Variable finite endpoints cause no measurability loss in the physical sausage charge. No stopping-time assumption on these endpoints is needed.

theorem segmentSausageCharge_measurable
    {Ω : Type*} [MeasurableSpace Ω] (f : Ω → C(ℝ≥0, ℂ)) (hf : Measurable f)
    (s t : Ω → ℝ≥0) (hs : Measurable s) (ht : Measurable t)
    (κ v : ℝ) (R : Set ℂ) :
    Measurable (fun ω => segmentSausageCharge κ (f ω) (s ω) (t ω) v R) := by
…

Mentions: OAI.SLEExactGauge.segmentSausageCharge

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.measurableSet_prefix_mapsTo line 68

Source documentation

An open target and a measurable finite endpoint give a measurable whole-prefix containment event.

theorem measurableSet_prefix_mapsTo
    {Ω : Type*} [MeasurableSpace Ω] (f : Ω → C(ℝ≥0, ℂ)) (hf : Measurable f)
    (t : Ω → ℝ≥0) (ht : Measurable t) (V : Set ℂ) (hV : IsOpen V) :
    MeasurableSet {ω | MapsTo (f ω) (Icc 0 (t ω)) V} := by
…

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.firstFrontTime_eq_of_prefix line 94

Source documentation

Agreement through an attained first hit identifies the first hitting time, regardless of how the two coordinates are defined later.

theorem firstFrontTime_eq_of_prefix
    (x y : ℝ≥0 → ℝ) (q : ℝ) (τ : ℝ≥0)
    (hx : firstFrontTime x q = (τ : WithTop ℝ≥0)) (hattain : x τ = q)
    (hxy : EqOn x y (Icc 0 τ)) :
    firstFrontTime y q = (τ : WithTop ℝ≥0) := by
…

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.frontSuccess_eq_of_eqOn line 120

Source documentation

The concrete success event depends only on the coordinate inside its allowed region; the attained front equation makes this exact.

theorem frontSuccess_eq_of_eqOn
    {Ω : Type*} (η : ℕ → Ω → ℝ≥0 → ℂ) (p p' : ℕ → ℂ → ℝ)
    (σ : Ω → ℝ≥0) (V : ℕ → Set ℂ) (a : ℕ → ℂ) (ε : ℝ) (n : ℕ)
    (hpeq : EqOn (p n) (p' n) (V n)) :
    FrontSuccess η p σ V a ε n = FrontSuccess η p' σ V a ε n := by
…

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.firstFrontTime_stopping line 142

Source documentation

A globally continuous progress coordinate gives the actual adapted front stopping time, including the possibility of no hit.

theorem firstFrontTime_stopping
    {Ω : Type*} [m : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 m)
    (η : Ω → ℝ≥0 → ℂ) (ha : Adapted ℱ (fun t ω => η ω t))
    (hc : ∀ ω, Continuous (η ω)) (p : ℂ → ℝ) (hp : Continuous p) :
    IsStoppingTime ℱ (fun ω => firstFrontTime (fun t => p (η ω t)) 1) :=
…

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.measurableSet_frontSuccess_of_continuous line 152

Source documentation

Success is measurable when the progress coordinate is globally continuous; the next theorem removes this unnecessary global requirement.

theorem measurableSet_frontSuccess_of_continuous
    {Ω : Type*} [m : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 m)
    (η : ℕ → Ω → ℝ≥0 → ℂ) (p : ℕ → ℂ → ℝ) (σ : Ω → ℝ≥0)
    (V : ℕ → Set ℂ) (a : ℕ → ℂ) (ε : ℝ) (n : ℕ)
    (ha : Adapted ℱ (fun t ω => η n ω t)) (hc : ∀ ω, Continuous (η n ω))
    (hp : Continuous (p n)) (hσ : Measurable σ) (hV : IsOpen (V n)) :
    MeasurableSet (FrontSuccess η p σ V a ε n) := by
…

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.exists_continuous_progress_extension line 181
Source documentation
A closed physical ribbon patch supplies a continuous progress extension by the proved Tietze theorem.
```
theorem exists_continuous_progress_extension
    (p : ℂ → ℝ) (K : Set ℂ) (hK : IsClosed K) (hp : ContinuousOn p K) :
    ∃ g : C(ℂ, ℝ), EqOn p g K := by
…
```

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.measurableSet_frontSuccess_of_continuousOn line 193

Source documentation

The original local front event is measurable, and agrees there with an adapted front stopping time obtained by extending the ribbon coordinate.

theorem measurableSet_frontSuccess_of_continuousOn
    {Ω : Type*} [m : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 m)
    (η : ℕ → Ω → ℝ≥0 → ℂ) (p : ℕ → ℂ → ℝ) (σ : Ω → ℝ≥0)
    (V : ℕ → Set ℂ) (a : ℕ → ℂ) (ε : ℝ) (n : ℕ)
    (ha : Adapted ℱ (fun t ω => η n ω t)) (hc : ∀ ω, Continuous (η n ω))
    (K : Set ℂ) (hK : IsClosed K) (hp : ContinuousOn (p n) K)
    (hσ : Measurable σ) (hV : IsOpen (V n)) (hVK : V n ⊆ K) :
    MeasurableSet (FrontSuccess η p σ V a ε n) ∧
      ∃ ρ : Ω → WithTop ℝ≥0, IsStoppingTime ℱ ρ ∧
        ∀ ω ∈ FrontSuccess η p σ V a ε n,
          ρ ω = firstFrontTime (fun t => p n (η n ω t)) 1 := by
…

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.measurableSet_frontSuccess_mass line 218

Source documentation

The full local-coordinate success-and-mass event is measurable. This is the concrete event used by the repeated ribbon passage argument.

theorem measurableSet_frontSuccess_mass
    {Ω : Type*} [m : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 m)
    (η : ℕ → Ω → ℝ≥0 → ℂ) (p : ℕ → ℂ → ℝ) (σ : Ω → ℝ≥0)
    (V : ℕ → Set ℂ) (a : ℕ → ℂ) (ε : ℝ) (n : ℕ)
    (ha : Adapted ℱ (fun t ω => η n ω t)) (hc : ∀ ω, Continuous (η n ω))
    (K : Set ℂ) (hK : IsClosed K) (hp : ContinuousOn (p n) K)
    (hσ : Measurable σ) (hV : IsOpen (V n)) (hVK : V n ⊆ K)
    (κ v c : ℝ) (R : Set ℂ) :
    MeasurableSet {ω | ω ∈ FrontSuccess η p σ V a ε n ∧ ENNReal.ofReal c ≤
      segmentSausageCharge κ (η n ω) (σ ω)
        (frontTime (fun t => p n (η n ω t)) 1) v R} := by
…

Mentions: OAI.SLEExactGauge.segmentSausageCharge