Fields on rescaled past cylinders

The original velocity, weak gradient, and pressure are extended by zero from the source cylinder before parabolic rescaling, as in prop:blowup-limit.

def ESS.blowupDomain (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

The rescaled preimage of the original open cylinder (prop:blowup-limit).

Equations

• One or more equations did not get rendered due to their size.

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

The velocity after zero extension from the source cylinder and scaling.

Equations

• ESS.blowupVelocity x₀ t₀ r u = ESS.parabolicRescaleVelocity x₀ t₀ r (ESS.goodPointDomain.indicator u)

noncomputable def ESS.blowupGradient (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

The weak spatial gradient after zero extension and scaling.

Equations

• ESS.blowupGradient x₀ t₀ r Du = ESS.parabolicRescaleGradient x₀ t₀ r (ESS.goodPointDomain.indicator Du)

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

The pressure after zero extension from the source cylinder and scaling.

Equations

• ESS.blowupPressure x₀ t₀ r p = ESS.parabolicRescalePressure x₀ t₀ r (ESS.goodPointDomain.indicator p)

theorem ESS.blowupVelocity_eq_of_mem (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ blowupDomain x₀ t₀ r) : blowupVelocity x₀ t₀ r u z = r • u (CKN.Foundation.Parabolic.parabolicTranslate x₀ t₀ (CKN.Foundation.Parabolic.parabolicScale r z))

On the rescaled source domain, the velocity agrees with ordinary Navier--Stokes scaling.

theorem ESS.blowupGradient_eq_of_mem (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ blowupDomain x₀ t₀ r) : blowupGradient x₀ t₀ r Du z = fun (i : Fin 3) => r ^ 2 • Du (CKN.Foundation.Parabolic.parabolicTranslate x₀ t₀ (CKN.Foundation.Parabolic.parabolicScale r z)) i

On the rescaled source domain, the weak gradient agrees with ordinary Navier--Stokes scaling.

theorem ESS.blowupPressure_eq_of_mem (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ blowupDomain x₀ t₀ r) : blowupPressure x₀ t₀ r p z = r ^ 2 * p (CKN.Foundation.Parabolic.parabolicTranslate x₀ t₀ (CKN.Foundation.Parabolic.parabolicScale r z))

On the rescaled source domain, the pressure agrees with ordinary Navier--Stokes scaling.