Diameter shrinking for iterated barycentric subdivision

This file proves the geometric metric shrinking facts for affine barycentric subdivision of the standard topological simplex Δⁿ and its iterates. These are the metric inputs needed by the later small-simplices theorem.

The mathematical content is the classical estimate: one barycentric subdivision of a simplex contracts diameters by the factor n/(n+1) < 1, and therefore the N-fold subdivision contracts by (n/(n+1))^N → 0.

Design

Rather than route through the singular-chain subdivision operator, we work directly with the affine layer. A simplex is described by its tuple of n+1 vertices V : Fin (n+1) → E in a real normed space E. One barycentric subdivision step, for a permutation π of the vertices, produces the new vertex tuple

(stepVertices V π) k = barycenter {V (π 0), …, V (π k)}
 = (k+1)⁻¹ • Σ_{j ≤ k} V (π j).

The geometric simplex is the convex hull of the vertex tuple, and Metric.diam (convexHull ℝ (Set.range V)) = Metric.diam (Set.range V) (convexHull_diam), so it suffices to bound Metric.diam (Set.range V).

Main results

• contractionFactor n = n/(n+1), with contractionFactor_nonneg and contractionFactor_lt_one.
• stepVertices_diam_le — one-step contraction: diam (range (stepVertices V π)) ≤ contractionFactor n * diam (range V).
• iterVertices — the vertex tuple of an affine sub-simplex of sdᴺ.
• iterVertices_diam_le — diam (range (iterVertices …)) ≤ (contractionFactor n)^N * diam (range V).
• exists_iteratedSubdivision_affine_diameter_lt — for every ε > 0 there is N such that every affine sub-simplex appearing in the N-fold barycentric subdivision of Δⁿ has diameter < ε.

The contraction factor

noncomputable def SphereOddDegree.BarycentricSubdivisionDiameter.contractionFactor (n : ℕ) : ℝ

The dimension-dependent contraction factor n/(n+1). It is < 1 for every n (in particular 0 for n = 0).

Equations

• SphereOddDegree.BarycentricSubdivisionDiameter.contractionFactor n = ↑n / (↑n + 1)

theorem SphereOddDegree.BarycentricSubdivisionDiameter.contractionFactor_nonneg (n : ℕ) : 0 ≤ contractionFactor n

theorem SphereOddDegree.BarycentricSubdivisionDiameter.contractionFactor_lt_one (n : ℕ) : contractionFactor n < 1

theorem SphereOddDegree.BarycentricSubdivisionDiameter.ratio_le_contractionFactor {l n : ℕ} (h : l ≤ n) : ↑l / (↑l + 1) ≤ contractionFactor n

One barycentric subdivision step on a vertex tuple

noncomputable def SphereOddDegree.BarycentricSubdivisionDiameter.stepVertices {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (V : Fin (n + 1) → E) (π : Equiv.Perm (Fin (n + 1))) : Fin (n + 1) → E

One barycentric subdivision step applied to a vertex tuple V, ordered by the permutation π. The k-th new vertex is the barycenter of the first k+1 old vertices in the order π.

Equations

• SphereOddDegree.BarycentricSubdivisionDiameter.stepVertices n V π k = (↑↑k + 1)⁻¹ • ∑ j ≤ k, V (π j)

theorem SphereOddDegree.BarycentricSubdivisionDiameter.isBounded_range {E : Type u_1} [NormedAddCommGroup E] (n : ℕ) (V : Fin (n + 1) → E) : Bornology.IsBounded (Set.range V)

The range of any vertex tuple over Fin (n+1) is bounded.

theorem SphereOddDegree.BarycentricSubdivisionDiameter.dist_vertex_step_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (V : Fin (n + 1) → E) (π : Equiv.Perm (Fin (n + 1))) (l i : Fin (n + 1)) (hi : i ≤ l) : dist (V (π i)) (stepVertices n V π l) ≤ ↑↑l / (↑↑l + 1) * Metric.diam (Set.range V)

theorem SphereOddDegree.BarycentricSubdivisionDiameter.dist_step_step_le_aux {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (V : Fin (n + 1) → E) (π : Equiv.Perm (Fin (n + 1))) (l l' : Fin (n + 1)) (hll : l ≤ l') : dist (stepVertices n V π l) (stepVertices n V π l') ≤ ↑↑l' / (↑↑l' + 1) * Metric.diam (Set.range V)

theorem SphereOddDegree.BarycentricSubdivisionDiameter.dist_step_step_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (V : Fin (n + 1) → E) (π : Equiv.Perm (Fin (n + 1))) (l l' : Fin (n + 1)) : dist (stepVertices n V π l) (stepVertices n V π l') ≤ contractionFactor n * Metric.diam (Set.range V)

theorem SphereOddDegree.BarycentricSubdivisionDiameter.stepVertices_diam_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (V : Fin (n + 1) → E) (π : Equiv.Perm (Fin (n + 1))) : Metric.diam (Set.range (stepVertices n V π)) ≤ contractionFactor n * Metric.diam (Set.range V)

noncomputable def SphereOddDegree.BarycentricSubdivisionDiameter.iterVertices {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n N : ℕ) : (Fin N → Equiv.Perm (Fin (n + 1))) → (Fin (n + 1) → E) → Fin (n + 1) → E

Iterate barycentric subdivision of a vertex family along a permutation word.

Equations

• One or more equations did not get rendered due to their size.
• SphereOddDegree.BarycentricSubdivisionDiameter.iterVertices n 0 x_3 x✝ = x✝

@[simp]

theorem SphereOddDegree.BarycentricSubdivisionDiameter.iterVertices_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (πs : Fin 0 → Equiv.Perm (Fin (n + 1))) (V : Fin (n + 1) → E) : iterVertices n 0 πs V = V

theorem SphereOddDegree.BarycentricSubdivisionDiameter.iterVertices_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n N : ℕ) (πs : Fin (N + 1) → Equiv.Perm (Fin (n + 1))) (V : Fin (n + 1) → E) : iterVertices n (N + 1) πs V = stepVertices n (iterVertices n N (fun (i : Fin N) => πs i.castSucc) V) (πs (Fin.last N))

theorem SphereOddDegree.BarycentricSubdivisionDiameter.iterVertices_diam_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n N : ℕ) (πs : Fin N → Equiv.Perm (Fin (n + 1))) (V : Fin (n + 1) → E) : Metric.diam (Set.range (iterVertices n N πs V)) ≤ contractionFactor n ^ N * Metric.diam (Set.range V)

The standard simplex and the main existence theorem

noncomputable def SphereOddDegree.BarycentricSubdivisionDiameter.stdVerts (n : ℕ) : Fin (n + 1) → Fin (n + 1) → ℝ

The tuple of n+1 standard basis vertices of Δⁿ, as points of Fin (n+1) → ℝ.

Equations

• SphereOddDegree.BarycentricSubdivisionDiameter.stdVerts n k = Pi.single k 1

theorem SphereOddDegree.BarycentricSubdivisionDiameter.diam_range_stdVerts_le_one (n : ℕ) : Metric.diam (Set.range (stdVerts n)) ≤ 1

theorem SphereOddDegree.BarycentricSubdivisionDiameter.exists_iteratedSubdivision_affine_diameter_lt (n : ℕ) (eps : ℝ) (heps : 0 < eps) : ∃ (N : ℕ), ∀ (πs : Fin N → Equiv.Perm (Fin (n + 1))), Metric.diam (Set.range (iterVertices n N πs (stdVerts n))) < eps

theorem SphereOddDegree.BarycentricSubdivisionDiameter.exists_iteratedSubdivision_affine_convexHull_diameter_lt (n : ℕ) (eps : ℝ) (heps : 0 < eps) : ∃ (N : ℕ), ∀ (πs : Fin N → Equiv.Perm (Fin (n + 1))), Metric.diam ((convexHull ℝ) (Set.range (iterVertices n N πs (stdVerts n)))) < eps

Convex-hull form of the theorem: the geometric affine sub-simplex (the convex hull of the vertex tuple) has diameter < ε after enough subdivisions.