OAI/Probability/GammaPassage/BKBitLaw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.gammaDyadicRankCell line 13
2. lemma OAI.GammaFPP.measurableSet_gammaDyadicRankCell line 17
3. lemma OAI.GammaFPP.gammaDyadicRankCell_disjoint line 29
4. lemma OAI.GammaFPP.GammaEnvironment.gammaDyadicRankCell_real line 37
5. theorem OAI.GammaFPP.GammaEnvironment.gammaDyadicRankCells_real line 50

   Source documentation

   Uniform bit-cube probabilities, obtained from the actual Gamma edge law through an exact disjoint partition into dyadic rank cells.

   theorem GammaEnvironment.gammaDyadicRankCells_real (h : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate)
       (S : Finset Edge) (t : ℕ) (A : Finset (Finset (Edge × Fin t)))
       (hA : A ⊆ (S ×ˢ Finset.univ).powerset) :
       P.real (⋃ x ∈ A, gammaDyadicRankCell shape rate τ S t x) = fairFamilyMass (S ×ˢ Finset.univ) A := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaDyadicRankCell

6. theorem OAI.GammaFPP.GammaEnvironment.ae_gammaDyadicRankCell line 70

   Source documentation

   Every original environment lies in one of the bit cells almost surely. Coverage follows from exact mass one, so no choice of a binary expansion on null endpoint configurations is needed.

   theorem GammaEnvironment.ae_gammaDyadicRankCell (h : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate)
       (S : Finset Edge) (t : ℕ) :
       ∀ᵐ ω ∂P, ∃ x ∈ (S ×ˢ (Finset.univ : Finset (Fin t))).powerset, ω ∈ gammaDyadicRankCell shape rate τ S t x := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaDyadicRankCell