OAI/Probability/SLE/Multipoint/MultipointRadiusStatus.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The literal radius stop is the inverse of the actual increasing radius clock. Horizon truncation preserves all threshold tests strictly before its cutoff, including equality at a crossed threshold.

  1. lemma OAI.SLEExactGauge.radiusLevelTime_le_iff_clock line 17
  2. lemma OAI.SLEExactGauge.radiusLevelTime_eq_iff_clock line 46
  3. lemma OAI.SLEExactGauge.radiusLevelTime_lt_iff_clock line 65
  4. lemma OAI.SLEExactGauge.cutoffStop_reached_before_horizon line 82
  5. lemma OAI.SLEExactGauge.cutoffStop_strictly_reached_before_horizon line 90
  6. lemma OAI.SLEExactGauge.cutoffStop_eq_before_horizon line 98
  7. def OAI.SLEExactGauge.Multipoint.sourceClockLevel line 106
  8. lemma OAI.SLEExactGauge.Multipoint.cutoff_radius_reached_iff line 108
  9. lemma OAI.SLEExactGauge.Multipoint.cutoff_radius_strictly_reached_iff line 132
  10. lemma OAI.SLEExactGauge.Multipoint.cutoff_radius_eq_iff line 156
  11. theorem OAI.SLEExactGauge.Multipoint.cutoff_radius_factor_thresholds line 182

    Source documentation

    The three concrete radius switches give exactly the source branch thresholds, also after truncation at H + 1.

    theorem cutoff_radius_factor_thresholds
    {Ω : Type*} {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hU : Continuous U) (hw : IsCapacityTwoWitness U γ G F)
    {κ : ℝ} (hκ : 0 < κ) (z : ℂ) (u₀ u₂ : ℝ) (h₀ : 0 ≤ u₀) (h₂ : 0 ≤ u₂)
    (H t : ℝ≥0) (htH : t ≤ H) (ht : z ∈ survivingDomain γ t) (ω : Ω) :
    let τ := fun u => cutoffStop (fun _ : Ω => (radiusLevelTime γ G z u : WithTop ℝ≥0)) (H+1) ω
…

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.cutoffStop, OAI.SLEExactGauge.radiusLevelTime

  12. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.physical_radius_at_activation line 231

    Source documentation

    At the activation clock chosen from the physical initial radius, the physical conformal radius is exactly the prescribed activation radius.

    theorem IsCapacityTwoWitness.physical_radius_at_activation
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (hU : Continuous U)
    (J : ℂ → ℂ) (z : ℂ) (R b : ℝ) (hR : 0 < R) (hb : 0 < b)
    (hRdef : R = 2*z.im*‖deriv J z‖)
    (t : ℝ≥0) (ht : z ∈ survivingDomain γ t)
    (hclock : logRadiusClock (Real.log z.im) (logLoewnerCoordinates G z t) =
      Real.log (R/b)) :
    physicalConformalRadius J G t z = b := by
…

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.logRadiusClock, OAI.SLEExactGauge.logLoewnerCoordinates, OAI.SLEExactGauge.physicalConformalRadius