Gradient energy bounds for the two-reflection extension

The chain rule and the operator-norm estimates from SeeleyBounds are combined with the pullback estimates from SeeleyEnergy.

theorem CKN.seeley_fderiv_norm_le_three_classicalGradient (f : Vec 3 → ℝ) (x : Vec 3) : ‖fderiv ℝ f x‖ ≤ 3 * ‖classicalGradient f x‖

theorem CKN.seeleyExtension_gradient_energy_le (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) : ∫⁻ (x : Vec 3) in seeleyOuterAnnulus, ENNReal.ofReal (‖classicalGradient (seeleyExtension v) x‖ ^ 2) ≤ (2 * 675 ^ 2 * 64 + 2 * 3042 ^ 2 * 648) * ∫⁻ (y : Vec 3) in euclideanClosedBall 0 1, ENNReal.ofReal (‖classicalGradient v y‖ ^ 2)