OAI/Geometry/HyperbolicGroups/Cost.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.SparsePattern.Pattern.cost_subset line 17
2. lemma OAI.HyperbolicObstruction.SparsePattern.Pattern.pinned_overlap_margin line 29

   Source documentation

   Pinning zero or one named field leaves a full unit on any active row overlap.

   lemma pinned_overlap_margin (supports : ∀ r, 3 ≤ (P.support r).card)
       (budget : ∀ W : Finset F, (min 2 W.card : ℕ) ≤ P.exponent W)
       {J : Finset R} (hJ : J.Nonempty) (I : Finset F) (hI : I.card ≤ 1) :
       1 ≤ ((J.biUnion P.support \ I).card : ℤ) - ∑ r ∈ J, P.cost r := by
   …

3. def OAI.HyperbolicObstruction.IncidenceTemplate.rowSurcharge line 49

   Source documentation

   Exact increases from critical to actual array-entry costs.

   def rowSurcharge (α β δ : ℝ) : Row → ℝ
     | Sum.inl _ => α
     | Sum.inr (Sum.inl _) => β - 7 * α
     | Sum.inr (Sum.inr _) => δ
   
   /-- Source Equation (sample:eq-costs), with the critical integer cost displayed. -/

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Row

4. def OAI.HyperbolicObstruction.IncidenceTemplate.actualRowCost line 55

   Source documentation

   Source Equation (sample:eq-costs), with the critical integer cost displayed.

   def actualRowCost (α β δ : ℝ) (r : Row) : ℝ := rowCost r + rowSurcharge α β δ r

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Row, OAI.HyperbolicObstruction.IncidenceTemplate.rowCost, OAI.HyperbolicObstruction.IncidenceTemplate.rowSurcharge

5. lemma OAI.HyperbolicObstruction.IncidenceTemplate.rowSurcharge_nonneg line 57
6. lemma OAI.HyperbolicObstruction.IncidenceTemplate.rowSurcharge_sum line 64
7. lemma OAI.HyperbolicObstruction.IncidenceTemplate.rowSurcharge_subset line 68
8. lemma OAI.HyperbolicObstruction.IncidenceTemplate.actualRowCost_nonneg line 74
9. lemma OAI.HyperbolicObstruction.IncidenceTemplate.actual_pinned_overlap line 79