OAI/Analysis/FiniteFactor/FiniteMixtureAlgebra.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.probabilityAverage line 12

   Source documentation

   Equal-weight mixture of two probability measures.

   def probabilityAverage {X : Type*} [MeasurableSpace X] (μ ν : Measure X) : Measure X :=
   …

2. instance OAI.FiniteFactor.probabilityAverage_probability line 15
3. def OAI.FiniteFactor.coordinateUpdateLaw line 23

   Source documentation

   A single-coordinate update, as a linear operation on the remaining law.

   def coordinateUpdateLaw {ι X : Type*} [DecidableEq ι] [MeasurableSpace X]
       (i : ι) (μ : Measure X) (ν : Measure (ι → X)) : Measure (ι → X) :=
   …

4. theorem OAI.FiniteFactor.measurable_coordinateUpdate line 27
5. theorem OAI.FiniteFactor.coordinateUpdateLaw_add_right line 36
6. theorem OAI.FiniteFactor.coordinateUpdateLaw_average line 43