Change-of-variables energy bounds for the two-reflection extension

The closed-annulus Jacobian lower bounds turn the exact change-of-variables identities into explicit pullback estimates. The statements are written for nonnegative extended-valued integrands, so no auxiliary measurability assumptions are needed at this stage.

def CKN.seeleyOuterAnnulus : Set (Vec 3)

The part of the closed annulus lying in the outer unit-ball shell.

Equations

• CKN.seeleyOuterAnnulus = {x : CKN.Vec 3 | 1 < CKN.vecEuclideanNorm x ∧ CKN.vecEuclideanNorm x < 2}

theorem CKN.seeleyOuterAnnulus_subset_closedAnnulus : seeleyOuterAnnulus ⊆ seeleyClosedAnnulus

theorem CKN.seeleyOuterAnnulus_measurableSet : MeasurableSet seeleyOuterAnnulus

theorem CKN.seeleyExtension_value_eq_reflection_combo (v : Vec 3 → ℝ) {x : Vec 3} (hx : x ∈ seeleyOuterAnnulus) : seeleyExtension v x = 3 * v (seeleyReflectionOne x) - 2 * v (seeleyReflectionTwo x)

theorem CKN.seeleyExtension_value_energy_le (v : Vec 3 → ℝ) (c : ℝ) (hv : Continuous v) : ∫⁻ (x : Vec 3) in seeleyOuterAnnulus, ENNReal.ofReal |seeleyExtension (fun (y : Vec 3) => v y - c) x| ^ 2 ≤ 6336 * ∫⁻ (y : Vec 3) in euclideanClosedBall 0 1, ENNReal.ofReal |v y - c| ^ 2