Error margins and the driving function in the main argument

These estimates use a uniform bound C for the hollow constant. They avoid the particular exponential constants in the paper; only a positive margin after rounding and balancing is needed.

noncomputable def EGZ.MainProof.errorScale (C ζ : ℝ) : ℝ

A sufficiently small internal loss parameter.

Equations

• EGZ.MainProof.errorScale C ζ = ζ / (100 * (C + 1))

theorem EGZ.MainProof.errorScale_pos {C ζ : ℝ} (hC : 0 ≤ C) (hζ : 0 < ζ) : 0 < errorScale C ζ

theorem EGZ.MainProof.errorScale_le {C ζ : ℝ} (hC : 0 ≤ C) (hζ : ζ ≤ 1) : errorScale C ζ ≤ 1 / 100

theorem EGZ.MainProof.errorScale_le_inv {C ζ W : ℝ} (hC : 0 ≤ C) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) (hW : 0 < W) (hWC : W ≤ C) : errorScale C ζ ≤ W⁻¹

noncomputable def EGZ.MainProof.gapScale (d : ℕ) (δ : ℝ) (K : ℕ) : ℝ

The flag lemma supplies this fraction of p in every nonempty fibre, because the normalized input contains at least p terms.

Equations

• EGZ.MainProof.gapScale d δ K = δ ^ 3 * (↑K)⁻¹ ^ d

theorem EGZ.MainProof.gapScale_pos {d K : ℕ} {δ : ℝ} (hδ : 0 < δ) (hK : 1 ≤ K) : 0 < gapScale d δ K

theorem EGZ.MainProof.balancing_margin {C ζ W : ℝ} (hC : 0 ≤ C) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) (hW : 0 ≤ W) (hWC : W ≤ C) : (1 + errorScale C ζ) * W ≤ (1 - errorScale C ζ) ^ 4 * (W + ζ)

A fourth power accounts for the two rounding factors, the retained mass loss, and the final reserve in each fibre.

theorem EGZ.MainProof.coefficient_le_reserve {C ζ W p m R a : ℝ} (hC : 0 ≤ C) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) (hW : 0 ≤ W) (hWC : W ≤ C) (hp : 0 ≤ p) (hm : 0 ≤ m) (hR : 0 < R) (hretained : (1 - errorScale C ζ) * (W + ζ) * p ≤ R) (ha : a ≤ (1 + errorScale C ζ) / (1 - errorScale C ζ) ^ 2 * p * W * m / R) : a ≤ (1 - errorScale C ζ) * m

The numerical step after rounding and balanced combination. The centrality denominator θ M is bounded below by retained mass divided by the hollow constant.

def EGZ.MainProof.drivingFunction (threshold : ℕ → ℕ) (K : ℕ) : ℕ

A pointwise prescribed threshold has a monotone majorant strictly larger than the identity. No monotonicity of expansion thresholds is assumed.

Equations

• EGZ.MainProof.drivingFunction threshold K = K + 1 + (Finset.range (K + 1)).sup threshold

theorem EGZ.MainProof.drivingFunction_isGrowing (threshold : ℕ → ℕ) : IsGrowing (drivingFunction threshold)

theorem EGZ.MainProof.threshold_lt_drivingFunction (threshold : ℕ → ℕ) (K : ℕ) : threshold K < drivingFunction threshold K