OAI/Probability/SLE/Mass/RationalTraceMassLocal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Rational-time reconstruction on the open half-plane. The terminal measure is only locally finite; the trace is allowed to touch the real line. Compact test supports supply the finite ambient control measures.

  1. structure OAI.SLEExactGauge.HalfPlaneTraceIncrements line 18
  2. lemma OAI.SLEExactGauge.HalfPlaneTraceIncrements.monotone line 25
  3. def OAI.SLEExactGauge.ambientCompactRestriction line 33
  4. lemma OAI.SLEExactGauge.ambientCompactRestriction_finite line 36
  5. lemma OAI.SLEExactGauge.ambientCompactRestriction_nullSingletons line 42
  6. lemma OAI.SLEExactGauge.HalfPlaneTraceIncrements.integral_dist_le line 53
  7. lemma OAI.SLEExactGauge.HalfPlaneTraceIncrements.continuous_test_extension line 100
  8. theorem OAI.SLEExactGauge.HalfPlaneTraceIncrements.exists_continuous_extension line 115

    Source documentation

    One locally finite Radon family extends all rational times. Every compact test is continuous, even when the physical trace meets the real line.

    theorem HalfPlaneTraceIncrements.exists_continuous_extension
    {μ : ℚ → Measure upperHalfPlane} {ν : Measure upperHalfPlane} [ν.Regular]
    [NullSingletonClass ν] {γ : ℝ → ℂ}
    (H : HalfPlaneTraceIncrements μ ν γ) (hγ : Continuous γ) :
    ∃ M : ℝ → Measure upperHalfPlane, (∀ t, (M t).Regular) ∧ (∀ t, M t ≤ ν) ∧
      (∀ q : ℚ, M q = μ q) ∧
      (∀ f : C_c(upperHalfPlane,ℝ), Continuous (fun t => ∫ z, f z ∂M t)) ∧ Monotone M := by
…

    Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.HalfPlaneTraceIncrements

  9. theorem OAI.SLEExactGauge.halfPlane_continuous_measure_extension_unique line 176

    Source documentation

    Agreement at rational times identifies continuous Radon families. Thus the reconstruction is independent of compact exhaustions.

    theorem halfPlane_continuous_measure_extension_unique
    (M N : ℝ → Measure upperHalfPlane)
    (hMr : ∀ t, (M t).Regular) (hNr : ∀ t, (N t).Regular)
    (hMc : ∀ f : C_c(upperHalfPlane,ℝ), Continuous (fun t => ∫ z, f z ∂M t))
    (hNc : ∀ f : C_c(upperHalfPlane,ℝ), Continuous (fun t => ∫ z, f z ∂N t))
    (heq : ∀ q : ℚ, M q = N q) : M = N := by
…

    Mentions: OAI.SLEExactGauge.upperHalfPlane