Dense-graph estimates for Dross cuts

The K₄ partner count and the triangle-through-edge count are bounded using minimum degree. Finite convex averaging supplies the cut-level estimate.

theorem LeanPool.DrossFractionalTriangleDecomposition.convex_avg {α : Type u_2} {A : Finset α} (hA : A.Nonempty) (T : α → ℝ) (c₀ : ℝ) : ↑A.card * ((∑ e ∈ A, T e / ↑A.card) * (∑ e ∈ A, T e / ↑A.card - c₀)) ≤ ∑ e ∈ A, T e * (T e - c₀)

Convex averaging (finite Jensen for T ↦ T(T − c₀)). For a nonempty finite A, the sum of T e (T e − c₀) dominates |A| times T_A (T_A − c₀) with T_A the average. (Proved via Cauchy–Schwarz; the linear part cancels exactly.)

theorem LeanPool.DrossFractionalTriangleDecomposition.codeg_ge_of_dense {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (h : 9 * Fintype.card V ≤ 10 * G.minDegree) (u v : V) : 8 * Fintype.card V ≤ 10 * codeg G u v

Codegree lower bound. In a dense graph (δ ≥ (9/10)n), adjacent vertices have at least (8/10)n common neighbours — Dross's Tₑ ≥ n − 2δn bound (δ = 1/10).

theorem LeanPool.DrossFractionalTriangleDecomposition.numK4_lower {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (h : 9 * Fintype.card V ≤ 10 * G.minDegree) {u v : V} (huv : G.Adj u v) : ↑(triThrough G s(u, v)) * (↑(triThrough G s(u, v)) - ↑(Fintype.card V) / 10) ≤ 2 * ↑(numK4Through G u v)

A6 in real form, per edge. For an edge uv, the K₄ count through it dominates Tₑ(Tₑ − n/10)/2 (Tₑ = triThrough). Combines A6 (k4_lower_bound), triThrough_edge, and the codegree bound, with the Nat→ℝ casting justified by codeg ≥ d.

theorem LeanPool.DrossFractionalTriangleDecomposition.numK4_lower_delta {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (h : 9 * Fintype.card V ≤ 10 * G.minDegree) (δ : ℝ) (hδ_deg : ↑(Fintype.card V) - ↑G.minDegree ≤ δ * ↑(Fintype.card V)) {u v : V} (huv : G.Adj u v) : ↑(triThrough G s(u, v)) * (↑(triThrough G s(u, v)) - δ * ↑(Fintype.card V)) ≤ 2 * ↑(numK4Through G u v)

A6 in real form, per edge, with an arbitrary deficiency δ. Generalises numK4_lower: for any δ bounding the max non-degree ratio (n − minDegree ≤ δ·n), Tₑ(Tₑ − δn) ≤ 2·numK4Through. Used with the tighter δ = 1/10 − ε in the ε-reparametrisation.

theorem LeanPool.DrossFractionalTriangleDecomposition.triThrough_bounds {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (h : 9 * Fintype.card V ≤ 10 * G.minDegree) {u v : V} (huv : G.Adj u v) : 8 / 10 * ↑(Fintype.card V) ≤ ↑(triThrough G s(u, v)) ∧ ↑(triThrough G s(u, v)) ≤ ↑(Fintype.card V)

Per-edge Tₑ bounds. In a dense graph, every edge lies in between (8/10)n and n triangles.

theorem LeanPool.DrossFractionalTriangleDecomposition.triThrough_bounds_delta {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (δ : ℝ) (hδ_deg : ↑(Fintype.card V) - ↑G.minDegree ≤ δ * ↑(Fintype.card V)) {u v : V} (huv : G.Adj u v) : (1 - 2 * δ) * ↑(Fintype.card V) ≤ ↑(triThrough G s(u, v)) ∧ ↑(triThrough G s(u, v)) ≤ ↑(Fintype.card V)

Per-edge Tₑ bounds with an arbitrary deficiency δ. Tₑ ∈ [(1−2δ)n, n] from codeg ≥ 2·minDegree − n ≥ (1−2δ)n. Used in the ε-reparametrisation (tighter than 0.8n).