Scaling Invariance S2

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

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

Space-time scaling homeomorphism used for the divergence-free weak equation.

Equations

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

theorem CKN.s2_rescale {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hΩ : MeasurableSet Ω) (hI : MeasurableSet I) (hS2 : ∀ ψ ∈ spaceTimeTestFunction Ω I, MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, u z i * spatialPartial ψ i z) (tsupport ψ) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3, u z i * spatialPartial ψ i z = 0) (z₀ : Foundation.Parabolic.ParabolicPoint) {μ : ℝ} (hμ : 0 < μ) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) : ψ ∈ spaceTimeTestFunction (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I) → MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, rescaleVelocity μ z₀ u z i * spatialPartial ψ i z) (tsupport ψ) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I), ∑ i : Fin 3, rescaleVelocity μ z₀ u z i * spatialPartial ψ i z = 0