Documentation

LeanPool.EscauriazaSereginSverak.LPS.LocalStrongKineticPairing

The slice pairing of a mollified equation #

For a fixed smooth compact kernel, pairing the mollified momentum equation with the mollified velocity gives the mollified energy identity: the Laplacian contributes minus the squared mollified gradient, the pressure drops out by the solenoidal condition, and the transport term remains as the pairing of the mollified quadratic tensor with the mollified gradient (prop:lps-local-strong).

source
theorem ESS.LPS.lps_conv_pair_ibp {η : CKN.Foundation.Parabolic.Vec3 → ℝ} (hη : CKN.IsVlKernel η) {h₁ h₂ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hh₁ : MeasureTheory.MemLp h₁ 2 MeasureTheory.volume) (hh₂ : MeasureTheory.MemLp h₂ 2 MeasureTheory.volume) (j : Fin 3) :
∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv (CKN.vlDeriv η j) h₁ x * CKN.vlConv η h₂ x = -∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv η h₁ x * CKN.vlConv (CKN.vlDeriv η j) h₂ x

Integration by parts moving the derivative from the kernel of the first factor to the kernel of the second.

source
theorem ESS.LPS.lps_slice_mollified_energy {η : CKN.Foundation.Parabolic.Vec3 → ℝ} (hη : CKN.IsVlKernel η) {U W : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} {G H F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} {P : CKN.Foundation.Parabolic.Vec3 → ℝ} (hU : ∀ (i : Fin 3), MeasureTheory.MemLp (U i) 2 MeasureTheory.volume) (hW : ∀ (i : Fin 3), MeasureTheory.MemLp (W i) 2 MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 MeasureTheory.volume) (hH : ∀ (i j : Fin 3), MeasureTheory.MemLp (H i j) 2 MeasureTheory.volume) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) 2 MeasureTheory.volume) (hP : MeasureTheory.MemLp P 2 MeasureTheory.volume) (hM : ∀ (i : Fin 3), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv η (W i) x + ∑ j : Fin 3, CKN.vlConv (CKN.vlDeriv η j) (F i j) x - ∑ j : Fin 3, CKN.vlConv η (H i j) x + CKN.vlConv (CKN.vlDeriv η i) P x = 0) (hG1 : ∀ (i j : Fin 3), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv (CKN.vlDeriv η j) (U i) x = CKN.vlConv η (G i j) x) (hH1 : ∀ (i j : Fin 3), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv (CKN.vlDeriv η j) (G i j) x = CKN.vlConv η (H i j) x) (hdiv : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.vlConv (CKN.vlDeriv η i) (U i) x = 0) :
∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv η (W i) x * CKN.vlConv η (U i) x = (∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv η (F i j) x * CKN.vlConv η (G i j) x) - ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv η (G i j) x ^ 2

The mollified energy identity on one time slice.

source
theorem ESS.LPS.lps_slice_energy_limit {U W : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} {G H F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} {P : CKN.Foundation.Parabolic.Vec3 → ℝ} (hU : ∀ (i : Fin 3), MeasureTheory.MemLp (U i) 2 MeasureTheory.volume) (hW : ∀ (i : Fin 3), MeasureTheory.MemLp (W i) 2 MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 MeasureTheory.volume) (hH : ∀ (i j : Fin 3), MeasureTheory.MemLp (H i j) 2 MeasureTheory.volume) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) 2 MeasureTheory.volume) (hP : MeasureTheory.MemLp P 2 MeasureTheory.volume) (hM : ∀ (n : ℕ) (i : Fin 3), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv (CKN.vlMoll n) (W i) x + ∑ j : Fin 3, CKN.vlConv (CKN.vlDeriv (CKN.vlMoll n) j) (F i j) x - ∑ j : Fin 3, CKN.vlConv (CKN.vlMoll n) (H i j) x + CKN.vlConv (CKN.vlDeriv (CKN.vlMoll n) i) P x = 0) (hG1 : ∀ (n : ℕ) (i j : Fin 3), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv (CKN.vlDeriv (CKN.vlMoll n) j) (U i) x = CKN.vlConv (CKN.vlMoll n) (G i j) x) (hH1 : ∀ (n : ℕ) (i j : Fin 3), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv (CKN.vlDeriv (CKN.vlMoll n) j) (G i j) x = CKN.vlConv (CKN.vlMoll n) (H i j) x) (hdiv : ∀ (n : ℕ), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.vlConv (CKN.vlDeriv (CKN.vlMoll n) i) (U i) x = 0) :
∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), W i x * U i x = (∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), F i j x * G i j x) - ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), G i j x ^ 2

The slice energy identity, in the limit of vanishing mollification.