OAI/Geometry/HyperbolicGroups/IncidenceTemplate.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Row line 14
2. instance OAI.HyperbolicObstruction.IncidenceTemplate.instRowDecidableEq line 16
3. lemma OAI.HyperbolicObstruction.IncidenceTemplate.card_rows line 18
4. def OAI.HyperbolicObstruction.IncidenceTemplate.rowSupport line 22

   Source documentation

   The 98 distinct array types of the exact master pattern.

   def rowSupport : Row → Finset Field
     | Sum.inl i => (fan i).map Function.Embedding.inl
     | Sum.inr (Sum.inl _) => Finset.univ.map Function.Embedding.inl
     | Sum.inr (Sum.inr τ) => squareSupport τ

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Row, OAI.HyperbolicObstruction.IncidenceTemplate.Field, OAI.HyperbolicObstruction.IncidenceTemplate.fan, OAI.HyperbolicObstruction.IncidenceTemplate.squareSupport

5. def OAI.HyperbolicObstruction.IncidenceTemplate.rowCost line 27
6. def OAI.HyperbolicObstruction.IncidenceTemplate.pattern line 32
7. lemma OAI.HyperbolicObstruction.IncidenceTemplate.pattern_exponent line 43
8. lemma OAI.HyperbolicObstruction.IncidenceTemplate.rowSupport_card line 56
9. lemma OAI.HyperbolicObstruction.IncidenceTemplate.admissible_card line 63
10. lemma OAI.HyperbolicObstruction.IncidenceTemplate.admissible_subset line 70
11. theorem OAI.HyperbolicObstruction.IncidenceTemplate.exists_critical_closure line 83

    Source documentation

    The closure and its whole-integer positive margin with no uninstantiated budget hypotheses: this is the exact master-pattern closure of Section 4.

    theorem exists_critical_closure (I : Finset Field) (e : Field) (he : e ∉ I)
        (hadm : Admissible (insert e I)) :
        ∃ U : Finset Field, I ⊆ U ∧ criticalExponent U = I.card ∧ e ∉ U ∧
          ∀ V : Finset Field, V.Nonempty → Disjoint V U →
            1 ≤ criticalExponent (U ∪ V) - criticalExponent U := by
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Field, OAI.HyperbolicObstruction.IncidenceTemplate.Admissible, OAI.HyperbolicObstruction.IncidenceTemplate.criticalExponent