RationalTraceMass.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Continuous extension of a rational measure family whose positive increments are supported on the corresponding trace intervals.

structure OAI.SLEExactGauge.RationalTraceIncrements line 21
Source documentation
This is the positive-increment and interval-support assertion used in the pathwise extension. Local applications restrict all measures to one compact set, making the terminal measure finite.
```
structure RationalTraceIncrements (μ : ℚ → Measure X) (ν : Measure X) (γ : ℝ → X) : Prop where
…
```
lemma OAI.SLEExactGauge.RationalTraceIncrements.monotone line 28
lemma OAI.SLEExactGauge.RationalTraceIncrements.integral_dist_le line 36
lemma OAI.SLEExactGauge.exists_rational_sequence_tendsto line 62

theorem OAI.SLEExactGauge.RationalTraceIncrements.exists_continuous_extension line 72

Source documentation

The rational family has an all-real-time regular extension, continuous against every compact continuous test. It is dominated by the same finite terminal measure, and agrees exactly at every rational time.

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

Mentions: OAI.SLEExactGauge.RationalTraceIncrements