OAI/Analysis/FiniteFactor/FiniteProductMixture.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.finiteChoiceLaw line 14
2. instance OAI.FiniteFactor.finiteChoiceLaw_probability line 19
3. def OAI.FiniteFactor.finiteAverageLaw line 23
4. instance OAI.FiniteFactor.finiteAverageLaw_probability line 28
5. theorem OAI.FiniteFactor.finiteChoiceLaw_update_base line 32
6. theorem OAI.FiniteFactor.finiteChoiceLaw_update_replace line 42
7. theorem OAI.FiniteFactor.finiteAverageLaw_insert line 52
8. theorem OAI.FiniteFactor.coordinateUpdateLaw_smul_right line 65
9. theorem OAI.FiniteFactor.coordinateUpdateLaw_finset_sum line 72
10. theorem OAI.FiniteFactor.finiteAverageLaw_eq_sum line 83

    Source documentation

    The finite independent diagonal-or-replacement mixture is an exact finite sum of the laws for each replacement pattern.

    theorem finiteAverageLaw_eq_sum (μ ν : ι → Measure X)
        [∀ i, IsProbabilityMeasure (μ i)] [∀ i, IsProbabilityMeasure (ν i)] (F : Finset ι) :
        finiteAverageLaw μ ν F = ((2 : ℝ≥0∞)⁻¹)^F.card •
          ∑ I ∈ F.powerset, finiteChoiceLaw μ ν I := by
    …

    Mentions: OAI.FiniteFactor.finiteAverageLaw, OAI.FiniteFactor.finiteChoiceLaw