Scaling Invariance

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

noncomputable def CKN.scalingHomeomorph (μ : ℝ) (hμ : 0 < μ) (z₀ : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.Vec3 × ℝ ≃ₜ Foundation.Parabolic.Vec3 × ℝ

Space-time homeomorphism implementing positive parabolic scaling and translation.

Equations

• CKN.scalingHomeomorph μ hμ z₀ = ((Homeomorph.smulOfNeZero μ ⋯).trans (Homeomorph.addLeft z₀.1)).prodCongr ((Homeomorph.smulOfNeZero (μ ^ 2) ⋯).trans (Homeomorph.addLeft z₀.2))

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

Spatial dilation and translation as a homeomorphism.

Equations

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

noncomputable def CKN.temporalHomeomorph (μ : ℝ) (hμ : 0 < μ) (t₀ : ℝ) : ℝ ≃ₜ ℝ

Quadratic time dilation and translation as a homeomorphism.

Equations

• CKN.temporalHomeomorph μ hμ t₀ = (Homeomorph.smulOfNeZero (μ ^ 2) ⋯).trans (Homeomorph.addLeft t₀)

theorem CKN.isSuitableWeakSolutionIntegrable_rescale {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (z₀ : Foundation.Parabolic.ParabolicPoint) {μ : ℝ} (hμ : 0 < μ) : IsSuitableWeakSolutionIntegrable (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I) q (rescaleVelocity μ z₀ u) (rescaleGradient μ z₀ Du) (rescalePressure μ z₀ p) (rescaleForce μ z₀ f)