OAI/Analysis/FiniteFactor/Coupling/Marginals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.withDensity_finite_sum line 10
2. theorem OAI.FiniteFactor.mixture_withDensity line 18
3. def OAI.FiniteFactor.CouplingParameters.endpoint line 46
4. theorem OAI.FiniteFactor.CouplingParameters.endpoint_measurable line 48
5. theorem OAI.FiniteFactor.CouplingParameters.endpointComponentDensity_measurable line 53
6. theorem OAI.FiniteFactor.CouplingParameters.coupling_eq_sum line 57
7. theorem OAI.FiniteFactor.CouplingParameters.pairComponentLaw_endpoint line 66
8. theorem OAI.FiniteFactor.CouplingParameters.coupling_endpoint_density line 82

   Source documentation

   Identification of the actual pair law's two endpoint densities.

   theorem coupling_endpoint_density (right : Bool) :
       p.coupling.map (endpoint right) =
         unitIntervalMeasure.withDensity (fun t => ENNReal.ofReal (p.endpointDensity right t)) := by
   …

   Mentions: OAI.FiniteFactor.CouplingParameters.endpoint