ENNReal Half Scale

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Measure.ofReal_mul_div_ofReal_half {A t : ℝ} (ht : 0 < t) (X : ENNReal) : ENNReal.ofReal A * X / ENNReal.ofReal (t / 2) = ENNReal.ofReal (2 * A / t) * X

For t > 0 and any extended nonnegative real X, ENNReal.ofReal A * X / ENNReal.ofReal (t/2) = ENNReal.ofReal (2*A/t) * X.

theorem CKN.Foundation.Measure.ofReal_mul_div_ofReal_half_sq {B t : ℝ} (ht : 0 < t) (X : ENNReal) : ENNReal.ofReal B * X / ENNReal.ofReal (t / 2) ^ 2 = ENNReal.ofReal (4 * B / t ^ 2) * X

For t > 0 and any extended nonnegative real X, ENNReal.ofReal B * X / (ENNReal.ofReal (t/2))^2 = ENNReal.ofReal (4*B/t^2) * X.