RadonTestFamily.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A countable determining family on a second-countable locally compact space, constructed from compact exhaustion and separability on compacts.

theorem OAI.SLEExactGauge.exists_compact_test_sequence line 22

Source documentation

Compact support in a fixed compact set admits a countable uniformly dense family, with the same support constraint.

theorem exists_compact_test_sequence (K : Set X) (hK : IsCompact K) :
    ∃ f : ℕ → C_c(X, ℝ), (∀ j, tsupport (f j) ⊆ K) ∧
      ∀ g : C_c(X, ℝ), tsupport g ⊆ K → ∀ ε : ℝ, 0 < ε →
        ∃ j, ∀ x, |g x-f j x| ≤ ε := by
…

theorem OAI.SLEExactGauge.exists_compact_test_cutoff line 57
Source documentation
One nonnegative compactly supported cutoff dominates one on a given compact set.
```
theorem exists_compact_test_cutoff (K : Set X) (hK : IsCompact K) :
    ∃ f : C_c(X, ℝ), (∀ x, 0 ≤ f x) ∧ ∀ x ∈ K, 1 ≤ f x := by
…
```
theorem OAI.SLEExactGauge.exists_localTestFamily line 68
Source documentation
The determining family required by Radon reconstruction exists without an additional density or cutoff hypothesis.
```
theorem exists_localTestFamily : Nonempty (LocalTestFamily X) := by
…
```
Mentions: OAI.SLEExactGauge.LocalTestFamily
def OAI.SLEExactGauge.localTestFamily line 110
Source documentation
A chosen countable family can be used for all times and all random outcomes of a measure-valued construction.
```
def localTestFamily (X : Type*) [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X]
    [SecondCountableTopology X] : LocalTestFamily X :=
…
```
Mentions: OAI.SLEExactGauge.LocalTestFamily