Scaling Invariance Weak

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

noncomputable def CKN.weakSpatialHomeomorph (μ : ℝ) (hμ : 0 < μ) (x₀ : Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 ≃ₜ Foundation.Parabolic.Vec3

Spatial scaling homeomorphism used to transport weak derivatives.

Equations

• CKN.weakSpatialHomeomorph μ hμ x₀ = (Homeomorph.smulOfNeZero μ ⋯).trans (Homeomorph.addLeft x₀)

theorem CKN.hasWeakPartialDerivOn_scaling (μ : ℝ) (hμ : 0 < μ) (x₀ : Foundation.Parabolic.Vec3) {Ω Ω' : Set Foundation.Parabolic.Vec3} (hΩ : MeasurableSet Ω) {g dg : Foundation.Parabolic.Vec3 → ℝ} (j : Fin 3) (hΩeq : Ω = scalingSpace μ x₀ '' Ω') (hweak : HasWeakPartialDerivOn Ω j g dg) (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict Ω)) (hdg : MeasureTheory.AEStronglyMeasurable dg (MeasureTheory.volume.restrict Ω)) : HasWeakPartialDerivOn Ω' j (fun (x : Vec 3) => μ * g (scalingSpace μ x₀ x)) fun (x : Vec 3) => μ ^ 2 * dg (scalingSpace μ x₀ x)