Suitable solutions under parabolic rescaling

These fields use the translation and scaling convention of CKN's rescaling definition. Suitability is transported on arbitrary product domains by CKN's scaling theorem.

def ESS.parabolicRescaleVelocity (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

Velocity after translating and parabolically scaling by r, as in manuscript label lem:thmA-rescaled.

Equations

• ESS.parabolicRescaleVelocity x₀ t₀ r u z = r • u (CKN.Foundation.Parabolic.parabolicTranslate x₀ t₀ (CKN.Foundation.Parabolic.parabolicScale r z))

def ESS.parabolicRescaleGradient (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3

Weak gradient after translating and parabolically scaling by r, as in manuscript label lem:thmA-rescaled.

Equations

• ESS.parabolicRescaleGradient x₀ t₀ r Du z i = r ^ 2 • Du (CKN.Foundation.Parabolic.parabolicTranslate x₀ t₀ (CKN.Foundation.Parabolic.parabolicScale r z)) i

def ESS.parabolicRescalePressure (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : CKN.Foundation.Parabolic.ParabolicPoint → ℝ

Pressure after translating and parabolically scaling by r, as in manuscript label lem:thmA-rescaled.

Equations

• ESS.parabolicRescalePressure x₀ t₀ r p z = r ^ 2 * p (CKN.Foundation.Parabolic.parabolicTranslate x₀ t₀ (CKN.Foundation.Parabolic.parabolicScale r z))

theorem ESS.isSuitableWeakSolution_parabolicRescale {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hSuitable : CKN.IsSuitableWeakSolution Ω I q u Du p f) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) : CKN.IsSuitableWeakSolution (CKN.rescaledSpace r x₀ Ω) (CKN.rescaledTime r t₀ I) q (parabolicRescaleVelocity x₀ t₀ r u) (parabolicRescaleGradient x₀ t₀ r Du) (parabolicRescalePressure x₀ t₀ r p) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => r ^ 3 • f (CKN.Foundation.Parabolic.parabolicTranslate x₀ t₀ (CKN.Foundation.Parabolic.parabolicScale r z))

Suitability is preserved under translation and parabolic scaling on an arbitrary product domain, as used in manuscript label lem:thmA-rescaled.

theorem ESS.rescaledTime_Ioi_zero (t₀ r : ℝ) (hr : 0 < r) : CKN.rescaledTime r t₀ (Set.Ioi 0) = Set.Ioi (-(t₀ / r ^ 2))

The positive-time interval pulls back to its translated and rescaled half-line.