Spatial change of variables in the blow-up pairing #
The source momentum flux against the pulled-back test is exactly the rescaled momentum flux against the original test on its compact support.
noncomputable def
ESS.blowupLimitPairingSpatialPullback
(x₀ : CKN.Foundation.Parabolic.Vec3)
(r : ℝ)
(w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3)
:
The source test associated with a spatially rescaled compact test.
Equations
- ESS.blowupLimitPairingSpatialPullback x₀ r w y = CKN.weakContL3OfLp (w (r⁻¹ • (y - x₀)))
Instances For
theorem
ESS.blowup_limit_rescaled_momentum_flux_spatial_integral
{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 → ℝ}
{w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3}
{C : Set CKN.Foundation.Parabolic.Vec3}
(hwsupport : tsupport w ⊆ C)
(hC : IsCompact C)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ r t : ℝ)
(hr : 0 < r)
(himage : (fun (x : CKN.Foundation.Parabolic.Vec3) => x₀ + r • x) '' C ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))
(htime : t₀ + r ^ 2 * t ∈ Set.Ioo (-1) 0)
:
∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ∑ i : Fin 3,
∑ j : Fin 3,
u (y, t₀ + r ^ 2 * t) i * u (y, t₀ + r ^ 2 * t) j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => blowupLimitPairingSpatialPullback x₀ r w z i)
j y - ∑ i : Fin 3,
∑ j : Fin 3,
Du (y, t₀ + r ^ 2 * t) i j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => blowupLimitPairingSpatialPullback x₀ r w z i)
j y + p (y, t₀ + r ^ 2 * t) * ∑ i : Fin 3,
CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => blowupLimitPairingSpatialPullback x₀ r w z i) i
y = ∫ (x : CKN.Foundation.Parabolic.Vec3) in C, ∑ i : Fin 3,
∑ j : Fin 3,
blowupVelocity x₀ t₀ r u (x, t) i * blowupVelocity x₀ t₀ r u (x, t) j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => (w z).ofLp i) j x - ∑ i : Fin 3,
∑ j : Fin 3,
blowupGradient x₀ t₀ r Du (x, t) i j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => (w z).ofLp i) j x + blowupPressure x₀ t₀ r p (x, t) * ∑ i : Fin 3, CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => (w z).ofLp i) i x
The source spatial momentum-flux integral against the pulled-back test equals the rescaled flux integral over the compact support.