Finite mixtures of ensembles
DefinitionEnsembleSpaceDraft_finiteMixtureDefinition 1.10 associates to finitely many ensembles and coefficients with a single ensemble, the finite mixture .
Coefficients equal to zero are deleted and the remaining pairs keep their order. If one pair remains, the mixture is . If several remain, with first pair and with the sum of the later coefficients, the mixture is
where is the finite mixture of the later ensembles with coefficients divided by . This is the bracketing written as (1.11) in the draft.
The same value is defined for a list of real coefficients and ensembles, and for a finite index set presented as Fin n.
Formalization Note. The operation is partial. It returns no ensemble if every coefficient is zero, or if a tail of the list sums to zero. Corollary 1.12 states that a value does exist when the coefficients lie in and sum to . While a tail is rescaled, each new coefficient is passed through the projection of onto . For nonnegative summands that projection is the identity on the ratios that arise from a positive tail sum.
import Definitions.Def_EnsembleSpaceDraft_axioms
import Mathlib
/-!
# Finite mixtures (Definition 1.10)
The nested expression (1.11) is realized by dropping coefficients equal to `0` and then
folding binary mixes from the left. A coefficient known only as a real number is sent
through `Set.projIcc`, which is the identity on `[0, 1]`. If the filtered list is empty,
or a partial sum of a tail vanishes, the function returns `none`.
-/
open scoped unitInterval
namespace EnsembleSpaceDraft
universe u
variable {E : Type u} [TopologicalSpace E]
/-- Left-nested mixture of a list whose coefficients are intended to be strictly positive.
Returns `none` on the empty list and when a tail sums to zero. -/
noncomputable def nestMixture? (X : EnsembleSpace E) : List (ℝ × E) → Option E
| [] => none
| (p, e) :: t =>
if t = [] then some e
else
let s := (t.map Prod.fst).sum
if s = 0 then none
else
(nestMixture? X (t.map fun pe => (pe.1 / s, pe.2))).map fun tail =>
X.mix (Set.projIcc (0 : ℝ) 1 zero_le_one p) e tail
termination_by l => l.length
decreasing_by
simp_wf
/-- Definition 1.10. Zero coefficients are dropped, preserving order; the remaining list
is mixed by (1.11). Returns `none` if every coefficient is zero. -/
noncomputable def finiteMixtureList? (X : EnsembleSpace E) (l : List (ℝ × E)) : Option E :=
nestMixture? X (l.filter fun pe => pe.1 ≠ 0)
/-- Definition 1.10, indexed by `Fin n`. -/
noncomputable def finiteMixture {n : ℕ} (X : EnsembleSpace E) (p : Fin n → ℝ) (e : Fin n → E) :
Option E :=
finiteMixtureList? X (List.ofFn fun i => (p i, e i))
end EnsembleSpaceDraft
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.