Exact deficient-cut averaging #
Jensen's inequality turns the two per-edge cut inequalities into a scalar contradiction at the exact 9/10 threshold.
theorem
LeanPool.DrossFractionalTriangleDecomposition.deficient_finish_exact
{α : Type u_1}
(A B : Finset α)
(hA : A.Nonempty)
(hB : B.Nonempty)
(T : α → ℝ)
(n m cc wΔ δ : ℝ)
(hδ0 : 0 < δ)
(hδ1 : δ ≤ 1 / 10)
(hn : 20 ≤ n)
(hcc : 0 < cc)
(hccrel : 2 * wΔ = cc * (3 * n * (1 - δ) - 3))
(hcard : ↑A.card + ↑B.card = m)
(hTA : ∀ e ∈ A, (1 - 2 * δ) * n ≤ T e ∧ T e ≤ n)
(hTB : ∀ e ∈ B, (1 - 2 * δ) * n ≤ T e ∧ T e ≤ n)
(mbound : 2 * m ≤ (1 - δ + 2 * δ ^ 2) * n ^ 2 + 4 + n - 6 * δ * n)
(ineq1 : cc * ∑ e ∈ A, (T e * (T e - δ * n) / 2 - ↑A.card) < ∑ e ∈ A, (T e * wΔ - 1))
(ineq2 : cc * ∑ e ∈ B, (T e * (T e - δ * n) / 2 - ↑B.card) < ∑ e ∈ B, (1 - T e * wΔ))
: