DensityMixture.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.densityMeasure_const_mul line 14
Source documentation
The nonnegative real-density constructor respects finite scalar multiples.
```
theorem densityMeasure_const_mul {a : ℝ} (ha : 0 ≤ a) (rho : E3 → ℝ) :
    densityMeasure (fun x => a * rho x) = ENNReal.ofReal a • densityMeasure rho := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.densityMeasure

theorem OAI.Problem356.densityMeasure_add line 21

Source documentation

The real density constructor is additive on nonnegative densities.

theorem densityMeasure_add {rho sigma : E3 → ℝ}
    (hrho : ∀ x, 0 ≤ rho x) (hsigma : ∀ x, 0 ≤ sigma x)
    (hm : Measurable rho) :
    densityMeasure (fun x => rho x + sigma x) =
      densityMeasure rho + densityMeasure sigma := by
…

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

theorem OAI.Problem356.densityMeasure_finset_mixture line 32

Source documentation

Finite nonnegative density mixtures agree with mixtures of the induced measures. This identifies the smooth marginal with the branch-plan marginal.

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

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

theorem OAI.Problem356.densityMeasure_fintype_mixture line 57

Source documentation

Fintype form of the density-mixture identity.

theorem densityMeasure_fintype_mixture {ι : Type uIndex} [Fintype ι]
    (a : ι → ℝ) (rho : ι → E3 → ℝ)
    (ha : ∀ i, 0 ≤ a i) (hrho : ∀ i x, 0 ≤ rho i x)
    (hm : ∀ i, Measurable (rho i)) :
    densityMeasure (fun x => ∑ i, a i * rho i x) =
      ∑ i, ENNReal.ofReal (a i) • densityMeasure (rho i) := by
…

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

theorem OAI.Problem356.densityMeasure_five_component_mixture line 66