Documentation

LeanPool.EscauriazaSereginSverak.LPS.SmoothingTransportEnergy

Ordered transport-energy pairing #

After one derivative is moved from the tensor divergence onto the energy test field, the transport term is controlled by the gradient energy and the tensor H^m energy.

source
theorem ESS.lps_ordered_transport_pairing_bound (m : ℕ) (hm : 2 ≤ m) :
∃ (C : ℝ), 0 ≤ C ∧ ∀ (v u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), (∀ (j : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) → (∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) → (∀ (j : Fin 3) (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) 2 MeasureTheory.volume) → (∀ (i : Fin 3) (α : List (Fin 3)), α.length ≤ m + 1 → MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) 2 MeasureTheory.volume) → have W := CKN.sobolevWords m; have Nv := ∑ j : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => v x j; have Nu := ∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i; have D := ∑ i : Fin 3, ∑ α ∈ W, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) x ^ 2; ∑ i : Fin 3, ∑ α ∈ W, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) x * CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j * u y i) x ≤ √D * √(C * Nv * Nu)

The differentiated transport tensor pairs against the velocity gradient with a scale-independent H^m bound (eq:lps-regularized-Hm-identity).

source
theorem ESS.lps_ordered_transport_pairing_contractive (m : ℕ) (hm : 2 ≤ m) :
∃ (C : ℝ), 0 ≤ C ∧ ∀ (v u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), (∀ (j : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) → (∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) → (∀ (j : Fin 3) (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) 2 MeasureTheory.volume) → (∀ (i : Fin 3) (α : List (Fin 3)), α.length ≤ m + 1 → MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) 2 MeasureTheory.volume) → have W := CKN.sobolevWords m; have Nv := ∑ j : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => v x j; have Nu := ∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i; have D := ∑ i : Fin 3, ∑ α ∈ W, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) x ^ 2; Nv ≤ Nu → ∑ i : Fin 3, ∑ α ∈ W, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) x * CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j * u y i) x ≤ √C * Nu * √D

Contracting the transport velocity in H^m turns the tensor estimate into the quadratic coefficient of the corrected energy inequality (eq:lps-Hm-energy).