RadonTestMeasurability.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A Radon measure determined by measurable compact continuous tests is a measurable measure-valued function. Local finite restrictions are used, so no finite total-mass hypothesis is imposed.

theorem OAI.SLEExactGauge.exists_open_cutoff_sequence line 22

Source documentation

A fixed countable list of compact cutoffs recovers the mass of a fixed open set simultaneously for all Radon measures.

theorem exists_open_cutoff_sequence (U : Set X) (hU : IsOpen U) :
    ∃ f : ℕ → C_c(X, ℝ), (∀ n x, 0 ≤ f n x ∧ f n x ≤ 1) ∧
      (∀ n, tsupport (f n) ⊆ U) ∧ ∀ (μ : Measure X), μ.Regular →
        μ U = ⨆ n, ENNReal.ofReal (∫ x, f n x ∂μ) := by
…

theorem OAI.SLEExactGauge.measurable_open_evaluation_of_tests line 54

Source documentation

Measurability of all compact continuous test integrals implies measurability of every open-set evaluation.

theorem measurable_open_evaluation_of_tests
    {Ω : Type*} [MeasurableSpace Ω] (ν : Ω → Measure X)
    (hν : ∀ ω, (ν ω).Regular)
    (htest : ∀ f : C_c(X, ℝ), Measurable (fun ω => ∫ x, f x ∂ν ω))
    (U : Set X) (hU : IsOpen U) : Measurable (fun ω => ν ω U) := by
…

theorem OAI.SLEExactGauge.measurable_radon_of_open_evaluations line 68

Source documentation

Locally finite Radon kernels are measurable once all their open-set evaluations are measurable.

theorem measurable_radon_of_open_evaluations
    {Ω : Type*} [MeasurableSpace Ω] (ν : Ω → Measure X)
    (hν : ∀ ω, (ν ω).Regular)
    (hopen : ∀ U : Set X, IsOpen U → Measurable (fun ω => ν ω U)) : Measurable ν := by
…

theorem OAI.SLEExactGauge.measurable_radon_of_tests line 115

Source documentation

A reconstruction with measurable compact-test integrals is a genuine measurable measure-valued map, not only a collection of scalar tests.

theorem measurable_radon_of_tests
    {Ω : Type*} [MeasurableSpace Ω] (ν : Ω → Measure X)
    (hν : ∀ ω, (ν ω).Regular)
    (htest : ∀ f : C_c(X, ℝ), Measurable (fun ω => ∫ x, f x ∂ν ω)) : Measurable ν :=
…

theorem OAI.SLEExactGauge.measurable_radon_of_test_limits line 123

Source documentation

Pointwise convergence of measurable compact-test integrals provides measurability of the reconstructed Radon kernel.

theorem measurable_radon_of_test_limits
    {Ω : Type*} [MeasurableSpace Ω] (μ : ℕ → Ω → Measure X) (ν : Ω → Measure X)
    (hν : ∀ ω, (ν ω).Regular)
    (hmeas : ∀ n (f : C_c(X, ℝ)), Measurable (fun ω => ∫ x, f x ∂μ n ω))
    (hlim : ∀ ω (f : C_c(X, ℝ)), Tendsto (fun n => ∫ x, f x ∂μ n ω)
      atTop (𝓝 (∫ x, f x ∂ν ω))) : Measurable ν := by
…