finite midpoint chain affine

Proved

BirkhoffGlobalSection.finite_midpoint_chain_affine

by Mazecto · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-geometryreal-analysistopology

A finite nonempty phase-space chain whose internal vertices are midpoints of their neighbors is an affine arithmetic progression. The exact regularity, compactness, nonzero and uniqueness hypotheses displayed in the formal statement are retained.

Preamble

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

Formal statement

theorem BirkhoffGlobalSection.finite_midpoint_chain_affine (N : ℕ) (hN : 0 < N) (p : Fin (N + 1) → Phase)
    (hmid : ∀ i j : Fin N, j.succ = i.castSucc →
      p i.castSucc = (1 / 2 : ℝ) • (p j.castSucc + p i.succ)) :
    ∃ d : Phase, ∀ k : Fin (N + 1), p k = p 0 + (k.val : ℝ) • d := by sorry

Source

Independent extraction from accepted source Solutions/Sol_BirkhoffGlobalSection_closed_preconnected_locally_convex_is_convex.lean:327. Local normalization abbreviations and map definitions are expanded explicitly in the statement. Exact mathematical scope retained; no global-section conclusion.

View graph