Large faces after passing to a common measure

Deleting at most ε² / 4 of the global reference mass preserves positivity and makes every old ε-large face ε / 2-large for the retained measure. The estimates apply to finite real weights, including natural weights by WeightedIncidence.mass_natCast.

theorem EGZ.WeightedIncidence.mass_weight_mono {α : Type u_1} [Fintype α] (w u : α → ℝ) (h : ∀ (a : α), u a ≤ w a) (S : Set α) : mass u S ≤ mass w S

theorem EGZ.WeightedIncidence.mass_sub_weight {α : Type u_1} [Fintype α] (w u : α → ℝ) (S : Set α) : mass (fun (a : α) => w a - u a) S = mass w S - mass u S

theorem EGZ.WeightedIncidence.mass_loss_le_total {α : Type u_1} [Fintype α] (w u : α → ℝ) (h : ∀ (a : α), u a ≤ w a) (S : Set α) : mass w S - mass u S ≤ ∑ a : α, (w a - u a)

The loss on any set is bounded by the loss on all atoms.

theorem EGZ.CommonMeasure.mass_tail_estimates {ε R D a b : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hR : 0 < R) (hD : 0 ≤ D) (hDsmall : D ≤ ε ^ 2 / 4 * R) (ha : ε * R ≤ a) (hb : a - D ≤ b) : 0 < b ∧ ε / 2 * R ≤ b ∧ (1 - ε) * a < (1 - ε / 2) * b

Numerical form of the mass-and-tail estimate. The strict proper-face inequality has enough room to tolerate the whole permitted tail loss.

theorem EGZ.CommonMeasure.face_estimates {α : Type u_1} [Fintype α] (w u : α → ℝ) (hle : ∀ (a : α), u a ≤ w a) {ε R : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hR : 0 < R) (hloss : ∑ a : α, (w a - u a) ≤ ε ^ 2 / 4 * R) (S : Set α) (hlarge : ε * R ≤ WeightedIncidence.mass w S) : 0 < WeightedIncidence.mass u S ∧ ε / 2 * R ≤ WeightedIncidence.mass u S ∧ ∀ (T : Set α), WeightedIncidence.mass w T ≤ (1 - ε) * WeightedIncidence.mass w S → WeightedIncidence.mass u T < (1 - ε / 2) * WeightedIncidence.mass u S

Positivity, reference-mass largeness, and strict proper-subface separation for a retained finite measure.

theorem EGZ.CommonMeasure.relative_mass_le {α : Type u_1} [Fintype α] (w u : α → ℝ) (hle : ∀ (a : α), u a ≤ w a) {ε R : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hR : 0 < R) (hloss : ∑ a : α, (w a - u a) ≤ ε ^ 2 / 4 * R) (S P : Set α) (hlarge : ε * R ≤ WeightedIncidence.mass w S) (hP : WeightedIncidence.mass w P ≤ R) : ε / 2 * WeightedIncidence.mass u P ≤ WeightedIncidence.mass u S

Largeness relative to any polytope whose old mass is below the global reference mass.

theorem EGZ.CommonMeasure.final_mass_le {α : Type u_1} [Fintype α] (w u : α → ℝ) (hu : ∀ (a : α), 0 ≤ u a) (hle : ∀ (a : α), u a ≤ w a) {ε R : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hR : 0 < R) (hloss : ∑ a : α, (w a - u a) ≤ ε ^ 2 / 4 * R) (S P Q : Set α) (hlarge : ε * R ≤ WeightedIncidence.mass w S) (hSQ : S ⊆ Q) (hP : WeightedIncidence.mass w P ≤ R) : ε / 2 * WeightedIncidence.mass u P ≤ WeightedIncidence.mass u Q

A retained large face inside the final polytope bounds the final polytope mass relative to any initial set below the same reference mass.

theorem EGZ.card_largeFaceSequence_of_mass_loss {α : Type u_1} [Fintype α] {d N : ℕ} (q : α → RealCoord d) (u : α → ℝ) (hu : ∀ (a : α), 0 ≤ u a) (w : Fin (N + 1) → α → ℝ) (R : Fin (N + 1) → ℝ) (hle : ∀ (i : Fin (N + 1)) (a : α), u a ≤ w i a) (hR : ∀ (i : Fin (N + 1)), 0 < R i) (htotal : ∀ (i : Fin (N + 1)), ∑ a : α, w i a ≤ R i) (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 < ε) (hεhalf : ε ≤ 1 / 2) (hloss : ∀ (i : Fin (N + 1)), ∑ a : α, (w i a - u a) ≤ ε ^ 2 / 4 * R i) (hlarge : ∀ (i : Fin (N + 1)), ε * R i ≤ WeightedIncidence.mass (w i) (q ⁻¹' (Γ i).carrier)) (hproper : ∀ (i : Fin (N + 1)) (Δ : (P i).Face), Δ.carrier ⊂ (Γ i).carrier → WeightedIncidence.mass (w i) (q ⁻¹' Δ.carrier) ≤ (1 - ε) * WeightedIncidence.mass (w i) (q ⁻¹' (Γ i).carrier)) : ↑(N + 1) ≤ (((ε / 2) ^ 3)⁻¹ + ↑d + 2) ^ (d + 2)

Apply the uniform large-face bound to varying old measures and one common retained measure. Only the dimension and ε occur in the bound.