Content.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

Compact dimension contents, their finite measures, and positive support.

structure OAI.Kaplansky.PositiveDimensionFunctional line 24
Source documentation
The elementary dimension properties used to construct a compact content. This is an auxiliary interface, not a quasitrace or a linearity assumption.
```
structure PositiveDimensionFunctional (X : Type*) [TopologicalSpace X] where
…
```
def OAI.Kaplansky.PositiveDimensionFunctional.majorants line 35
Source documentation
Continuous nonnegative functions majorizing one on the compact set.
```
def majorants (K : Compacts X) : Set C(X, ℝ) := {f | 0 ≤ f ∧ ∀ x ∈ K, 1 ≤ f x}
```
def OAI.Kaplansky.PositiveDimensionFunctional.compactValue line 37
theorem OAI.Kaplansky.PositiveDimensionFunctional.majorants_nonempty line 39
theorem OAI.Kaplansky.PositiveDimensionFunctional.majorant_values_bddBelow line 42
theorem OAI.Kaplansky.PositiveDimensionFunctional.compactValue_nonneg line 47
theorem OAI.Kaplansky.PositiveDimensionFunctional.compactValue_le line 52
theorem OAI.Kaplansky.PositiveDimensionFunctional.le_compactValue line 55
theorem OAI.Kaplansky.PositiveDimensionFunctional.compactValue_le_one line 61
theorem OAI.Kaplansky.PositiveDimensionFunctional.compactValue_mono line 64
theorem OAI.Kaplansky.PositiveDimensionFunctional.compactValue_sup_le line 70

theorem OAI.Kaplansky.exists_disjoint_compact_cutoffs line 101

Source documentation

Disjoint closed sets admit nonnegative continuous cutoffs with disjoint supports and sum at most one.

theorem exists_disjoint_compact_cutoffs {X : Type*} [TopologicalSpace X] [NormalSpace X]
    (K L : Set X) (hK : IsClosed K) (hL : IsClosed L) (hKL : Disjoint K L) :
    ∃ u v : C(X, ℝ), 0 ≤ u ∧ 0 ≤ v ∧ u+v ≤ 1 ∧ u*v=0 ∧
      (∀ x ∈ K, u x=1) ∧ (∀ x ∈ L, v x=1) := by
…

theorem OAI.Kaplansky.PositiveDimensionFunctional.compactValue_sup_disjoint line 146
def OAI.Kaplansky.PositiveDimensionFunctional.content line 182
Source documentation
An actual compact content obtained by infima of positive dimension values.
```
def content : MeasureTheory.Content X where
…
```
theorem OAI.Kaplansky.PositiveDimensionFunctional.content_toReal line 188
def OAI.Kaplansky.PositiveDimensionFunctional.measure line 208
Source documentation
The Borel measure furnished by the proved compact content.
```
def measure : Measure X := D.content.measure
```
theorem OAI.Kaplansky.PositiveDimensionFunctional.measure_open line 210
theorem OAI.Kaplansky.PositiveDimensionFunctional.measure_open_eq_sup line 214
theorem OAI.Kaplansky.PositiveDimensionFunctional.content_le_one line 219
theorem OAI.Kaplansky.PositiveDimensionFunctional.measure_univ_le line 224
instance OAI.Kaplansky.PositiveDimensionFunctional.measure_isFiniteMeasure line 229
theorem OAI.Kaplansky.PositiveDimensionFunctional.zero_value line 246
theorem OAI.Kaplansky.PositiveDimensionFunctional.compactValue_empty line 251
def OAI.Kaplansky.PositiveDimensionFunctional.ScaleInvariant line 257
Source documentation
Positive scalar invariance is a dimension property, not spectral homogeneity.
```
def ScaleInvariant : Prop := ∀ (f : C(X, ℝ)), 0 ≤ f → ∀ r : ℝ, 0 < r →
…
```
theorem OAI.Kaplansky.PositiveDimensionFunctional.compactValue_le_of_pos line 260

theorem OAI.Kaplansky.PositiveDimensionFunctional.value_le_compactValue_of_support line 283

Source documentation

A function vanishing off K has dimension at most the compact content of K.

theorem value_le_compactValue_of_support (hscale : D.ScaleInvariant) (K : Compacts X)
    (f : C(X, ℝ)) (hf : 0 ≤ f) (hs : ∀ x, x ∉ K → f x=0) :
    D.toFun f ≤ D.compactValue K := by
…

def OAI.Kaplansky.continuousDimensionCutoff line 315
Source documentation
Continuous scalar cutoff, used only for uniform approximation of functions.
```
def continuousDimensionCutoff {X : Type*} [TopologicalSpace X] (f : C(X, ℝ)) (t : ℝ) : C(X, ℝ) :=
…
```
theorem OAI.Kaplansky.continuousDimensionCutoff_nonneg line 318
theorem OAI.Kaplansky.continuousDimensionCutoff_zero line 321
def OAI.Kaplansky.PositiveDimensionFunctional.ConeLowerSemicontinuous line 331
Source documentation
Lower semicontinuity is required only on the nonnegative cone.
```
def ConeLowerSemicontinuous : Prop :=
…
```
theorem OAI.Kaplansky.PositiveDimensionFunctional.exists_positive_cutoff line 334
theorem OAI.Kaplansky.PositiveDimensionFunctional.measure_positive_support line 358
Source documentation
The finite measure represents dimension on every positive support. The proof uses genuine compact contents and lower semicontinuity, not an assumed measure representation or finite-spectrum approximation.
```
theorem measure_positive_support (hscale : D.ScaleInvariant) (hsc : D.ConeLowerSemicontinuous)
    (f : C(X, ℝ)) (hf : 0 ≤ f) :
    D.measure {x | 0 < f x} = ENNReal.ofReal (D.toFun f) := by
…
```