Elementary positivity, normalization, and norm-power identities for the smoothing kernel.

theorem V7.Stage5AboveTwoLower.lowerKernelPhi_eq_norm_power {d : ℕ} {r0 theta : ℝ} (hr0 : r0 ≠ 0) (x : Point d) : lowerKernelPhi r0 theta x = 2 * lpNorm r0 x ^ (2 * theta)

theorem V7.Stage5AboveTwoLower.lowerKernelPhi_nonneg {d : ℕ} {r0 theta : ℝ} (x : Point d) : 0 ≤ lowerKernelPhi r0 theta x

theorem V7.Stage5AboveTwoLower.lowerKernelPhi_zero {d : ℕ} {r0 theta : ℝ} (hr0 : 0 < r0) (htheta : 0 < theta) : lowerKernelPhi r0 theta 0 = 0

theorem V7.Stage5AboveTwoLower.lowerKernelPhi_strict_of_one_lt_norm_power {d : ℕ} {r0 theta : ℝ} (hr0 : 0 < r0) (x : Point d) (hx : 1 < lpNorm r0 x ^ (2 * theta)) : 1 < lowerKernelPhi r0 theta x