Seeley Scaling

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

def CKN.seeleyAffineMap (x₀ : Vec 3) (r : ℝ) (x : Vec 3) : Vec 3

Affine map transporting the unit ball to a ball centered at x₀ with scale r.

Equations

• CKN.seeleyAffineMap x₀ r x = x₀ + r • x

theorem CKN.seeleyAffine_eLpNorm_comp {x₀ : Vec 3} {r : ℝ} (hr : 0 < r) {β : Type u_1} [NormedAddCommGroup β] {f : Vec 3 → β} (hf : Continuous f) (p : ENNReal) : MeasureTheory.eLpNorm (f ∘ seeleyAffineMap x₀ r) p (MeasureTheory.volume.restrict (euclideanBall 0 1)) = ENNReal.ofReal (r⁻¹ ^ 3) ^ (1 / p).toReal * MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict (euclideanBall x₀ r))

theorem CKN.seeleyAffine_average {x₀ : Vec 3} {r : ℝ} (hr : 0 < r) {f : Vec 3 → ℝ} (hf : Continuous f) : MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall 0 1)) (f ∘ seeleyAffineMap x₀ r) = MeasureTheory.average (MeasureTheory.volume.restrict (euclideanBall x₀ r)) f

theorem CKN.seeleyAffine_classicalGradient {x₀ : Vec 3} {r : ℝ} {f : Vec 3 → ℝ} : ContDiff ℝ 1 f → ∀ (x : Vec 3), classicalGradient (f ∘ seeleyAffineMap x₀ r) x = r • classicalGradient f (seeleyAffineMap x₀ r x)