OAI/Probability/SLE/Mass/DominatedMassTestContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact-test continuity extends to every terminal-integrable weight. This permits weighted inverse-chart tests whose supports approach the old boundary, using domination by the Radon terminal mass.

  1. lemma OAI.SLEExactGauge.integral_test_distance_le_of_domination line 18
  2. theorem OAI.SLEExactGauge.continuous_integral_of_radon_domination line 29

    Source documentation

    Monotonicity is not needed: domination and compact-test continuity suffice.

    theorem continuous_integral_of_radon_domination
    (N : ℝ≥0 → Measure upperHalfPlane) (ν : Measure upperHalfPlane) [ν.Regular]
    (hdom : ∀ t, N t ≤ ν)
    (hcont : ∀ f : C_c(upperHalfPlane,ℝ), Continuous (fun t => ∫ z, f z ∂N t))
    (g : upperHalfPlane → ℝ) (hg : Integrable g ν) :
    Continuous (fun t => ∫ z, g z ∂N t) := by
…

    Mentions: OAI.SLEExactGauge.upperHalfPlane

  3. theorem OAI.SLEExactGauge.continuous_lintegral_of_radon_domination line 54