OAI/Geometry/HyperbolicGroups/SixRows.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.SixTable.Rows line 17
2. instance OAI.HyperbolicObstruction.SixTable.(instance at line 20) line 20
3. def OAI.HyperbolicObstruction.SixTable.row line 23
4. lemma OAI.HyperbolicObstruction.SixTable.card_row_fiber line 25
5. lemma OAI.HyperbolicObstruction.SixTable.row_card_sum line 43
6. lemma OAI.HyperbolicObstruction.SixTable.count_bounds line 48
7. lemma OAI.HyperbolicObstruction.SixTable.rows_nonempty line 59
8. theorem OAI.HyperbolicObstruction.SixTable.marginal_bound line 74

   Source documentation

   The literal uniform law on the six-letter relators with first letter u has all five remaining marginal densities at most twice uniform.

   theorem marginal_bound {δ τ : ℝ} {w : (Fin 6 → A) → Bool}
       (hτ : τ ≤ 1/3) (h : ¬BadPairs δ τ w) (u : A) :
       letI := rows_nonempty (by linarith : τ < 1) h u
   …

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