RationalTraceMassAdapted.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Adapted and jointly measurable all-time Radon mass, obtained from rational left limits in the original filtration.

lemma OAI.SLEExactGauge.measurable_halfPlane_compact_test_integral line 17
theorem OAI.SLEExactGauge.halfPlane_extension_adapted line 31

theorem OAI.SLEExactGauge.halfPlane_extension_joint_measurable line 70

Source documentation

Joint measurability follows through real compact-test integrals; no topology on the space of Radon measures is required.

theorem halfPlane_extension_joint_measurable
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 mΩ)
    (μ : ℚ → Ω → Measure upperHalfPlane) (M : ℝ → Ω → Measure upperHalfPlane)
    (hMr : ∀ t ω, (M t ω).Regular)
    (hcont : ∀ ω (f : C_c(upperHalfPlane,ℝ)), Continuous (fun t => ∫ z, f z ∂M t ω))
    (hrat : ∀ (q : ℚ) ω, M q ω = μ q ω)
    (hμm : ∀ q : ℚ, 0 ≤ q → Measurable[ℱ (q : ℝ).toNNReal] (μ q)) :
    Measurable (fun q : ℝ≥0 × Ω => M q.1 q.2) := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.halfPlane_extension_progressive line 87