RationalTraceMassVariation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform local total-variation control for the all-time extension.

theorem OAI.SLEExactGauge.RationalTraceIncrements.local_variation_continuity line 18

Source documentation

Local total variation is expressed uniformly on measurable sets. The finite-terminal form applies to each compact restriction in the source.

theorem RationalTraceIncrements.local_variation_continuity
    {μ : ℚ → Measure X} {ν : Measure X} [ν.Regular] [IsFiniteMeasure ν]
    [NullSingletonClass ν] {γ : ℝ → X} (H : RationalTraceIncrements μ ν γ)
    (hγ : Continuous γ) (M : ℝ → Measure X)
    (hMr : ∀ t, (M t).Regular) (hdom : ∀ t, M t ≤ ν)
    (hrat : ∀ q : ℚ, M q=μ q)
    (hcont : ∀ f : C_c(X,ℝ), Continuous (fun t => ∫ x, f x ∂M t)) :
    ∀ t₀ : ℝ, ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
      ∀ s t : ℝ, dist s t₀ < δ → dist t t₀ < δ →
        ∀ A : Set X, MeasurableSet A → |(M s A).toReal-(M t A).toReal| < ε := by
…

Mentions: OAI.SLEExactGauge.RationalTraceIncrements

theorem OAI.SLEExactGauge.RationalTraceIncrements.exists_locally_tv_continuous_extension line 101

Source documentation

The pathwise rational squeeze gives one increasing extension with local total-variation continuity.

theorem RationalTraceIncrements.exists_locally_tv_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) ∧ Monotone M ∧
      (∀ f : C_c(X,ℝ), Continuous (fun t => ∫ x, f x ∂M t)) ∧
      ∀ t₀ : ℝ, ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
        ∀ s t : ℝ, dist s t₀ < δ → dist t t₀ < δ →
          ∀ A : Set X, MeasurableSet A → |(M s A).toReal-(M t A).toReal| < ε := by
…

Mentions: OAI.SLEExactGauge.RationalTraceIncrements