DisjointSquares.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.sqrt_sum_disjoint_squares line 16

Source documentation

Disjoint nonnegative summands allow the square root of a weighted sum of squares to be written without any nonsmooth square-root composition.

theorem sqrt_sum_disjoint_squares {ι : Type uIndex} {X : Type uX} (s : Finset ι)
    (a : ι → ℝ) (g : ι → X → ℝ)
    (ha : ∀ i ∈ s, 0 ≤ a i)
    (hg : ∀ i ∈ s, ∀ x, 0 ≤ g i x)
    (hd : ∀ i ∈ s, ∀ j ∈ s, i ≠ j →
      Disjoint (Function.support (g i)) (Function.support (g j)))
    (x : X) :
    Real.sqrt (∑ i ∈ s, a i * (g i x) ^ 2) =
      ∑ i ∈ s, Real.sqrt (a i) * g i x := by
…

theorem OAI.Problem356.isSmoothCompactProbabilityDensity_sum_disjoint_squares line 52

Source documentation

A finite disjoint family of smooth compactly supported nonnegative square roots yields a density satisfying both smoothness requirements of the target.

theorem isSmoothCompactProbabilityDensity_sum_disjoint_squares {ι : Type uIndex}
    (s : Finset ι) (a : ι → ℝ) (g : ι → E3 → ℝ)
    (ha : ∀ i ∈ s, 0 ≤ a i)
    (hg : ∀ i ∈ s, ∀ x, 0 ≤ g i x)
    (hsm : ∀ i ∈ s, ContDiff ℝ (↑(⊤ : ENat) : WithTop ENat) (g i))
    (hcs : ∀ i ∈ s, HasCompactSupport (g i))
    (hd : ∀ i ∈ s, ∀ j ∈ s, i ≠ j →
      Disjoint (Function.support (g i)) (Function.support (g j)))
    (hmass : (∫ x : E3, (∑ i ∈ s, a i * (g i x) ^ 2)
      ∂(volume : Measure E3)) = 1) :
    IsSmoothCompactProbabilityDensity (fun x => ∑ i ∈ s, a i * (g i x) ^ 2) := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.IsSmoothCompactProbabilityDensity

theorem OAI.Problem356.isSmoothCompactProbabilityDensity_sum_normalized_disjoint_squares line 87

Source documentation

Convenient normalization form for the five component densities: every square has unit mass, and the component weights sum to one.

theorem isSmoothCompactProbabilityDensity_sum_normalized_disjoint_squares
    {ι : Type uIndex} (s : Finset ι) (a : ι → ℝ) (g : ι → E3 → ℝ)
    (ha : ∀ i ∈ s, 0 ≤ a i)
    (hg : ∀ i ∈ s, ∀ x, 0 ≤ g i x)
    (hsm : ∀ i ∈ s, ContDiff ℝ (↑(⊤ : ENat) : WithTop ENat) (g i))
    (hcs : ∀ i ∈ s, HasCompactSupport (g i))
    (hd : ∀ i ∈ s, ∀ j ∈ s, i ≠ j →
      Disjoint (Function.support (g i)) (Function.support (g j)))
    (hgint : ∀ i ∈ s, (∫ x : E3, (g i x) ^ 2 ∂(volume : Measure E3)) = 1)
    (haint : (∑ i ∈ s, a i) = 1) :
    IsSmoothCompactProbabilityDensity (fun x => ∑ i ∈ s, a i * (g i x) ^ 2) := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.IsSmoothCompactProbabilityDensity

theorem OAI.Problem356.densityMeasure_sum_weighted_squares line 117

Source documentation

The density assembled from weighted squares represents the corresponding finite mixture of component measures. No disjointness is needed here.

theorem densityMeasure_sum_weighted_squares {ι : Type uIndex}
    (s : Finset ι) (a : ι → ℝ) (g : ι → E3 → ℝ)
    (ha : ∀ i ∈ s, 0 ≤ a i)
    (hgm : ∀ i ∈ s, Measurable (g i)) :
    densityMeasure (fun x => ∑ i ∈ s, a i * (g i x) ^ 2) =
      ∑ i ∈ s, ENNReal.ofReal (a i) • densityMeasure (fun x => (g i x) ^ 2) := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.densityMeasure