DensityMeasure.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.densityMeasure_absolutelyContinuous line 13
Source documentation
Every measure obtained from a density is absolutely continuous with respect to volume.
```
theorem densityMeasure_absolutelyContinuous (rho : E3 → ℝ) :
    densityMeasure rho ≪ (volume : Measure E3) :=
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.densityMeasure
instance OAI.Problem356.densityMeasure_nullSingletonClass line 18
Source documentation
A density measure has no point atoms, without any regularity assumption on the density.
```
instance densityMeasure_nullSingletonClass (rho : E3 → ℝ) :
    NullSingletonClass (densityMeasure rho) := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.densityMeasure
theorem OAI.Problem356.densityMeasure_tsupport_compl line 24
Source documentation
A density measure gives no mass to the complement of its topological support.
```
theorem densityMeasure_tsupport_compl (rho : E3 → ℝ) :
    densityMeasure rho (tsupport rho)ᶜ = 0 := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.densityMeasure
theorem OAI.Problem356.densityMeasure_exists_compact_conull line 33
Source documentation
Compact support of the density provides an explicit compact set of full measure.
```
theorem densityMeasure_exists_compact_conull {rho : E3 → ℝ}
    (hrho : HasCompactSupport rho) :
    ∃ K : Set E3, IsCompact K ∧ densityMeasure rho Kᶜ = 0 :=
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.densityMeasure