Documentation

LeanPool.EscauriazaSereginSverak.LPS.SmoothingHeatPairing

Whole-space heat pairing for high-order smoothing #

For a smooth scalar derivative of the regularized velocity, integration by parts converts the Laplacian pairing into its coordinate-gradient energy. This is the dissipative term of eq:lps-regularized-Hm-identity.

source
theorem ESS.lps_heat_pairing_direction {h : CKN.Foundation.Parabolic.Vec3 → ℝ} (hh : ContDiff ℝ (↑⊤) h) (j : Fin 3) (h0 : MeasureTheory.MemLp h 2 MeasureTheory.volume) (h1 : MeasureTheory.MemLp (CKN.spatialDeriv h j) 2 MeasureTheory.volume) (h2 : MeasureTheory.MemLp (CKN.spatialDeriv (CKN.spatialDeriv h j) j) 2 MeasureTheory.volume) :
∫ (x : CKN.Foundation.Parabolic.Vec3), h x * CKN.spatialDeriv (CKN.spatialDeriv h j) j x = -∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv h j x ^ 2

A scalar whole-space heat pairing dissipates the square of one coordinate derivative (eq:lps-regularized-Hm-identity).

source
theorem ESS.lps_heat_pairing_laplacian {h : CKN.Foundation.Parabolic.Vec3 → ℝ} (hh : ContDiff ℝ (↑⊤) h) (h0 : MeasureTheory.MemLp h 2 MeasureTheory.volume) (h1 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv h j) 2 MeasureTheory.volume) (h2 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (CKN.spatialDeriv h j) j) 2 MeasureTheory.volume) :
∫ (x : CKN.Foundation.Parabolic.Vec3), h x * ∑ j : Fin 3, CKN.spatialDeriv (CKN.spatialDeriv h j) j x = -∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv h j x ^ 2

Summing the coordinate heat pairings yields the full spatial-gradient dissipation (eq:lps-regularized-Hm-identity).

source
theorem ESS.lps_divergence_pairing_direction {h F : CKN.Foundation.Parabolic.Vec3 → ℝ} (hh : ContDiff ℝ (↑⊤) h) (hF : ContDiff ℝ (↑⊤) F) (j : Fin 3) (hh0 : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hh1 : MeasureTheory.MemLp (CKN.spatialDeriv h j) 2 MeasureTheory.volume) (hF0 : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hF1 : MeasureTheory.MemLp (CKN.spatialDeriv F j) 2 MeasureTheory.volume) :
∫ (x : CKN.Foundation.Parabolic.Vec3), h x * CKN.spatialDeriv F j x = -∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv h j x * F x

A smooth whole-space divergence term transfers one derivative to the energy test field (eq:lps-regularized-Hm-identity).