OAI/Analysis/FiniteFactor/Coupling/Law.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.densityMeasure_probability line 13

   Source documentation

   A probability density gives an actual probability measure.

   theorem densityMeasure_probability {X : Type*} [MeasurableSpace X]
       {μ : Measure X} {d : X → ℝ} (hd : Integrable d μ)
       (h0 : ∀ x, 0 ≤ d x) (hm : ∫ x, d x ∂μ = 1) :
       IsProbabilityMeasure (μ.withDensity (fun x => ENNReal.ofReal (d x))) := by
   …

2. def OAI.FiniteFactor.CouplingParameters.endpointComponentLaw line 25
3. instance OAI.FiniteFactor.CouplingParameters.endpointComponentLaw_probability line 28
4. def OAI.FiniteFactor.CouplingParameters.labelMass line 37

   Source documentation

   Six labels: zero is diagonal; the five successors retain both widths and the tag.

   def labelMass : Fin 6 → ℝ := Fin.cons p.diagonalMass p.replacementMass

5. def OAI.FiniteFactor.CouplingParameters.pairComponentLaw line 39
6. theorem OAI.FiniteFactor.CouplingParameters.labelMass_nonneg line 43
7. theorem OAI.FiniteFactor.CouplingParameters.labelMass_sum line 46
8. instance OAI.FiniteFactor.CouplingParameters.pairComponentLaw_probability line 49
9. def OAI.FiniteFactor.CouplingParameters.labelledCoupling line 59

   Source documentation

   The actual augmented one-coordinate law, including its mixture label.

   def labelledCoupling : Measure (Fin 6 × (ℝ × ℝ)) :=
   …

10. instance OAI.FiniteFactor.CouplingParameters.labelledCoupling_probability line 63
11. def OAI.FiniteFactor.CouplingParameters.coupling line 75

    Source documentation

    Forgetting labels gives the one-coordinate pair law.

    def coupling : Measure (ℝ × ℝ) := p.labelledCoupling.map Prod.snd

12. instance OAI.FiniteFactor.CouplingParameters.coupling_probability line 77
13. theorem OAI.FiniteFactor.CouplingParameters.endpointComponentLaw_eq line 82
14. theorem OAI.FiniteFactor.CouplingParameters.endpointComponentLaw_of_contains line 93