OAI/Analysis/FiniteFactor/CrossedProduct/ReferenceMixture.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceResamplingKernel line 11
2. instance OAI.FiniteFactor.sourceResamplingKernel_markov line 19
3. theorem OAI.FiniteFactor.sourceResamplingKernel_apply line 24
4. theorem OAI.FiniteFactor.sourceFiniteReferenceKernel_apply line 32
5. theorem OAI.FiniteFactor.sourceFiniteReferenceKernel_mixture line 45

   Source documentation

   The exact finite replacement-pattern expansion of the reference kernel.

   theorem sourceFiniteReferenceKernel_mixture (F : Finset SourceCoordinate) (x : SourceCoordinate → ℝ) :
       sourceFiniteReferenceKernel F x = ((2 : ℝ≥0∞)⁻¹)^F.card •
         ∑ I ∈ F.powerset, sourceResamplingKernel I x := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceFiniteReferenceKernel, OAI.FiniteFactor.sourceResamplingKernel

6. theorem OAI.FiniteFactor.sourceFiniteReference_compProd_mixture line 52

   Source documentation

   Integrating over the actual Haar base preserves the finite mixture formula.

   theorem sourceFiniteReference_compProd_mixture (F : Finset SourceCoordinate) :
       sourceSamplingHaar ⊗ₘ sourceFiniteReferenceKernel F =
         ((2 : ℝ≥0∞)⁻¹)^F.card •
           ∑ I ∈ F.powerset, sourceSamplingHaar ⊗ₘ sourceResamplingKernel I := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.sourceFiniteReferenceKernel, OAI.FiniteFactor.sourceResamplingKernel