OAI/Analysis/FiniteFactor/Coupling/FiniteLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.CouplingParameters.selectedLaw line 11
2. instance OAI.FiniteFactor.CouplingParameters.selectedLaw_probability line 14
3. theorem OAI.FiniteFactor.CouplingParameters.selectedLaw_endpoint line 19
4. theorem OAI.FiniteFactor.CouplingParameters.selectedLaw_apply_integral line 23
5. theorem OAI.FiniteFactor.CouplingParameters.finiteProductLaw_density line 33

   Source documentation

   The actual finite product law has the product density with the established L2 bounds. This identifies measures on every measurable set.

   theorem finiteProductLaw_density {ι : Type*} [Fintype ι]
       (p : ι → CouplingParameters) (enabled right : ι → Bool) :
       Measure.pi (fun i => (p i).selectedLaw (enabled i) (right i)) =
         (Measure.pi (fun _ : ι => unitIntervalMeasure)).withDensity
           (fun x => ENNReal.ofReal (finiteProductDensity p enabled right x)) := by
   …

   Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.selectedLaw, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.CouplingParameters.finiteProductDensity