OAI/Geometry/HyperbolicGroups/RankCollection.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.shapeFintype line 16
  2. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape line 26

    Source documentation

    Each count is bounded separately. Thus every collection of at most M occurrences is included, with all its retained fan slots. This harmless stronger finite family needs no union over diagram copies or equality guesses.

    abbrev BoundedShape (M : ℕ) := Σ s : Fin (M+1), Σ u : Fin (M+1),
…
  3. instance OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.(instance at line 29) line 29
  4. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape.tops line 36
  5. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape.fans line 37
  6. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape.squares line 38
  7. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape.sixes line 39
  8. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape.shape line 40
  9. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape.Good line 42
  10. instance OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape.(instance at line 44) line 44
  11. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape.rate line 47
  12. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape.rate_nonneg line 51
  13. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape.rate_tendsto line 54
  14. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.BoundedShape.bad_bound line 57
  15. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.GoodUpTo line 65

    Source documentation

    The exact source diagram:rank conclusion at any fixed finite size.

    def GoodUpTo (M : ℕ) {n : ℕ} (α β δ : ℝ) (w : Entry (SymmetricAlphabet n) → Bool) :=
…

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Entry, OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet

  16. instance OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.(instance at line 67) line 67
  17. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.rankRate line 70
  18. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.rankRate_nonneg line 72
  19. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.rankRate_tendsto line 75
  20. theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.rank_bad_bound line 82

    Source documentation

    The bounded-rank bad-event probability tends to zero, with literal costs and original full probability space.

    theorem rank_bad_bound (M : ℕ) {n : ℕ} {α β δ : ℝ}
    (ha : 0 ≤ α) (hb : 7*α ≤ β) (hd : 0 ≤ δ) :
    (FiniteLaw.bernoulliProduct (probability α β δ (SymmetricAlphabet n))
      (probability_mem ha hb hd)).prob (fun w => ¬GoodUpTo M α β δ w) ≤
      rankRate M α β δ (Fintype.card (SymmetricAlphabet n)) := by
…

    Mentions: OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.probability, OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.probability_mem, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.GoodUpTo, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.rankRate

  21. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.GoodUpTo.rank_bound line 91
  22. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.GoodUpTo.mono line 98