A uniform bound for successive large faces

Nested polytopes with no repeated restricted face admit only boundedly many faces which each carry a fixed positive fraction of a common finite weight and lose a fixed fraction of that mass on every proper subface. The bound depends only on the dimension and these two fractions.

noncomputable def EGZ.LargeFaceSequence.rank {α : Type u_1} {d : ℕ} (q : α → RealCoord d) (S : Finset α) : ℕ

Affine rank of a finite set of atoms in the coordinate space.

Equations

• EGZ.LargeFaceSequence.rank q S = Module.finrank ℝ ↥(affineSpan ℝ (q '' ↑S)).direction

def EGZ.LargeFaceSequence.closure {α : Type u_1} {d : ℕ} (q : α → RealCoord d) (S : Finset α) : Set α

Atoms lying in the affine span of a finite configuration.

Equations

• EGZ.LargeFaceSequence.closure q S = q ⁻¹' ↑(affineSpan ℝ (q '' ↑S))

theorem EGZ.LargeFaceSequence.rank_le {α : Type u_1} {d : ℕ} (q : α → RealCoord d) (S : Finset α) : rank q S ≤ d

theorem EGZ.LargeFaceSequence.rank_insert_lt {α : Type u_1} {d : ℕ} [Finite α] (q : α → RealCoord d) (S : Finset α) (hS : S.Nonempty) (a : α) (ha : a ∉ closure q S) : rank q S < rank q (insert a S)

theorem EGZ.card_largeFaceSequence_le {α : Type u_1} [Fintype α] {d N : ℕ} (q : α → RealCoord d) (w : α → ℝ) (hw : ∀ (a : α), 0 ≤ w a) (hM : 0 < ∑ a : α, w a) (P : Fin N → RationalPolytope d) (Γ : (i : Fin N) → (P i).Face) (hnested : ∀ (i j : Fin N), i < j → (P j).carrier ⊆ (P i).carrier) (hdistinct : ∀ (i j : Fin N), i < j → (Γ i).carrier ∩ (P j).carrier ≠ (Γ j).carrier) (δ η : ℝ) (hδ : 0 < δ) (hη : 0 < η) (hlarge : ∀ (i : Fin N), η * ∑ a : α, w a ≤ WeightedIncidence.mass w (q ⁻¹' (Γ i).carrier)) (hproper : ∀ (i : Fin N) (Δ : (P i).Face), Δ.carrier ⊂ (Γ i).carrier → WeightedIncidence.mass w (q ⁻¹' Δ.carrier) ≤ (1 - δ) * WeightedIncidence.mass w (q ⁻¹' (Γ i).carrier)) : ↑N ≤ WeightedIncidence.bound (↑d + 1) (δ * η) d / η

A uniform large-face bound. The common total weight is positive; each face has mass at least η times that total, and each proper subface loses at least the fraction δ of its face's mass.

theorem EGZ.card_largeFaceSequence_le_paper {α : Type u_1} [Fintype α] {d N : ℕ} (q : α → RealCoord d) (w : α → ℝ) (hw : ∀ (a : α), 0 ≤ w a) (P : Fin (N + 1) → RationalPolytope d) (Γ : (i : Fin (N + 1)) → (P i).Face) (hnested : ∀ (i j : Fin (N + 1)), i < j → (P j).carrier ⊆ (P i).carrier) (hdistinct : ∀ (i j : Fin (N + 1)), i < j → (Γ i).carrier ∩ (P j).carrier ≠ (Γ j).carrier) (ε : ℝ) (hε : 0 < ε) (hM : 0 < WeightedIncidence.mass w (q ⁻¹' (P 0).carrier)) (hfinal : ε * WeightedIncidence.mass w (q ⁻¹' (P 0).carrier) ≤ WeightedIncidence.mass w (q ⁻¹' (P (Fin.last N)).carrier)) (hlarge : ∀ (i : Fin (N + 1)), ε * WeightedIncidence.mass w (q ⁻¹' (P i).carrier) ≤ WeightedIncidence.mass w (q ⁻¹' (Γ i).carrier)) (hproper : ∀ (i : Fin (N + 1)) (Δ : (P i).Face), Δ.carrier ⊂ (Γ i).carrier → WeightedIncidence.mass w (q ⁻¹' Δ.carrier) ≤ (1 - ε) * WeightedIncidence.mass w (q ⁻¹' (Γ i).carrier)) : ↑(N + 1) ≤ ((ε ^ 3)⁻¹ + ↑d + 2) ^ (d + 2)

Proposition large for a finitely supported measure, with its explicit bound. The necessary positive initial-mass hypothesis is stated explicitly. Weights outside the first polytope are harmless and are restricted away in the proof. The weak proper-subface inequality suffices.