OAI/Probability/SLE/Multipoint/MultipointPhaseRegulator.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

On each active interval the finite phase selects exactly the raw radius regulator. Completion freezes the coordinate and removes its rate.

  1. lemma OAI.SLEExactGauge.Multipoint.phaseActive_iff_val line 16
  2. lemma OAI.SLEExactGauge.Multipoint.phaseAt_active_iff line 20
  3. lemma OAI.SLEExactGauge.Multipoint.phaseAt_first_iff line 40
  4. lemma OAI.SLEExactGauge.Multipoint.phaseAt_second_iff line 63
  5. lemma OAI.SLEExactGauge.Multipoint.phaseAt_active_stopped_state line 86
  6. lemma OAI.SLEExactGauge.Multipoint.phaseAt_active_stopped_velocity line 96
  7. lemma OAI.SLEExactGauge.Multipoint.phaseAt_active_chart line 108

    Source documentation

    Agreement up to each point's own completion suffices on every active phase; no common live endpoint for all coordinates is required.

    lemma phaseAt_active_chart {Ω ι : Type*}
    (ρ : (ι × Fin 3) → Ω → ℝ≥0) (ω : Ω) (i : ι)
    (hρ : Monotone (fun k => ρ (i,k) ω)) (t : ℝ≥0)
    (hactive : phaseActive (phaseAt ρ t ω i))
    (Q : ℝ → Ω → ι → ℂ × ℝ) (G : ℝ≥0 → ℂ → ℂ) (z : ℂ)
    (hQ : EqOn (fun u => Q u ω i) (logLoewnerCoordinates G z)
      (Icc 0 (ρ (i,2) ω : ℝ))) :
    stoppedCoordinateState Q (fun i => ρ (i,2)) t ω i =
      logLoewnerCoordinates G z t := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.phaseActive, OAI.SLEExactGauge.Multipoint.phaseAt, OAI.SLEExactGauge.logLoewnerCoordinates, OAI.SLEExactGauge.Multipoint.stoppedCoordinateState

  8. theorem OAI.SLEExactGauge.Multipoint.phaseRegulator_eq_and_le_one line 123

    Source documentation

    The selected active branch has the raw regulator and never exceeds one.

    theorem phaseRegulator_eq_and_le_one (κ β a U : ℝ) (hβ : 0 ≤ β)
    (j : Fin 4) (hj : phaseActive j) (z : ℂ × ℝ)
    (hfirst : j = 1 → 0 ≤ logFactorClock κ z-a ∧ logFactorClock κ z-a ≤ U/2)
    (hsecond : j = 2 → U/2 ≤ logFactorClock κ z-a ∧ logFactorClock κ z-a ≤ U) :
    branchRegulator κ (phaseRegulatorScale β a U j) (phaseRegulatorSlope β j) z =
      regulator β U (logFactorClock κ z-a) ∧
    branchRegulator κ (phaseRegulatorScale β a U j) (phaseRegulatorSlope β j) z ≤ 1 := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.phaseActive, OAI.SLEExactGauge.Multipoint.logFactorClock, OAI.SLEExactGauge.Multipoint.branchRegulator, OAI.SLEExactGauge.Multipoint.phaseRegulatorScale, OAI.SLEExactGauge.Multipoint.phaseRegulatorSlope, OAI.SLEExactGauge.Multipoint.regulator

  9. theorem OAI.SLEExactGauge.Multipoint.phaseAt_regulator_eq_and_le_one line 142

    Source documentation

    Threshold status for the actual stopping-time phase supplies the branch bounds; no separate regulator assumption is needed.

    theorem phaseAt_regulator_eq_and_le_one {Ω ι : Type*}
    (ρ : (ι × Fin 3) → Ω → ℝ≥0) (ω : Ω) (i : ι)
    (hρ : Monotone (fun k => ρ (i,k) ω)) (t : ℝ≥0)
    (κ β a U : ℝ) (hβ : 0 ≤ β) (z : ℂ × ℝ)
    (hactive : phaseActive (phaseAt ρ t ω i))
    (hstart : ρ (i,0) ω ≤ t → 0 ≤ logFactorClock κ z-a)
    (hbefore : t < ρ (i,1) ω → logFactorClock κ z-a ≤ U/2)
    (hafter : ρ (i,1) ω ≤ t → U/2 ≤ logFactorClock κ z-a)
    (hend : t < ρ (i,2) ω → logFactorClock κ z-a ≤ U) :
    branchRegulator κ (phaseRegulatorScale β a U (phaseAt ρ t ω i))
      (phaseRegulatorSlope β (phaseAt ρ t ω i)) z =
      regulator β U (logFactorClock κ z-a) ∧
…

    Mentions: OAI.SLEExactGauge.Multipoint.phaseActive, OAI.SLEExactGauge.Multipoint.phaseAt, OAI.SLEExactGauge.Multipoint.logFactorClock, OAI.SLEExactGauge.Multipoint.branchRegulator, OAI.SLEExactGauge.Multipoint.phaseRegulatorScale, OAI.SLEExactGauge.Multipoint.phaseRegulatorSlope, OAI.SLEExactGauge.Multipoint.regulator