affine chain convex combinations mem

import Definitions.Def_BirkhoffGlobalSection
import Mathlib.Topology.Algebra.Module.LocallyConvex
import Mathlib.Topology.MetricSpace.Pseudo.Lemmas
import Mathlib.Analysis.Normed.Module.Convex
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Topology.UnitInterval
import Mathlib.Topology.Order.Compact
import Mathlib.Analysis.Normed.Affine.AddTorsor
import Mathlib.Algebra.Order.Floor.Semiring
import Mathlib.Tactic.NormNum
import Mathlib.Topology.MetricSpace.ProperSpace

open scoped Topology
open Set Metric Filter
open BirkhoffGlobalSection


open BirkhoffGlobalSection NormedSpace Set Metric Filter
open scoped Topology unitInterval BigOperators
set_option autoImplicit false
set_option maxHeartbeats 1600000
set_option linter.unusedVariables false

theorem BirkhoffGlobalSection.affine_chain_convex_combinations_mem (K : Set Phase) (N : ℕ) (hN : 0 < N)
    (p : Fin (N + 1) → Phase) (d : Phase)
    (haff : ∀ k, p k = p 0 + (k.val : ℝ) • d)
    (hpmem : ∀ k, p k ∈ K) (δ ε : ℝ) (hδ : 0 < δ) (hεδ : ε < δ)
    (hedge : ∀ i : Fin N, dist (p i.castSucc) (p i.succ) ≤ ε)
    (hloc : ∀ k, Convex ℝ (K ∩ ball (p k) δ))
    (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
    a • p 0 + b • p (Fin.last N) ∈ K := by sorry