Documentation

LeanPool.CaffarelliKohnNirenberg.Core.Caccioppoli.CaccioppoliCenteredRhs

The scalar normalization used by the centered Caccioppoli estimate.

theorem CKN.caccioppoli_centered_rhs_eq {C r a b : ℝ} (hC : 0 ≤ C) (hr : 0 < r) (ha : 0 ≤ a) (hb : 0 ≤ b) :
ENNReal.ofReal C * ENNReal.ofReal (r * a ^ 2) ^ (1 / 2) * ENNReal.ofReal (r * b ^ 2) ^ (1 / 2) * ENNReal.ofReal (r ^ 2) ^ (1 / 6) = ENNReal.ofReal (C * r ^ (4 / 3) * a * b)