OAI/Probability/SLE/Geometry/JointRadiusKernel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Jointly measurable geometric radius and radius-level kernels, constructed from the clipped Loewner equations. Agreement holds simultaneously at every marked point and nonnegative radius level on each actual capacity witness.

  1. lemma OAI.SLEExactGauge.fullRadius_strictAnti_on_live line 17
  2. lemma OAI.SLEExactGauge.radiusLevelTime_lt_of_live_radius_lt line 35
  3. lemma OAI.SLEExactGauge.radiusLevelTime_lt_iff_dense line 58

    Source documentation

    A radius level is before x exactly when a time in one fixed countable dense set is before x, still live, and strictly beyond that radius level.

    lemma radiusLevelTime_lt_iff_dense
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hU : Continuous U) (hw : IsCapacityTwoWitness U γ G F)
    (z : ℂ) (u : ℝ) (hu : 0 ≤ u) (x : ℝ≥0∞) :
    radiusLevelTime γ G z u < x ↔ ∃ n : ℕ,
      (denseSeq ℝ≥0 n : ℝ≥0∞) < x ∧
      z ∈ survivingDomain γ (denseSeq ℝ≥0 n) ∧
      fullRadius G (denseSeq ℝ≥0 n) z < (2 * z.im) * Real.exp (-u) := by
…

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

  4. def OAI.SLEExactGauge.SpatialClippedFamily.jointLive line 94
  5. lemma OAI.SLEExactGauge.SpatialClippedFamily.jointLive_measurable line 96
  6. lemma OAI.SLEExactGauge.SpatialClippedFamily.jointLive_iff line 100
  7. def OAI.SLEExactGauge.SpatialClippedFamily.radiusApprox line 111
  8. lemma OAI.SLEExactGauge.SpatialClippedFamily.radiusApprox_measurable line 116
  9. def OAI.SLEExactGauge.SpatialClippedFamily.jointRadius line 125
  10. lemma OAI.SLEExactGauge.SpatialClippedFamily.jointRadius_measurable line 128
  11. lemma OAI.SLEExactGauge.SpatialClippedFamily.jointRadius_eq line 132
  12. def OAI.SLEExactGauge.SpatialClippedFamily.jointRadiusLevel line 147
  13. lemma OAI.SLEExactGauge.SpatialClippedFamily.jointRadiusLevel_measurable line 152
  14. lemma OAI.SLEExactGauge.SpatialClippedFamily.jointRadiusLevel_eq line 164
  15. theorem OAI.SLEExactGauge.exists_joint_radius_and_level line 188

    Source documentation

    The kernels agree on one probability-one set simultaneously for all points, all times, and every nonnegative radius level. Consequently random measurable marked states may be substituted without changing that null set.

    theorem exists_joint_radius_and_level
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    (U : ℝ≥0 → Ω → ℝ)
    (hUm : Measurable (fun p : ℝ≥0 × Ω => U p.1 p.2))
    (hUc : ∀ ω, Continuous (fun t => U t ω))
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ᵐ ω ∂P, IsCapacityTwoWitness (fun t => U t ω) (γ ω) (G ω) (F ω)) :
    ∃ R : ℝ≥0 × (ℂ × Ω) → ℝ, ∃ τ : ℝ × (ℂ × Ω) → ℝ≥0∞,
      Measurable R ∧ Measurable τ ∧ ∀ᵐ ω ∂P,
        (∀ t z, R (t, z, ω) =
          if z ∈ survivingDomain (γ ω) t then fullRadius (G ω) t z else 0) ∧
        (∀ u, 0 ≤ u → ∀ z, τ (u, z, ω) = radiusLevelTime (γ ω) (G ω) z u) := by
…

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