RadonTestLimit.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Deterministic reconstruction in mass:construction. A countable family locally dense in compactly supported continuous functions, including nonnegative exhaustion cutoffs, determines one Radon limit.

structure OAI.SLEExactGauge.LocalTestFamily line 21
Source documentation
A countable determining family with explicit support control. Density is in the uniform norm within each compact exhaustion set.
```
structure LocalTestFamily (X : Type*) [TopologicalSpace X] where
…
```
lemma OAI.SLEExactGauge.LocalTestFamily.weighted_approximation line 34
lemma OAI.SLEExactGauge.integral_sub_le_cutoff line 49

theorem OAI.SLEExactGauge.LocalTestFamily.integrals_cauchy line 61

Source documentation

Compactly supported integrals are Cauchy once the countable tests converge. Cutoff convergence supplies the uniform local mass bounds.

theorem LocalTestFamily.integrals_cauchy (D : LocalTestFamily X)
    (μ : ℕ → Measure X) [∀ n, IsFiniteMeasureOnCompacts (μ n)]
    (htest : ∀ j, ∃ a : ℝ, Tendsto (fun n => ∫ x, D.test j x ∂μ n) atTop (𝓝 a))
    (f : C_c(X, ℝ)) : CauchySeq (fun n => ∫ x, f x ∂μ n) := by
…

Mentions: OAI.SLEExactGauge.LocalTestFamily

theorem OAI.SLEExactGauge.radon_limit_of_all_test_limits line 98

Source documentation

Positive limits of compact continuous tests are represented by one locally finite regular measure.

theorem radon_limit_of_all_test_limits (μ : ℕ → Measure X)
    [∀ n, IsFiniteMeasureOnCompacts (μ n)]
    (hlimit : ∀ f : C_c(X, ℝ), ∃ a : ℝ,
      Tendsto (fun n => ∫ x, f x ∂μ n) atTop (𝓝 a)) :
    ∃ ν : Measure X, ν.Regular ∧ IsFiniteMeasureOnCompacts ν ∧
      ∀ f : C_c(X, ℝ), Tendsto (fun n => ∫ x, f x ∂μ n) atTop (𝓝 (∫ x, f x ∂ν)) := by
…

theorem OAI.SLEExactGauge.LocalTestFamily.exists_radon_limit line 125

Source documentation

Reconstruction from a single countable locally determining family.

theorem LocalTestFamily.exists_radon_limit (D : LocalTestFamily X)
    (μ : ℕ → Measure X) [∀ n, IsFiniteMeasureOnCompacts (μ n)]
    (htest : ∀ j, ∃ a : ℝ, Tendsto (fun n => ∫ x, D.test j x ∂μ n) atTop (𝓝 a)) :
    ∃ ν : Measure X, ν.Regular ∧ IsFiniteMeasureOnCompacts ν ∧
      ∀ f : C_c(X, ℝ), Tendsto (fun n => ∫ x, f x ∂μ n) atTop (𝓝 (∫ x, f x ∂ν)) := by
…

Mentions: OAI.SLEExactGauge.LocalTestFamily