Scaling Invariance S3 S4

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

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

Space-time scaling homeomorphism used for momentum and local energy transport.

Equations

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

theorem CKN.s3_rescale {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {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} (hΩ : MeasurableSet Ω) (hI : MeasurableSet I) (hS3 : ∀ φ ∈ spaceTimeTestFunction Ω I, MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => -∑ i : Fin 3, u z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z - ∑ i : Fin 3, f z i * φ z i) (tsupport φ) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, -∑ i : Fin 3, u z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z - ∑ i : Fin 3, f z i * φ z i = 0) (z₀ : Foundation.Parabolic.ParabolicPoint) {μ : ℝ} (hμ : 0 < μ) (φ : Foundation.Parabolic.Vec3 × ℝ → 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 * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, rescaleVelocity μ z₀ u z i * rescaleVelocity μ z₀ u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, rescaleGradient μ z₀ Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z - rescalePressure μ z₀ p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z - ∑ i : Fin 3, rescaleForce μ z₀ f z i * φ z i) (tsupport φ) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I), -∑ i : Fin 3, rescaleVelocity μ z₀ u z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, rescaleVelocity μ z₀ u z i * rescaleVelocity μ z₀ u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, rescaleGradient μ z₀ Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z - rescalePressure μ z₀ p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z - ∑ i : Fin 3, rescaleForce μ z₀ f z i * φ z i = 0

theorem CKN.s4_rescale {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {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} (hΩ : MeasurableSet Ω) (hI : MeasurableSet I) (hS4 : ∀ ψ ∈ spaceTimeTestFunction Ω I, (∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ ψ z) → MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialGradientSq u Du z * ψ z) (tsupport ψ) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + (Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 + 2 * p z) * ∑ i : Fin 3, u z i * spatialPartial ψ i z + (2 * ∑ i : Fin 3, f z i * u z i) * ψ z) (tsupport ψ) MeasureTheory.volume ∧ 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, spatialGradientSq u Du z * ψ z ≤ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + (Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 + 2 * p z) * ∑ i : Fin 3, u z i * spatialPartial ψ i z + (2 * ∑ i : Fin 3, f z i * u z i) * ψ z) (z₀ : Foundation.Parabolic.ParabolicPoint) {μ : ℝ} (hμ : 0 < μ) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) : ψ ∈ spaceTimeTestFunction (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I) → (∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ ψ z) → MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialGradientSq (rescaleVelocity μ z₀ u) (rescaleGradient μ z₀ Du) z * ψ z) (tsupport ψ) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (rescaleVelocity μ z₀ u z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + (Foundation.Parabolic.vec3EuclideanNorm (rescaleVelocity μ z₀ u z) ^ 2 + 2 * rescalePressure μ z₀ p z) * ∑ i : Fin 3, rescaleVelocity μ z₀ u z i * spatialPartial ψ i z + (2 * ∑ i : Fin 3, rescaleForce μ z₀ f z i * rescaleVelocity μ z₀ u z i) * ψ z) (tsupport ψ) MeasureTheory.volume ∧ 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I), spatialGradientSq (rescaleVelocity μ z₀ u) (rescaleGradient μ z₀ Du) z * ψ z ≤ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I), Foundation.Parabolic.vec3EuclideanNorm (rescaleVelocity μ z₀ u z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + (Foundation.Parabolic.vec3EuclideanNorm (rescaleVelocity μ z₀ u z) ^ 2 + 2 * rescalePressure μ z₀ p z) * ∑ i : Fin 3, rescaleVelocity μ z₀ u z i * spatialPartial ψ i z + (2 * ∑ i : Fin 3, rescaleForce μ z₀ f z i * rescaleVelocity μ z₀ u z i) * ψ z