OAI/Analysis/FiniteFactor/Coupling/Bayes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.CouplingParameters.endpointDensity_measurable line 14
2. theorem OAI.FiniteFactor.CouplingParameters.posteriorMass_measurable line 18
3. def OAI.FiniteFactor.CouplingParameters.posteriorKernel line 23
4. instance OAI.FiniteFactor.CouplingParameters.posteriorKernel_markov line 35
5. theorem OAI.FiniteFactor.CouplingParameters.posteriorLaw_weighted line 38
6. theorem OAI.FiniteFactor.CouplingParameters.coupling_rectangle line 55
7. theorem OAI.FiniteFactor.CouplingParameters.posterior_rectangle_integral line 69

   Source documentation

   The posterior formula satisfies the defining conditional-law identity on all measurable rectangles, in either endpoint orientation.

   theorem posterior_rectangle_integral (right : Bool) {A B : Set ℝ}
       (hA : MeasurableSet A) (hB : MeasurableSet B) :
       (∫⁻ t in A, p.posteriorLaw right t B ∂(p.coupling.map (endpoint right))) =
         ENNReal.ofReal p.diagonalMass * unitIntervalMeasure (A ∩ B) +
           ∑ i, ENNReal.ofReal (p.replacementMass i) *
             p.endpointComponentLaw right i A * p.endpointComponentLaw (!right) i B := by
   …

   Mentions: OAI.FiniteFactor.CouplingParameters.endpoint, OAI.FiniteFactor.unitIntervalMeasure

8. theorem OAI.FiniteFactor.CouplingParameters.conditional_given_x line 109

   Source documentation

   Genuine forward disintegration of the constructed coupling.

   theorem conditional_given_x {A B : Set ℝ} (hA : MeasurableSet A) (hB : MeasurableSet B) :
       (∫⁻ t in A, p.posteriorKernel false t B ∂(p.coupling.map Prod.fst)) = p.coupling (A ×ˢ B) := by
   …

9. theorem OAI.FiniteFactor.CouplingParameters.conditional_given_y line 115

   Source documentation

   Genuine reverse disintegration of the same coupling.

   theorem conditional_given_y {A B : Set ℝ} (hA : MeasurableSet A) (hB : MeasurableSet B) :
       (∫⁻ t in A, p.posteriorKernel true t B ∂(p.coupling.map Prod.snd)) = p.coupling (B ×ˢ A) := by
   …