SplitMeasure.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Measure identities for the five-component splitting construction.

theorem OAI.Problem356.Splitting.measure_eq_zero_of_disjoint line 20
Source documentation
A measure supported almost everywhere on B vanishes on any set disjoint from B.
```
theorem measure_eq_zero_of_disjoint
    (ν : Measure α) {B S : Set α}
    (hν : ∀ᵐ x ∂ν, x ∈ B) (hBS : Disjoint B S) : ν S = 0 := by
…
```

theorem OAI.Problem356.Splitting.map_eq_zero_of_disjoint line 29

Source documentation

A branch pushforward vanishes away from the image of the central component.

theorem map_eq_zero_of_disjoint
    (ν : Measure α) {B S : Set α} {H : α → α}
    (hν : ∀ᵐ x ∂ν, x ∈ B) (hH : Measurable H)
    (hS : MeasurableSet S) (hBS : Disjoint (H '' B) S) :
    (Measure.map H ν) S = 0 := by
…

theorem OAI.Problem356.Splitting.map_image_eq line 40

Source documentation

An injective branch has the original mass on the image of each central subset.

theorem map_image_eq
    (ν : Measure α) {B S : Set α} {H : α → α}
    (hν : ∀ᵐ x ∂ν, x ∈ B) (hH : Measurable H)
    (hInj : Set.InjOn H B) (hSB : S ⊆ B)
    (hImage : MeasurableSet (H '' S)) :
    (Measure.map H ν) (H '' S) = ν S := by
…

def OAI.Problem356.Splitting.splitMeasure line 61
Source documentation
The central measure together with finitely many weighted branch pushforwards.
```
def splitMeasure (ν : Measure α) (a : ℝ≥0∞) (b : ι → ℝ≥0∞)
    (H : ι → α → α) : Measure α :=
…
```

theorem OAI.Problem356.Splitting.splitMeasure_isProbabilityMeasure line 66

Source documentation

Weights adding to one produce a probability measure.

theorem splitMeasure_isProbabilityMeasure
    (ν : Measure α) [IsProbabilityMeasure ν]
    (a : ℝ≥0∞) (b : ι → ℝ≥0∞) (H : ι → α → α)
    (hH : ∀ i, Measurable (H i)) (hweight : a + ∑ i, b i = 1) :
    IsProbabilityMeasure (splitMeasure ν a b H) := by
…

Mentions: OAI.Problem356.Splitting.splitMeasure

theorem OAI.Problem356.Splitting.absolutelyContinuous_splitMeasure line 81
Source documentation
A nonzero central coefficient transfers all almost-everywhere properties of the mixture to its central reference measure.
```
theorem absolutelyContinuous_splitMeasure
    (ν : Measure α) (a : ℝ≥0∞) (b : ι → ℝ≥0∞) (H : ι → α → α)
    (ha : a ≠ 0) : ν ≪ splitMeasure ν a b H := by
…
```
Mentions: OAI.Problem356.Splitting.splitMeasure

theorem OAI.Problem356.Splitting.splitMeasure_apply_central line 87

Source documentation

On the central component, only the central summand contributes.

theorem splitMeasure_apply_central
    (ν : Measure α) (a : ℝ≥0∞) (b : ι → ℝ≥0∞) (H : ι → α → α)
    {B S : Set α} (hν : ∀ᵐ x ∂ν, x ∈ B)
    (hH : ∀ i, Measurable (H i)) (hSB : S ⊆ B) (hS : MeasurableSet S)
    (hDisj : ∀ i, Disjoint B (H i '' B)) :
    splitMeasure ν a b H S = a * ν S := by
…

Mentions: OAI.Problem356.Splitting.splitMeasure

theorem OAI.Problem356.Splitting.splitMeasure_apply_image line 100

Source documentation

On one branch image only that branch summand contributes.

theorem splitMeasure_apply_image
    (ν : Measure α) (a : ℝ≥0∞) (b : ι → ℝ≥0∞) (H : ι → α → α)
    {B S : Set α} (hν : ∀ᵐ x ∂ν, x ∈ B)
    (hH : ∀ i, Measurable (H i)) (hInj : ∀ i, Set.InjOn (H i) B)
    (hSB : S ⊆ B) (hImage : ∀ i, MeasurableSet (H i '' S))
    (hCentral : ∀ i, Disjoint B (H i '' B))
    (hPair : Pairwise fun i j => Disjoint (H i '' B) (H j '' B)) (j : ι) :
    splitMeasure ν a b H (H j '' S) = b j * ν S := by
…

Mentions: OAI.Problem356.Splitting.splitMeasure