OAI/Analysis/FiniteFactor/BiasedPairs/PrefixDomination.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceBiasedRealMeasure_ordered line 11
2. theorem OAI.FiniteFactor.sourceBiasedPrefix_domination_real line 20
3. theorem OAI.FiniteFactor.sourceBiasedPrefix_domination line 30

   Source documentation

   Finite-prefix domination by the actual lambda_I measures on the same torus used for the uncapped invariant-projection identity and weak limits.

   theorem sourceBiasedPrefix_domination (j n : ℕ) :
       (sourceBiasedTorusMeasure j (sourceBiasedPrefixMask n) : Measure SourceSamplingTorus) ≪
         ∑ I ∈ (blockPrefix sourceBlockSize n).powerset,
           (sourceSamplingLambdaTorus I : Measure SourceSamplingTorus) := by
   …

   Mentions: OAI.FiniteFactor.sourceBiasedTorusMeasure, OAI.FiniteFactor.sourceBiasedPrefixMask, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.sourceSamplingLambdaTorus