Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.BlowupLimitAssemblyPressureScaling

Spatial rescaling of the pressure Poisson identity #

The distributional identity -Δ P = ∂_i ∂_j F_ij is invariant under the spatial rescaling P ↦ r² P(x₀ + r ·), F ↦ r² F(x₀ + r ·). This is the scaling identity p₁^k = P[v^k ⊗ v^k] used in prop:blowup-limit.

source
theorem ESS.blowupLimitAssemblyPressure_integral_comp_affine (g : CKN.Foundation.Parabolic.Vec3 → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) :
∫ (x : CKN.Foundation.Parabolic.Vec3), g (x₀ + r • x) = (r ^ 3)⁻¹ * ∫ (y : CKN.Foundation.Parabolic.Vec3), g y

Change of variables along a positive spatial dilation and translation.

source
theorem ESS.blowupLimitAssemblyPressure_spatialDeriv_affine (g : CKN.Foundation.Parabolic.Vec3 → ℝ) (hg : Differentiable ℝ g) (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (j : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) :
CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => g (r⁻¹ • (y - x₀))) j y = r⁻¹ * CKN.spatialDeriv g j (r⁻¹ • (y - x₀))

First coordinate derivatives along the inverse affine map.

source
theorem ESS.blowupLimitAssemblyPressure_spatialDeriv_const_mul (G : CKN.Foundation.Parabolic.Vec3 → ℝ) {y : CKN.Foundation.Parabolic.Vec3} (hG : DifferentiableAt ℝ G y) (c : ℝ) (i : Fin 3) :
CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => c * G y) i y = c * CKN.spatialDeriv G i y

A constant factor passes through a coordinate derivative.

source
theorem ESS.blowupLimitAssemblyPressure_mixedSecond_affine (g : CKN.Foundation.Parabolic.Vec3 → ℝ) (hg : ContDiff ℝ (↑⊤) g) (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (i j : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) :
CKN.mixedSecond (fun (y : CKN.Foundation.Parabolic.Vec3) => g (r⁻¹ • (y - x₀))) i j y = r⁻¹ ^ 2 * CKN.mixedSecond g i j (r⁻¹ • (y - x₀))

Second coordinate derivatives along the inverse affine map.

source
theorem ESS.blowupLimitAssemblyPressure_laplacian_affine (g : CKN.Foundation.Parabolic.Vec3 → ℝ) (hg : ContDiff ℝ (↑⊤) g) (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (y : CKN.Foundation.Parabolic.Vec3) :
CKN.spatialLaplacian (fun (y : CKN.Foundation.Parabolic.Vec3) => g (r⁻¹ • (y - x₀))) y = r⁻¹ ^ 2 * CKN.spatialLaplacian g (r⁻¹ • (y - x₀))

The spatial Laplacian along the inverse affine map.

source
theorem ESS.blowupLimitAssemblyPressure_poisson_rescale {P : CKN.Foundation.Parabolic.Vec3 → ℝ} {F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (h : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : CKN.Foundation.Parabolic.Vec3), P x * -CKN.spatialLaplacian ψ x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), F i j x * CKN.mixedSecond ψ i j x) (x₀ : CKN.Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ) :
ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : CKN.Foundation.Parabolic.Vec3), r ^ 2 * P (x₀ + r • x) * -CKN.spatialLaplacian ψ x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), r ^ 2 * F i j (x₀ + r • x) * CKN.mixedSecond ψ i j x

The pressure Poisson identity on a time slice is invariant under the spatial parabolic rescaling.