FrontClockChange.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The exact change of capacity clock in a first-front passage. Ordered time changes preserve the stopped trace segment and its sausage, including the attained first front and terminal offset. This applies to the positive linear clocks arising from normalized Loewner charts.

theorem OAI.SLEExactGauge.FrontClockChange.firstFrontTime_of_clock_hit line 17
theorem OAI.SLEExactGauge.FrontClockChange.sourceSausageSet_clock line 35
theorem OAI.SLEExactGauge.FrontClockChange.segmentSausageCharge_clock line 48
theorem OAI.SLEExactGauge.FrontClockChange.frontSuccess_clock_transport line 55
theorem OAI.SLEExactGauge.FrontClockChange.frontSuccess_clock_iff line 80

theorem OAI.SLEExactGauge.FrontClockChange.frontSuccess_mass_clock line 99

Source documentation

The full success-and-mass event is unchanged by capacity-clock normalization. It is an exact event identity, before taking probabilities.

theorem frontSuccess_mass_clock
    {Ω : Type*} (e : ℝ≥0 ≃o ℝ≥0) (η : Ω → ℝ≥0 → ℂ)
    (p : ℂ → ℝ) (σ : Ω → ℝ≥0) (V : Set ℂ) (a : ℂ) (ε κ v c : ℝ) (R : Set ℂ) :
    {ω | ω ∈ FrontSuccess (fun _ ω t => η ω (e t)) (fun _ => p)
        (fun ω => e.symm (σ ω)) (fun _ => V) (fun _ => a) ε 0 ∧
      ENNReal.ofReal c ≤ segmentSausageCharge κ (fun t => η ω (e t))
        (e.symm (σ ω)) (frontTime (fun t => p (η ω (e t))) 1) v R} =
    {ω | ω ∈ FrontSuccess (fun _ => η) (fun _ => p) σ
        (fun _ => V) (fun _ => a) ε 0 ∧
      ENNReal.ofReal c ≤ segmentSausageCharge κ (η ω) (σ ω)
        (frontTime (fun t => p (η ω t)) 1) v R} := by
…

Mentions: OAI.SLEExactGauge.segmentSausageCharge