Admissibility

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

The De Giorgi admissibility algebra

The scalar inequality feeding deGiorgi_levelVolume_tendsto_zero's hKcond. With α = q/2, β = α − 1, B = 4^α, Crec = C_F²·E₀², K = Cd·L·E₀, Ld = L^d, and the critical-exponent relation d·β = 2·α (equivalently q = 2d/(d−2)), the powers of L and E₀ cancel and the admissibility condition reduces to a choice of Cd ≥ C_F·B^{1/(2β)}.

theorem HCPolySupport.deGiorgi_admissible {d : ℕ} {C_F E₀ L Cd α β : ℝ} (hα : 0 < α) (hβ : 0 < β) (hβeq : β = α - 1) (hB : ↑d * β = 2 * α) (hCF : 0 ≤ C_F) (hE₀ : 0 < E₀) (hL : 0 < L) (hCd : 0 < Cd) (hchoice : C_F * (4 ^ α) ^ (1 / (2 * β)) ≤ Cd) : (C_F ^ 2 * E₀ ^ 2 / (Cd * L * E₀) ^ 2) ^ α * 4 ^ α * (L ^ d) ^ β ≤ (4 ^ α) ^ (-(1 / β))

Admissibility algebra. Given the critical relation (d:ℝ)·β = 2·α (with α, β > 0, β = α − 1), B = 4^α, and Cd ≥ C_F·B^{1/(2β)} with Cd > 0, C_F ≥ 0, E₀ > 0, L > 0, the De Giorgi leading constant is admissible: ((C_F²·E₀²)/(Cd·L·E₀)²)^α · B · (L^d)^β ≤ B^{−(1/β)}.