RelativeApexAggregate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_nominal_apex line 30

Source documentation

The summed apex estimate is now a theorem about the actual selected mixed-picture faces. All nominal slots, turns, partial links and radial boundary sides are extracted from the picture itself.

theorem actual_nominal_apex (hb : P.NoBigon) :
    3 * (Fintype.card (SelectedTopFace n w d ell hell word c hc f P select) : ℝ) +
      2 * ((∑ b : Fan n w, ((indexedFanData n w d ell hell word c hc f P select b hs hm hred hrad).weight : ℝ)) -
        7 * Fintype.card (SelectedTopFace n w d ell hell word c hc f P select)) ≤
    ((∑ b : Fan n w, ((indexedFanData n w d ell hell word c hc f P select b hs hm hred hrad).triangles : ℝ)) +
      ∑ b : Fan n w, ((indexedFanData n w d ell hell word c hc f P select b hs hm hred hrad).payments : ℝ))/2 +
      2 * ∑ b : Fan n w, ((indexedFanData n w d ell hell word c hc f P select b hs hm hred hrad).partialCount : ℝ) := by
…

Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.SelectedTopFace, OAI.HyperbolicObstruction.ConeSkeleton.Fan, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.indexedFanData

lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_triangles_le line 49
lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_partial_le line 56