OAI/Probability/SLE/Mass/CanonicalMassRemaining.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.Multipoint.CanonicalMass.atTime line 24
2. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.atTime_radon line 27
3. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.atTime_measurable line 31
4. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.atTime_le_terminal line 35
5. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.atTime_mean_le line 43
6. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.exists_remaining_kernel line 49
7. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.exists_remaining_random_tests line 71

   Source documentation

   The kernel permits all nonnegative tests jointly measurable in the original stopped past and the spatial point, with arbitrary compact support.

   theorem exists_remaining_random_tests
       (hBc : ∀ ω, Continuous (fun t => B t ω)) (F : Ω → ℝ≥0 → ℂ → ℂ)
       (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
       (S : Ω → WithTop ℝ≥0)
       (hS : IsStoppingTime (Filtration.natural B (fun r =>
         (hBm.comp (measurable_const.prodMk measurable_id) : Measurable (B r)).stronglyMeasurable)) S) :
       ∃ η : Ω → Measure upperHalfPlane, Measurable η ∧
         (∀ ω, (η ω).Regular ∧ IsFiniteMeasureOnCompacts (η ω)) ∧
         (∀ᵐ ω ∂P, η ω + C.atTime (S ω) ω = C.rational.terminal ω) ∧
         ∀ K : Set upperHalfPlane, IsCompact K → ∀ f : Ω × upperHalfPlane → ℝ≥0∞,
           Measurable[hS.measurableSpace.prod inferInstance] f →
           (∫⁻ ω, (∫⁻ z in K, f (ω,z) ∂η ω) ∂P) =
   …

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