Quantitative bounds for the two-reflection extension

This file records the derivative and Jacobian estimates on the closed annulus. The constants are deliberately coarse absolute constants; their role is to make the change-of-variables estimates explicit.

theorem CKN.seeleyReflectionOne_fderiv_det_bounds {x : Vec 3} (hx : x ∈ seeleyClosedAnnulus) : 1 / 64 ≤ |(fderiv ℝ seeleyReflectionOne x).det| ∧ |(fderiv ℝ seeleyReflectionOne x).det| ≤ 1

theorem CKN.seeleyReflectionTwo_fderiv_det_bounds {x : Vec 3} (hx : x ∈ seeleyClosedAnnulus) : 1 / 648 ≤ |(fderiv ℝ seeleyReflectionTwo x).det| ∧ |(fderiv ℝ seeleyReflectionTwo x).det| ≤ 8

theorem CKN.seeleyReflectionOne_fderiv_norm_le {x : Vec 3} (hx : x ∈ seeleyClosedAnnulus) : ‖fderiv ℝ seeleyReflectionOne x‖ ≤ 25

theorem CKN.seeleyReflectionTwo_fderiv_norm_le {x : Vec 3} (hx : x ∈ seeleyClosedAnnulus) : ‖fderiv ℝ seeleyReflectionTwo x‖ ≤ 169

theorem CKN.seeleyReflectionOne_lintegral_comp_le (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 (g : Vec 3 → ENNReal) : ∫⁻ (x : Vec 3) in seeleyClosedAnnulus, g (seeleyReflectionTwo x) ≤ 648 * ∫⁻ (y : Vec 3) in euclideanClosedBall 0 1, g y