OAI/Geometry/HyperbolicGroups/RestrictOccurrence.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights line 15

    Source documentation

    Integer weights on the occurrences, with fan slots retained at every level.

    structure Weights where
…
  2. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.position line 27
  3. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.TopAt line 33
  4. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.FanAt line 34
  5. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.SquareAt line 35
  6. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.SixAt line 36
  7. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.topEnum line 38
  8. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.fanEnum line 39
  9. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.squareEnum line 40
  10. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.sixEnum line 41
  11. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.topIndex line 43
  12. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.fanIndex line 44
  13. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.squareIndex line 45
  14. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.sixIndex line 46
  15. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.atLevel line 49

    Source documentation

    The literal collection at level j; a retained top keeps every fan slot.

    def atLevel (j : ℕ) : Shape (Fintype.card (W.TopAt j)) (Fintype.card (W.FanAt j))
    (Fintype.card (W.SquareAt j)) :=
…

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape

  16. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.embedPosition line 59

    Source documentation

    Positions and trials embed in the unchanged original arrays.

    def embedPosition (j : ℕ) : (W.atLevel j).Pos (Fintype.card (W.SixAt j)) → T.Pos v
  | .inl a => .inl (W.topIndex j a)
  | .inr (.inl ⟨b,f⟩) => .inr (.inl ⟨W.fanIndex j b,f⟩)
  | .inr (.inr (.inl ⟨e,f⟩)) => .inr (.inr (.inl ⟨W.squareIndex j e,f⟩))
  | .inr (.inr (.inr (e,i))) => .inr (.inr (.inr (W.sixIndex j e,i)))

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Pos

  17. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.embedTrial line 65
  18. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.embedPosition_injective line 72
  19. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.embedTrial_injective line 89
  20. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.image_embedPosition line 99
  21. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.coreCoord_embed line 131
  22. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.row_embed line 140
  23. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.rank_embed line 159
  24. theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.rank_level_bound line 170

    Source documentation

    Any good bounded-rank table supplies the full weighted-level estimates on actual field positions; the restricted collection is reindexed rather than assumed to satisfy a new condition.

    theorem rank_level_bound {M n : ℕ} {α β δ : ℝ} {w : Entry (SymmetricAlphabet n) → Bool}
    (h : GoodUpTo M α β δ w) (hs : s ≤ M) (hu : u ≤ M) (hq : q ≤ M) (hv : v ≤ M)
    (σ : T.Pos v → SymmetricAlphabet n) (hi : Function.Injective (T.row σ))
    (hp : BernoulliCandidates.Present T.row w σ) (j : ℕ) :
    (Coincidence.rankOn (fun p => (σ p).1) (Finset.univ.filter (fun p => j < W.position p)) : ℝ) ≤
      ((3-β)-7*(2-α)) * Fintype.card (W.TopAt j) + (2-α) * Fintype.card (W.FanAt j) +
        (2-δ) * Fintype.card (W.SquareAt j) + (3-δ) * Fintype.card (W.SixAt j) := by
…

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Entry, OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.GoodUpTo, OAI.HyperbolicObstruction.BernoulliCandidates.Present, OAI.HyperbolicObstruction.Coincidence.rankOn