CanonicalJointDisk.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Joint angle and sample measurability of actual canonical disk masses at radius stops. No angle-dependent exceptional set is selected.

lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.disk_at_parameter_measurable line 21
def OAI.SLEExactGauge.Multipoint.CanonicalMass.diskAtRadius line 33
Source documentation
The actual compact disk mass at the indicated logarithmic radius level. Infinite radius times use the already constructed terminal measure.
```
def diskAtRadius (θ u : ℝ) (ω : Ω) : ℝ :=
…
```
lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.diskAtRadius_nonneg line 37
lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.diskAtRadius_joint_measurable line 40
lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.diskAtRadius_eq_finite line 60

lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.levelCoefficient_eq_diskAtRadius_moment line 76

Source documentation

The moment identity uses the same jointly measurable disk variable which enters tail events, with exactly the prescribed inner-clock scaling.

lemma levelCoefficient_eq_diskAtRadius_moment [IsProbabilityMeasure P]
    (hB : IsBrownianReal B P)
    (hc : ∀ ω, Continuous (fun t => B t ω)) (h0 : ∀ ω, B 0 ω=0)
    (hκ : 0<κ) (hκ8 : κ<8) (F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ*B t ω) (γ ω) (G ω) (F ω))
    (hgrowth : PublishedDiskUnivalentGrowth) (W : Target.WienerLaw) (hW : Target.IsWiener W)
    (θ : ℝ) (hθ : θ∈Ioo (0:ℝ) Real.pi) (ℓ : ℝ) (hℓ : 0≤ℓ) (m : ℕ) :
    ENNReal.ofReal (Target.levelCoefficient κ W ℓ m θ) =
      ∫⁻ ω, ENNReal.ofReal (C.diskAtRadius θ (4*ℓ/κ) ω)^m
        ∂finiteCenteredLaw P κ B γ G (Target.diskMapInv θ 0) (4*ℓ/κ) := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedDiskUnivalentGrowth, OAI.SLEExactGauge.Target.WienerLaw, OAI.SLEExactGauge.Target.IsWiener, OAI.SLEExactGauge.Target.levelCoefficient, OAI.SLEExactGauge.finiteCenteredLaw, OAI.SLEExactGauge.Target.diskMapInv