Algebraic layer: HM-GM inequality

theorem hm_le_gm (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : 2 * a * b / (a + b) ≤ √(a * b)

The harmonic mean of two positive reals is at most their geometric mean. More precisely, if a, b > 0, then 2ab/(a+b) ≤ √(ab). Equivalently, 4a²b² ≤ ab(a+b)², which simplifies to 0 ≤ ab(a-b)².

theorem prod_sub_one_mul_prod_add_one {n : ℕ} (α : Fin n → ℝ) : (∏ i : Fin n, (α i - 1)) * ∏ i : Fin n, (α i + 1) = ∏ i : Fin n, (α i ^ 2 - 1)

Product identity: ∏ᵢ (αᵢ - 1) · ∏ᵢ (αᵢ + 1) = ∏ᵢ (αᵢ² - 1).

Definitions for the Erdős–Gallai setting

noncomputable def erdos_gallai_deriv_at_one {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ

f'(1) for our polynomial, up to sign: f'(1) = -2 · ∏ᵢ(αᵢ - 1) · ∏ⱼ(βⱼ + 1).

Equations

• erdos_gallai_deriv_at_one α β = (-2 * ∏ i : Fin m, (α i - 1)) * ∏ j : Fin n, (β j + 1)

noncomputable def erdos_gallai_deriv_at_neg_one {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ

f'(-1) for our polynomial: f'(-1) = 2 · ∏ᵢ(αᵢ + 1) · ∏ⱼ(βⱼ - 1).

Equations

• erdos_gallai_deriv_at_neg_one α β = (2 * ∏ i : Fin m, (α i + 1)) * ∏ j : Fin n, (β j - 1)

noncomputable def erdos_gallai_C_sq {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ

C² = ∏ᵢ(αᵢ² - 1) · ∏ⱼ(βⱼ² - 1).

Equations

• erdos_gallai_C_sq α β = (∏ i : Fin m, (α i ^ 2 - 1)) * ∏ j : Fin n, (β j ^ 2 - 1)

theorem erdos_gallai_deriv_product {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : -erdos_gallai_deriv_at_one α β * erdos_gallai_deriv_at_neg_one α β = 4 * erdos_gallai_C_sq α β

Key identity: -f'(1)·f'(-1) = 4·C². That is, -(-2∏(αᵢ-1)∏(βⱼ+1))·(2∏(αᵢ+1)∏(βⱼ-1)) = 4·∏(αᵢ²-1)·∏(βⱼ²-1).

noncomputable def erdos_gallai_T {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ

The tangential trapezoid: T = -2 f'(1) f'(-1) / (f'(1) - f'(-1)).

When f'(1) < 0 and f'(-1) > 0 (normal case), this equals 2·|f'(1)|·|f'(-1)| / (|f'(1)| + |f'(-1)|), the harmonic mean.

Equations

• erdos_gallai_T α β = -2 * erdos_gallai_deriv_at_one α β * erdos_gallai_deriv_at_neg_one α β / (erdos_gallai_deriv_at_one α β - erdos_gallai_deriv_at_neg_one α β)

Integral layer: f(x), area A, and the bound A ≥ (4/3)C

noncomputable def erdos_gallai_f {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) (x : ℝ) : ℝ

f(x) = (1 - x²) · ∏ᵢ (αᵢ - x) · ∏ⱼ (βⱼ + x).

Equations

• erdos_gallai_f α β x = ((1 - x ^ 2) * ∏ i : Fin m, (α i - x)) * ∏ j : Fin n, (β j + x)

noncomputable def erdos_gallai_area {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ

The area A = ∫₋₁¹ f(x) dx.

Equations

• erdos_gallai_area α β = ∫ (x : ℝ) in -1..1, erdos_gallai_f α β x

theorem erdos_gallai_f_continuous {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : Continuous (erdos_gallai_f α β)

f is continuous (finite product of continuous functions).

theorem erdos_gallai_f_integrable {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : IntervalIntegrable (erdos_gallai_f α β) MeasureTheory.volume (-1) 1

f is interval-integrable on [-1, 1].

theorem erdos_gallai_f_mul_neg {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) (x : ℝ) : erdos_gallai_f α β x * erdos_gallai_f α β (-x) = ((1 - x ^ 2) ^ 2 * ∏ i : Fin m, (α i ^ 2 - x ^ 2)) * ∏ j : Fin n, (β j ^ 2 - x ^ 2)

f(x) · f(-x) = (1 - x²)² · ∏ᵢ (αᵢ² - x²) · ∏ⱼ (βⱼ² - x²).

theorem erdos_gallai_C_sq_nonneg {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) (hα : ∀ (i : Fin m), 1 ≤ α i) (hβ : ∀ (j : Fin n), 1 ≤ β j) : 0 ≤ erdos_gallai_C_sq α β

C² ≥ 0 when all αᵢ, βⱼ ≥ 1.

theorem erdos_gallai_integral_neg_eq {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ∫ (x : ℝ) in -1..1, erdos_gallai_f α β (-x) = ∫ (x : ℝ) in -1..1, erdos_gallai_f α β x

Symmetrization: ∫₋₁¹ f(-x) dx = ∫₋₁¹ f(x) dx. By the substitution x ↦ -x, and using neg_neg on the bounds.

theorem erdos_gallai_f_nonneg {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) (hα : ∀ (i : Fin m), 1 ≤ α i) (hβ : ∀ (j : Fin n), 1 ≤ β j) (x : ℝ) (hx : x ∈ Set.Icc (-1) 1) : 0 ≤ erdos_gallai_f α β x

f(x) ≥ 0 for x ∈ [-1, 1] when αᵢ, βⱼ ≥ 1.

theorem sq_sub_sq_ge {a x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : a ^ 2 - 1 ≤ a ^ 2 - x ^ 2

For x ∈ [-1, 1]: a² - x² ≥ a² - 1. The hypothesis a ≥ 1 from the tex is not needed.

theorem erdos_gallai_f_mul_neg_ge {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) (hα : ∀ (i : Fin m), 1 ≤ α i) (hβ : ∀ (j : Fin n), 1 ≤ β j) (x : ℝ) (hx : x ∈ Set.Icc (-1) 1) : (1 - x ^ 2) ^ 2 * erdos_gallai_C_sq α β ≤ erdos_gallai_f α β x * erdos_gallai_f α β (-x)

f(x)·f(-x) ≥ (1 - x²)² · C² for x ∈ [-1,1], αᵢ,βⱼ ≥ 1.

theorem am_gm_sqrt (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 2 * √(a * b) ≤ a + b

AM-GM for square roots: 2√(ab) ≤ a + b for a, b ≥ 0.

theorem integral_one_sub_sq : ∫ (x : ℝ) in -1..1, 1 - x ^ 2 = 4 / 3

∫₋₁¹ (1-x²) dx = 4/3.

theorem erdos_gallai_integral_bound {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) (hα : ∀ (i : Fin m), 1 ≤ α i) (hβ : ∀ (j : Fin n), 1 ≤ β j) : erdos_gallai_area α β ≥ 4 / 3 * √(erdos_gallai_C_sq α β)

The area A ≥ (4/3) · √(C²). This is the integral layer of the Erdős–Gallai proof. By AM-GM, (f(x) + f(-x))/2 ≥ √(f(x)·f(-x)) ≥ (1-x²)·C. Integrating gives A ≥ (4/3)·C.