Geometric replacement bounds for the collapse induction

The proof of Proposition 5.9 replaces every point in a collapsed subtree by one distinguished leaf. The paper prints the weaker comparability (5.41), but the preceding argument gives a quarter-distance perturbation. Retaining that stronger form makes each changed edge cost at most 2; with at most 2n boundary edges this is the stated 4^n loss in (5.43).

theorem Anderson4D.four_mul_znorm_replacement_le_five_mul (y x x' : Fin 4 → ℤ) (hsmall : 4 * znorm (x - x') ≤ znorm (y - x)) : 4 * znorm (y - x') ≤ 5 * znorm (y - x)

A perturbation by at most one quarter of the original distance changes the new distance by at most a factor 5/4, in division-free form.

theorem Anderson4D.znorm_le_two_mul_replacement (y x x' : Fin 4 → ℤ) (hsmall : 4 * znorm (x - x') ≤ znorm (y - x)) : znorm (y - x) ≤ 2 * znorm (y - x')

The displayed lower half of paper (5.41).

theorem Anderson4D.collapse_distance_comparable (y x x' : Fin 4 → ℤ) (hsmall : 4 * znorm (x - x') ≤ znorm (y - x)) : znorm (y - x) ≤ 2 * znorm (y - x') ∧ znorm (y - x') ≤ 2 * znorm (y - x)

Paper (5.41), kept in division-free form.

theorem Anderson4D.inv_one_add_sq_le_two_mul_inv_one_add_sq (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hba : 4 * b ≤ 5 * a) : (1 + a ^ 2)⁻¹ ≤ 2 * (1 + b ^ 2)⁻¹

Scalar inverse-bracket comparison used for one boundary edge.

theorem Anderson4D.latticeEdgeWeight_le_two_mul_of_quarter_replacement (y x x' : Fin 4 → ℤ) (hsmall : 4 * znorm (x - x') ≤ znorm (y - x)) : latticeEdgeWeight y x ≤ 2 * latticeEdgeWeight y x'

Replacing one endpoint by a point within a quarter of the original edge length costs at most a factor 2 in latticeEdgeWeight.

theorem Anderson4D.latticeEdgeWeight_le_two_mul_of_quarter_replacement_left (y x x' : Fin 4 → ℤ) (hsmall : 4 * znorm (x - x') ≤ znorm (y - x)) : latticeEdgeWeight x y ≤ 2 * latticeEdgeWeight x' y

Symmetric endpoint version of the same replacement estimate.

theorem Anderson4D.prod_le_four_pow_mul_prod_of_card_le_two_mul {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (f g : ι → ℝ) (n : ℕ) (hf : ∀ i ∈ S, 0 ≤ f i) (hg : ∀ i ∈ S, 0 ≤ g i) (hfg : ∀ i ∈ S, f i ≤ 2 * g i) (hcard : S.card ≤ 2 * n) : ∏ i ∈ S, f i ≤ 4 ^ n * ∏ i ∈ S, g i

At most 2n replacement edges, each costing at most 2, give the 4^n loss printed in (5.43).