OAI/Analysis/FiniteFactor/Coupling/FiniteDisintegration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.CouplingParameters.mixedPosteriorKernel line 12

   Source documentation

   The mixed posterior keeps every unselected coordinate fixed.

   def mixedPosteriorKernel {ι : Type*} (p : ι → CouplingParameters) (r : ι → Bool) :
       Kernel (ι → ℝ) (ι → ℝ) := by
   …

   Mentions: OAI.FiniteFactor.CouplingParameters

2. instance OAI.FiniteFactor.CouplingParameters.mixedPosteriorKernel_markov line 18
3. theorem OAI.FiniteFactor.CouplingParameters.mixedCoordinate_compProd line 25
4. theorem OAI.FiniteFactor.CouplingParameters.mixedPosterior_disintegration line 43

   Source documentation

   Disintegration of every mixed endpoint pair under the actual augmented product law, conditioned on the entire original x vector.

   theorem mixedPosterior_disintegration {ι : Type*} (p : ι → CouplingParameters) (r : ι → Bool) :
       ((vectorCoupling p).map (vectorEndpoint (fun _ => false))) ⊗ₘ (mixedPosteriorKernel p r) =
         (vectorCoupling p).map (fun ω => (vectorEndpoint (fun _ => false) ω,vectorEndpoint r ω)) := by
   …

   Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.vectorCoupling, OAI.FiniteFactor.CouplingParameters.vectorEndpoint, OAI.FiniteFactor.CouplingParameters.mixedPosteriorKernel