OAI/Geometry/HyperbolicGroups/SixCounts.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.SixTable.PairPositions line 18
2. instance OAI.HyperbolicObstruction.SixTable.(instance at line 19) line 19
3. lemma OAI.HyperbolicObstruction.SixTable.card_pairPositions line 21
4. def OAI.HyperbolicObstruction.SixTable.pairTrials line 23
5. lemma OAI.HyperbolicObstruction.SixTable.mem_pairTrials line 27
6. lemma OAI.HyperbolicObstruction.SixTable.card_pairTrials line 32
7. def OAI.HyperbolicObstruction.SixTable.count line 37
8. def OAI.HyperbolicObstruction.SixTable.probability line 40
9. lemma OAI.HyperbolicObstruction.SixTable.probability_mem line 43
10. def OAI.HyperbolicObstruction.SixTable.law line 51
11. lemma OAI.HyperbolicObstruction.SixTable.pair_mean line 54
12. lemma OAI.HyperbolicObstruction.SixTable.centered_eq line 62
13. lemma OAI.HyperbolicObstruction.SixTable.count_chernoff line 67
14. abbrev OAI.HyperbolicObstruction.SixTable.BadPairs line 76
15. theorem OAI.HyperbolicObstruction.SixTable.badPairs_bound line 82

    Source documentation

    Simultaneous control of all ordered pairs in the actual single six-letter array. No independence of different pair counts is used.

    theorem badPairs_bound {δ ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 < ε) (hε2 : ε ≤ 2) :
        (law (A := A) δ hδ).prob (BadPairs δ ε) ≤
    …

    Mentions: OAI.HyperbolicObstruction.SixTable.law, OAI.HyperbolicObstruction.SixTable.BadPairs

16. lemma OAI.HyperbolicObstruction.SixTable.badPairs_rate_tendsto line 105