ActualAngleWarmup.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A one-unit conformal-radius warmup has a uniformly positive chance of producing a good angle, conditionally on every actual stopped-past event. The estimate uses the canonical Loewner witness.

lemma OAI.SLEExactGauge.IsCapacityTwoWitness.normalized_restart_stopped_sine line 25

lemma OAI.SLEExactGauge.canonical_good_angle_source_eq line 66

Source documentation

The canonical measurable event is exactly the geometric stopped-angle condition for the supplied actual witness.

lemma canonical_good_angle_source_eq
    {Ω : Type*} (κ : ℝ) (B : ℝ≥0 → Ω → ℝ)
    (hc : ∀ ω, Continuous (fun t => B t ω))
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (z : ℂ) (u s : ℝ) (hu : 0 ≤ u) :
    {ω | canonicalRadiusLevel κ (u, z, sourceDriverPath B hc ω) < ∞ ∧
      s ≤ canonicalStoppedSine κ (u, z, sourceDriverPath B hc ω)} =
    {ω | radiusLevelTime (γ ω) (G ω) z u < ∞ ∧
      s ≤ Real.sin (Complex.arg (G ω (radiusLevelTime (γ ω) (G ω) z u).toNNReal z -
        (Real.sqrt κ * B (radiusLevelTime (γ ω) (G ω) z u).toNNReal ω : ℝ)))} := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.canonicalRadiusLevel, OAI.SLEExactGauge.sourceDriverPath, OAI.SLEExactGauge.canonicalStoppedSine, OAI.SLEExactGauge.radiusLevelTime

theorem OAI.SLEExactGauge.actual_one_unit_angle_warmup line 86

Source documentation

The actual finite centered law is compared on every stopped-past event. The scale and canonical witness may be fixed before choosing that event.

theorem actual_one_unit_angle_warmup
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (B : ℝ≥0 → Ω → ℝ) (hB : IsBrownianReal B P)
    (hBm : Measurable (fun q : ℝ≥0 × Ω => B q.1 q.2))
    (hc : ∀ ω, Continuous (fun t => B t ω)) (hB0 : ∀ ω, B 0 ω = 0)
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (Φ : C(ℝ≥0, ℝ) → C(ℝ≥0, ℂ))
    (Gc Fc : C(ℝ≥0, ℝ) → ℝ≥0 → ℂ → ℂ)
    (hW : ∀ᵐ p ∂P.map (sourceDriverPath B hc), IsCapacityTwoWitness
      (fun t => Real.sqrt κ * p t) (Φ p) (Gc p) (Fc p)) :
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.sourceDriverPath