OAI/Probability/SLE/Loewner/CanonicalInverseAngle.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.canonicalStoppedCenter line 20
2. def OAI.SLEExactGauge.canonicalStoppedSine line 24
3. def OAI.SLEExactGauge.canonicalStoppedAngleSq line 27
4. def OAI.SLEExactGauge.canonicalInverseAngle line 30
5. lemma OAI.SLEExactGauge.canonicalStoppedCenter_measurable line 33
6. lemma OAI.SLEExactGauge.canonicalStoppedSine_measurable line 41
7. lemma OAI.SLEExactGauge.canonicalStoppedAngleSq_measurable line 46
8. lemma OAI.SLEExactGauge.canonicalInverseAngle_measurable line 49
9. lemma OAI.SLEExactGauge.canonicalStoppedAngleSq_nonneg line 52
10. lemma OAI.SLEExactGauge.canonicalInverseAngle_nonneg line 55
11. lemma OAI.SLEExactGauge.canonicalStoppedCenter_eq line 58
12. lemma OAI.SLEExactGauge.canonicalStoppedSine_eq line 73
13. lemma OAI.SLEExactGauge.canonicalStoppedAngleSq_eq line 84
14. lemma OAI.SLEExactGauge.canonicalInverseAngle_eq line 96
15. lemma OAI.SLEExactGauge.measurable_canonicalStoppedSine_random_state line 104
16. lemma OAI.SLEExactGauge.measurableSet_canonical_good_angle_random_state line 112

    Source documentation

    One common measurable event can be used for all random marked states.

    lemma measurableSet_canonical_good_angle_random_state
        {Ω : Type*} [MeasurableSpace Ω] (κ s : ℝ)
        {Y : Ω → C(ℝ≥0, ℝ)} (hY : Measurable Y)
        {u : Ω → ℝ} (hu : Measurable u) {z : Ω → ℂ} (hz : Measurable z) :
        MeasurableSet {ω | canonicalRadiusLevel κ (u ω, z ω, Y ω) < ∞ ∧
          s ≤ canonicalStoppedSine κ (u ω, z ω, Y ω)} :=
    …

    Mentions: OAI.SLEExactGauge.canonicalRadiusLevel, OAI.SLEExactGauge.canonicalStoppedSine

17. theorem OAI.SLEExactGauge.canonical_uniform_inverse_angle line 124

    Source documentation

    The inverse-angle moment bound, represented by a single jointly measurable canonical kernel.

    theorem canonical_uniform_inverse_angle
        (ν : Measure C(ℝ≥0, ℝ)) [IsProbabilityMeasure ν]
        (hB : IsBrownianReal (fun (t : ℝ≥0) (p : C(ℝ≥0, ℝ)) => p t) ν)
        (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
        (Φ : C(ℝ≥0, ℝ) → C(ℝ≥0, ℂ))
        (Gc Fc : C(ℝ≥0, ℝ) → ℝ≥0 → ℂ → ℂ)
        (hw : ∀ᵐ p ∂ν, IsCapacityTwoWitness
          (fun t => Real.sqrt κ * p t) (Φ p) (Gc p) (Fc p))
        (z : ℂ) (hz : z ∈ upperHalfPlane) (v : ℝ≥0) (hv : 1 ≤ (v : ℝ)) :
        Integrable (fun p => canonicalInverseAngle κ ((v : ℝ), z, p))
          (ν.withDensity (fun p => canonicalFiniteDensity κ ((v : ℝ), z, p))) ∧
        (∫ p, canonicalInverseAngle κ ((v : ℝ), z, p)
    …

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.canonicalInverseAngle, OAI.SLEExactGauge.canonicalFiniteDensity

18. theorem OAI.SLEExactGauge.canonical_finiteCenteredLaw_live_angle line 151

    Source documentation

    Under the finite centered law the canonical stopped point is live and its angle is strictly in the upper half-plane.

    theorem canonical_finiteCenteredLaw_live_angle
        (ν : Measure C(ℝ≥0, ℝ)) [IsProbabilityMeasure ν]
        (hB : IsBrownianReal (fun (t : ℝ≥0) (p : C(ℝ≥0, ℝ)) => p t) ν)
        (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
        (Φ : C(ℝ≥0, ℝ) → C(ℝ≥0, ℂ))
        (Gc Fc : C(ℝ≥0, ℝ) → ℝ≥0 → ℂ → ℂ)
        (hw : ∀ᵐ p ∂ν, IsCapacityTwoWitness
          (fun t => Real.sqrt κ * p t) (Φ p) (Gc p) (Fc p))
        (z : ℂ) (hz : z ∈ upperHalfPlane) (u : ℝ) (hu : 0 ≤ u) :
        ∀ᵐ p ∂ν.withDensity (fun p => canonicalFiniteDensity κ (u, z, p)),
          canonicalRadiusLevel κ (u, z, p) < ∞ ∧ 0 < canonicalStoppedSine κ (u, z, p) := by
    …

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.canonicalFiniteDensity, OAI.SLEExactGauge.canonicalRadiusLevel, OAI.SLEExactGauge.canonicalStoppedSine

19. theorem OAI.SLEExactGauge.canonical_uniform_good_angle line 186

    Source documentation

    A uniform positive fraction of every finite centered law has an angle bounded away from the real axis. The same threshold works for every marked point and every radius level at least one.

    theorem canonical_uniform_good_angle
        (ν : Measure C(ℝ≥0, ℝ)) [IsProbabilityMeasure ν]
        (hB : IsBrownianReal (fun (t : ℝ≥0) (p : C(ℝ≥0, ℝ)) => p t) ν)
        (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
        (Φ : C(ℝ≥0, ℝ) → C(ℝ≥0, ℂ))
        (Gc Fc : C(ℝ≥0, ℝ) → ℝ≥0 → ℂ → ℂ)
        (hw : ∀ᵐ p ∂ν, IsCapacityTwoWitness
          (fun t => Real.sqrt κ * p t) (Φ p) (Gc p) (Fc p)) :
        ∃ s : ℝ, 0 < s ∧ ∀ z ∈ upperHalfPlane, ∀ v : ℝ≥0, 1 ≤ (v : ℝ) →
          ENNReal.ofReal (1 / 2 : ℝ) ≤
            (ν.withDensity (fun p => canonicalFiniteDensity κ ((v : ℝ), z, p)))
              {p | canonicalRadiusLevel κ ((v : ℝ), z, p) < ∞ ∧
    …

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.canonicalFiniteDensity, OAI.SLEExactGauge.canonicalRadiusLevel