WalkApexAggregate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.ConeSkeleton.actual_nominal_apex line 29

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 c hc f P select) : ℝ) +
      2 * ((∑ b : Fan n w, ((indexedFanData n w d c hc f P select b hs hm hred hrad).weight : ℝ)) -
        7 * Fintype.card (SelectedTopFace n w d c hc f P select)) ≤
    ((∑ b : Fan n w, ((indexedFanData n w d c hc f P select b hs hm hred hrad).triangles : ℝ)) +
      ∑ b : Fan n w, ((indexedFanData n w d c hc f P select b hs hm hred hrad).payments : ℝ))/2 +
      2 * ∑ b : Fan n w, ((indexedFanData n w d c hc f P select b hs hm hred hrad).partialCount : ℝ) := by
…

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

lemma OAI.HyperbolicObstruction.ConeSkeleton.actual_triangles_le line 48
lemma OAI.HyperbolicObstruction.ConeSkeleton.actual_partial_le line 55