OAI/Probability/GammaPassage/DyadicRanks.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.dyadicPositions line 11

   Source documentation

   Positions of the zero bits, numbered from the least significant end.

   noncomputable def dyadicPositions (t : ℕ) (x : Finset (Edge × Fin t)) (e : Edge) : Finset ℕ :=
   …

2. def OAI.GammaFPP.dyadicRank line 14
3. lemma OAI.GammaFPP.dyadicPositions_subset line 17
4. lemma OAI.GammaFPP.mem_dyadicPositions line 25
5. lemma OAI.GammaFPP.sum_two_powers_range line 36
6. lemma OAI.GammaFPP.dyadicRank_lt line 41
7. lemma OAI.GammaFPP.dyadicRank_eq_iff line 49
8. lemma OAI.GammaFPP.dyadicRanks_injective line 66