Uniform.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.UniformSource.probability line 15
Source documentation
Normalization of a compact body with nonempty interior gives a probability measure.
```
theorem probability (hK : IsCompact K) (hinterior : (interior K).Nonempty) :
    IsProbabilityMeasure (uniformMeasure K) := by
…
```
theorem OAI.Problem358.UniformSource.supported line 22
theorem OAI.Problem358.UniformSource.ae_mem line 25
theorem OAI.Problem358.UniformSource.integrable_continuousOn line 30
Source documentation
Continuous functions on a compact source are integrable after normalization, including the zero-volume case.
```
theorem integrable_continuousOn {F : Type*} [NormedAddCommGroup F]
    (hK : IsCompact K) {f : E d → F} (hf : ContinuousOn f K) :
    Integrable f (uniformMeasure K) := by
…
```
theorem OAI.Problem358.UniformSource.integrable_norm line 40
theorem OAI.Problem358.UniformSource.integrable_norm_pow line 44
theorem OAI.Problem358.UniformSource.exists_ae_norm_bound line 48

theorem OAI.Problem358.isProbabilityMeasure_uniformMeasure_of_volume line 60

Source documentation

Normalizing a set of strictly positive finite volume gives a probability source.

theorem isProbabilityMeasure_uniformMeasure_of_volume {d : ℕ} {K : Set (E d)}
    (hpos : 0 < volume K) (hfinite : volume K ≠ ∞) :
    IsProbabilityMeasure (uniformMeasure K) := by
…

theorem OAI.Problem358.isProbabilityMeasure_uniformMeasure_of_compact line 69

Source documentation

The source hypotheses in the qualified stability theorem guarantee normalization.

theorem isProbabilityMeasure_uniformMeasure_of_compact {d : ℕ} {K : Set (E d)}
    (hK : IsCompact K) (hKi : (interior K).Nonempty) :
    IsProbabilityMeasure (uniformMeasure K) :=
…

theorem OAI.Problem358.uniformMeasure_absolutelyContinuous line 88
Source documentation
Every uniform source is absolutely continuous with respect to ambient volume, without any measurability, finiteness, or nondegeneracy assumptions on its set.
```
theorem uniformMeasure_absolutelyContinuous {d : ℕ} (K : Set (E d)) :
    uniformMeasure K ≪ volume := by
…
```
theorem OAI.Problem358.uniformMeasure_null_of_volume_null line 94
Source documentation
A volume-null exceptional set is null for any uniform source.
```
theorem uniformMeasure_null_of_volume_null {d : ℕ} (K : Set (E d))
    {N : Set (E d)} (hN : volume N = 0) : uniformMeasure K N = 0 :=
…
```

theorem OAI.Problem358.uniformMeasure_affineSubspace line 99

Source documentation

A proper affine subspace is null for any uniform source.

theorem uniformMeasure_affineSubspace {d : ℕ} (K : Set (E d))
    (A : AffineSubspace ℝ (E d)) (hA : A ≠ ⊤) :
    uniformMeasure K (A : Set (E d)) = 0 :=
…

def OAI.Problem358.innerLevelSubspace line 105
Source documentation
A level set of a real scalar product is an affine subspace.
```
def innerLevelSubspace {d : ℕ} (a : E d) (b : ℝ) : AffineSubspace ℝ (E d) where
…
```
theorem OAI.Problem358.innerLevelSubspace_ne_top line 117
Source documentation
A hyperplane with nonzero normal is a proper affine subspace.
```
theorem innerLevelSubspace_ne_top {d : ℕ} {a : E d} (ha : a ≠ 0) (b : ℝ) :
    innerLevelSubspace a b ≠ ⊤ := by
…
```
Mentions: OAI.Problem358.innerLevelSubspace
theorem OAI.Problem358.volume_inner_level line 129
Source documentation
Every nontrivial real scalar-product level set is volume-null.
```
theorem volume_inner_level {d : ℕ} {a : E d} (ha : a ≠ 0) (b : ℝ) :
    volume {x : E d | inner ℝ a x = b} = 0 := by
…
```

theorem OAI.Problem358.uniformMeasure_inner_level line 135

Source documentation

Every nontrivial real scalar-product level set is uniform-source-null.

theorem uniformMeasure_inner_level {d : ℕ} (K : Set (E d))
    {a : E d} (ha : a ≠ 0) (b : ℝ) :
    uniformMeasure K {x : E d | inner ℝ a x = b} = 0 :=
…

theorem OAI.Problem358.uniformMeasure_affine_tie line 141

Source documentation

The tie set of two affine functions with distinct slopes is null.

theorem uniformMeasure_affine_tie {d : ℕ} (K : Set (E d))
    {y z : E d} (hyz : y ≠ z) (c e : ℝ) :
    uniformMeasure K {x : E d | inner ℝ y x + c = inner ℝ z x + e} = 0 := by
…

theorem OAI.Problem358.ae_affine_eq_imp_slope_eq line 153

Source documentation

Outside a null set, equal values of two affine functions mean equal slopes.

theorem ae_affine_eq_imp_slope_eq {d : ℕ} (K : Set (E d))
    (y z : E d) (c e : ℝ) :
    ∀ᵐ x ∂uniformMeasure K, inner ℝ y x + c = inner ℝ z x + e → y = z := by
…

theorem OAI.Problem358.ae_all_affine_eq_imp_slope_eq line 166

Source documentation

A countable family of affine functions has no ties between distinct slopes at almost every source point. In particular this applies to finite maxima.

theorem ae_all_affine_eq_imp_slope_eq {d : ℕ} {ι : Type*} [Countable ι]
    (K : Set (E d)) (y : ι → E d) (c : ι → ℝ) :
    ∀ᵐ x ∂uniformMeasure K, ∀ i j,
      inner ℝ (y i) x + c i = inner ℝ (y j) x + c j → y i = y j := by
…

theorem OAI.Problem358.uniformMeasure_frontier_convex line 175

Source documentation

The boundary of a convex set is null under every uniform source.

theorem uniformMeasure_frontier_convex {d : ℕ} (K : Set (E d))
    {S : Set (E d)} (hS : Convex ℝ S) :
    uniformMeasure K (frontier S) = 0 :=
…

theorem OAI.Problem358.uniformMeasure_univ_le_one line 181
Source documentation
Normalization always has total mass at most one, even for degenerate sets.
```
theorem uniformMeasure_univ_le_one {d : ℕ} (K : Set (E d)) :
    uniformMeasure K Set.univ ≤ 1 := by
…
```
theorem OAI.Problem358.uniformMeasure_finite line 187
Source documentation
Every normalized restriction is a finite measure, including zero/infinite-volume sets.
```
theorem uniformMeasure_finite {d : ℕ} (K : Set (E d)) :
    IsFiniteMeasure (uniformMeasure K) :=
…
```

theorem OAI.Problem358.UniformSource.subset_support line 202

Source documentation

The topological support of normalized volume on a convex body is the whole body.

theorem subset_support {d : ℕ} {K : Set (E d)} (hK : IsCompact K)
    (hconv : Convex ℝ K) (hne : (interior K).Nonempty) :
    K ⊆ (uniformMeasure K).support := by
…

theorem OAI.Problem358.UniformSource.support_eq line 220