L¹ estimates for the two-reflection extension

These estimates are the endpoint companions of the established quadratic Seeley energy bounds. They are used to control the value and derivative terms after the compactly supported cutoff is applied to a mean-subtracted function.

theorem CKN.seeleyReflectionOne_lintegral_comp_le_l1 (g : Vec 3 → ENNReal) : ∫⁻ (x : Vec 3) in seeleyClosedAnnulus, g (seeleyReflectionOne x) ≤ 64 * ∫⁻ (y : Vec 3) in euclideanClosedBall 0 1, g y

theorem CKN.seeleyReflectionTwo_lintegral_comp_le_l1 (g : Vec 3 → ENNReal) : ∫⁻ (x : Vec 3) in seeleyClosedAnnulus, g (seeleyReflectionTwo x) ≤ 648 * ∫⁻ (y : Vec 3) in euclideanClosedBall 0 1, g y

theorem CKN.seeleyReflectionOne_value_lintegral_le (v : Vec 3 → ℝ) (c : ℝ) : ∫⁻ (x : Vec 3) in seeleyClosedAnnulus, ENNReal.ofReal |v (seeleyReflectionOne x) - c| ≤ 64 * ∫⁻ (y : Vec 3) in euclideanClosedBall 0 1, ENNReal.ofReal |v y - c|

theorem CKN.seeleyReflectionTwo_value_lintegral_le (v : Vec 3 → ℝ) (c : ℝ) : ∫⁻ (x : Vec 3) in seeleyClosedAnnulus, ENNReal.ofReal |v (seeleyReflectionTwo x) - c| ≤ 648 * ∫⁻ (y : Vec 3) in euclideanClosedBall 0 1, ENNReal.ofReal |v y - c|

theorem CKN.seeleyReflectionOne_comp_fderiv_norm_le_l1 (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) {x : Vec 3} (hx : x ∈ seeleyClosedAnnulus) : ‖fderiv ℝ (v ∘ seeleyReflectionOne) x‖ ≤ 25 * ‖fderiv ℝ v (seeleyReflectionOne x)‖

theorem CKN.seeleyReflectionTwo_comp_fderiv_norm_le_l1 (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) {x : Vec 3} (hx : x ∈ seeleyClosedAnnulus) : ‖fderiv ℝ (v ∘ seeleyReflectionTwo) x‖ ≤ 169 * ‖fderiv ℝ v (seeleyReflectionTwo x)‖