OAI/Geometry/HyperbolicGroups/StarIncidence.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.StarModel.center line 17
  2. def OAI.HyperbolicObstruction.StarModel.wing line 20
  3. lemma OAI.HyperbolicObstruction.StarModel.center_subset line 24
  4. lemma OAI.HyperbolicObstruction.StarModel.wing_disjoint line 29
  5. lemma OAI.HyperbolicObstruction.StarModel.mem_center line 37
  6. lemma OAI.HyperbolicObstruction.StarModel.mem_wing line 45
  7. lemma OAI.HyperbolicObstruction.StarModel.coord_mem line 55
  8. lemma OAI.HyperbolicObstruction.StarModel.card_center line 66
  9. lemma OAI.HyperbolicObstruction.StarModel.card_wing line 69
  10. lemma OAI.HyperbolicObstruction.StarModel.card_decomposition line 77
  11. lemma OAI.HyperbolicObstruction.StarModel.support_subset line 87
  12. lemma OAI.HyperbolicObstruction.StarModel.center_support_subset line 95
  13. lemma OAI.HyperbolicObstruction.StarModel.sum_subtype_ite line 108

    Source documentation

    A finite sum over an explicitly selected subtype, allowing the row array cost to be expressed without introducing independent branch arrays.

    lemma sum_subtype_ite {T : Type*} [Fintype T] (p : T → Prop) [DecidablePred p]
    (f : T → ℤ) : (∑ x : {x : T // p x}, f x.val) = ∑ x, if p x then f x else 0 := by
…
  14. lemma OAI.HyperbolicObstruction.StarModel.saturated_cost line 116
  15. lemma OAI.HyperbolicObstruction.StarModel.star_exponent_eq line 146
  16. lemma OAI.HyperbolicObstruction.StarModel.selected_cost line 156