OAI/Analysis/FiniteFactor/BiasedPairs/ReferenceDomination.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceDiagonalHaarKernel line 11
2. instance OAI.FiniteFactor.sourceDiagonalHaarKernel_markov line 19
3. def OAI.FiniteFactor.sourceFiniteReferenceKernel line 23

   Source documentation

   Independent diagonal-or-Haar replacement at a finite set of coordinates.

   def sourceFiniteReferenceKernel (F : Finset SourceCoordinate) :
       Kernel (SourceCoordinate → ℝ) (SourceCoordinate → ℝ) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate

4. instance OAI.FiniteFactor.sourceFiniteReferenceKernel_markov line 29
5. theorem OAI.FiniteFactor.sourceMixedPosterior_ac line 35

   Source documentation

   The mixed prefix posterior is dominated for every full conditioning vector.

   theorem sourceMixedPosterior_ac (j : ℕ) (F : Finset SourceCoordinate) (x : SourceCoordinate → ℝ) :
       mixedPosteriorKernel (fun i : SourceCoordinate => stagedCouplingParameters j i.1)
         (fun i => decide (i ∈ F)) x ≪ sourceFiniteReferenceKernel F x := by
   …

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

6. theorem OAI.FiniteFactor.sourceBiasedPrefix_ac_reference line 49

   Source documentation

   Actual prefix-pair domination after integrating the full x marginal. The x marginal is replaced by Haar only through its proved density, so the infinite diagonal tail is not assumed Haar-distributed.

   theorem sourceBiasedPrefix_ac_reference (j n : ℕ) :
       sourceBiasedRealMeasure j (sourceBiasedPrefixMask n) ≪
         sourceSamplingHaar ⊗ₘ sourceFiniteReferenceKernel (blockPrefix sourceBlockSize n) := by
   …

   Mentions: OAI.FiniteFactor.sourceBiasedRealMeasure, OAI.FiniteFactor.sourceBiasedPrefixMask, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.sourceFiniteReferenceKernel, OAI.FiniteFactor.sourceBlockSize