Weighted Kernel Identity

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

theorem CKN.Foundation.Measure.div_ofReal_half_mul_ofReal_rpow_sub_one {C A : ENNReal} {t p : ℝ} (ht : 0 < t) : C / ENNReal.ofReal (t / 2) * A * ENNReal.ofReal (t ^ (p - 1)) = 2 * C * (ENNReal.ofReal (t ^ (p - 2)) * A)

An algebraic identity in extended reals used in the strong-type maximal estimates: rewriting C / (t/2) * A * t^(p-1) as 2*C * (t^(p-2) * A).