RadonTestLimitProperties.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Order and closed-support properties of the reconstructed Radon limits.

lemma OAI.SLEExactGauge.compact_measure_le_test_integral line 16
lemma OAI.SLEExactGauge.test_integral_le_measure line 24

theorem OAI.SLEExactGauge.radon_measure_le_of_nonneg_tests line 33

Source documentation

The positive compact-test order determines the order of Radon measures.

theorem radon_measure_le_of_nonneg_tests (μ ν : Measure X) [μ.Regular] [ν.Regular]
    (h : ∀ f : C_c(X, ℝ), (∀ x, 0 ≤ f x) → (∫ x, f x ∂μ) ≤ ∫ x, f x ∂ν) : μ ≤ ν := by
…

theorem OAI.SLEExactGauge.radon_limits_mono line 58

Source documentation

Order of positive approximants passes to every compact-test limit.

theorem radon_limits_mono (μ ν : ℕ → Measure X)
    [∀ n, IsFiniteMeasureOnCompacts (μ n)] [∀ n, IsFiniteMeasureOnCompacts (ν n)]
    (μ₀ ν₀ : Measure X) [μ₀.Regular] [ν₀.Regular]
    (hμ : ∀ f : C_c(X, ℝ), Tendsto (fun n => ∫ x, f x ∂μ n) atTop (𝓝 (∫ x, f x ∂μ₀)))
    (hν : ∀ f : C_c(X, ℝ), Tendsto (fun n => ∫ x, f x ∂ν n) atTop (𝓝 (∫ x, f x ∂ν₀)))
    (hle : ∀ n, μ n ≤ ν n) : μ₀ ≤ ν₀ := by
…

theorem OAI.SLEExactGauge.radon_open_eq_zero_of_tests line 71

Source documentation

Vanishing compact tests inside an open set force the Radon mass of that open set to vanish.

theorem radon_open_eq_zero_of_tests (μ : Measure X) [μ.Regular] (U : Set X) (hU : IsOpen U)
    (hzero : ∀ f : C_c(X, ℝ), tsupport f ⊆ U → (∫ x, f x ∂μ)=0) : μ U=0 := by
…

theorem OAI.SLEExactGauge.radon_limit_carried_by_closed line 86

Source documentation

The compact-test limit is carried by a closed set if each compact test separated from it eventually vanishes.

theorem radon_limit_carried_by_closed (μ : ℕ → Measure X) (ν : Measure X) [ν.Regular]
    (hlim : ∀ f : C_c(X, ℝ), Tendsto (fun n => ∫ x, f x ∂μ n) atTop (𝓝 (∫ x, f x ∂ν)))
    (S : Set X) (hS : IsClosed S)
    (hvanish : ∀ f : C_c(X, ℝ), tsupport f ⊆ Sᶜ →
      ∀ᶠ n in atTop, (∫ x, f x ∂μ n)=0) : ν Sᶜ=0 := by
…