FrontSuccessStopped.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The front success-and-mass event is measurable in the actual extended front past, not merely in the full path sigma algebra.

def OAI.SLEExactGauge.FrontSuccessMeasurability.stoppedAtPath line 20
Source documentation
Stop at a possibly infinite time, leaving the path running if no front is ever reached.
```
def stoppedAtPath (f : C(ℝ≥0, ℂ)) (ρ : WithTop ℝ≥0) : C(ℝ≥0, ℂ) :=
…
```
theorem OAI.SLEExactGauge.FrontSuccessMeasurability.stoppedAtPath_apply line 23

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.stoppedAtPath_measurable line 33

Source documentation

The whole stopped path is measurable in its stopping-time past even when that stopping time can be infinite.

theorem stoppedAtPath_measurable
    {Ω : Type*} [m : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 m)
    (η : Ω → ℝ≥0 → ℂ) (ha : Adapted ℱ (fun t ω => η ω t))
    (hc : ∀ ω, Continuous (η ω)) (ρ : Ω → WithTop ℝ≥0) (hρ : IsStoppingTime ℱ ρ) :
    Measurable[hρ.measurableSpace]
      (fun ω => stoppedAtPath (sourceTracePath η hc ω) (ρ ω)) := by
…

Mentions: OAI.SLEExactGauge.FrontSuccessMeasurability.stoppedAtPath, OAI.SLEExactGauge.sourceTracePath

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.truncated_start_measurable line 51

Source documentation

A finite original stopping time truncated at the front is measurable in the front past.

theorem truncated_start_measurable
    {Ω : Type*} [m : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 m)
    (σ : Ω → ℝ≥0) (hσ : IsStoppingTime ℱ (fun ω => (σ ω : WithTop ℝ≥0)))
    (ρ : Ω → WithTop ℝ≥0) (hρ : IsStoppingTime ℱ ρ) :
    Measurable[hρ.measurableSpace]
      (fun ω => (min (σ ω : WithTop ℝ≥0) (ρ ω)).untopD 0) := by
…

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.firstFrontTime_attained line 61

Source documentation

A finite first front for a continuous coordinate is attained.

theorem firstFrontTime_attained
    (x : ℝ≥0 → ℝ) (hx : Continuous x) (q : ℝ) (τ : ℝ≥0)
    (hτ : firstFrontTime x q = (τ : WithTop ℝ≥0)) : x τ = q := by
…

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.frontSuccess_stopped_eq line 76

Source documentation

Stopping the path and truncating the earlier time at the front does not change the concrete success event.

theorem frontSuccess_stopped_eq
    {Ω : Type*} (η : ℕ → Ω → ℝ≥0 → ℂ) (p : ℕ → ℂ → ℝ)
    (σ : Ω → ℝ≥0) (V : ℕ → Set ℂ) (a : ℕ → ℂ) (ε : ℝ) (n : ℕ)
    (hc : ∀ ω, Continuous (η n ω)) (hp : Continuous (p n)) :
    let ρ := fun ω => firstFrontTime (fun t => p n (η n ω t)) 1
…

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.frontSuccess_mass_stopped_eq line 126

Source documentation

The mass on a successful passage is also unchanged by stopping at the front, including the earlier endpoint.

theorem frontSuccess_mass_stopped_eq
    {Ω : Type*} (η : ℕ → Ω → ℝ≥0 → ℂ) (p : ℕ → ℂ → ℝ)
    (σ : Ω → ℝ≥0) (V : ℕ → Set ℂ) (a : ℕ → ℂ) (ε : ℝ) (n : ℕ)
    (hc : ∀ ω, Continuous (η n ω)) (hp : Continuous (p n)) (κ v c : ℝ) (R : Set ℂ) :
    let ρ := fun ω => firstFrontTime (fun t => p n (η n ω t)) 1
…

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.frontSuccess_mass_measurable_at_front line 178

Source documentation

The full success-and-mass event belongs to the front past.

theorem frontSuccess_mass_measurable_at_front
    {Ω : 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σ : IsStoppingTime ℱ (fun ω => (σ ω : WithTop ℝ≥0)))
    (hV : IsOpen (V n)) (κ v c : ℝ) (R : Set ℂ) :
    let hρ := firstFrontTime_stopping ℱ (η n) ha hc (p n) hp
…

Mentions: OAI.SLEExactGauge.FrontSuccessMeasurability.firstFrontTime_stopping

theorem OAI.SLEExactGauge.FrontSuccessMeasurability.local_frontSuccess_mass_measurable_at_front line 205

Source documentation

Local physical ribbon coordinates suffice for an actual stopping time whose past contains the full success-and-mass event.

theorem local_frontSuccess_mass_measurable_at_front
    {Ω : 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σ : IsStoppingTime ℱ (fun ω => (σ ω : WithTop ℝ≥0)))
    (hV : IsOpen (V n)) (hVK : V n ⊆ K) (κ v c : ℝ) (R : Set ℂ) :
    ∃ ρ : Ω → WithTop ℝ≥0, ∃ hρ : IsStoppingTime ℱ ρ,
      MeasurableSet[hρ.measurableSpace] (FrontSuccess η p σ V a ε n) ∧
      MeasurableSet[hρ.measurableSpace] {ω | ω ∈ FrontSuccess η p σ V a ε n ∧ ENNReal.ofReal c ≤
        segmentSausageCharge κ (η n ω) (σ ω)
…

Mentions: OAI.SLEExactGauge.segmentSausageCharge