Documentation

LeanPool.EscauriazaSereginSverak.LPS.SmoothingSobolevProductHigh

High-order whole-space Sobolev product estimate #

At integer order at least three, every Leibniz term has a factor with at least two derivatives to spare. Whole-space H² → L∞ therefore bounds the product in the ordered Sobolev energy.

source
theorem ESS.lps_smooth_leibniz_normSq_high (m : ℕ) (hm : 3 ≤ m) :
∃ (C : ℝ), 0 ≤ C ∧ ∀ (f g : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) f → ContDiff ℝ (↑⊤) g → (∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) → (∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv α g) 2 MeasureTheory.volume) → (∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.sobolevLeibnizFamily α (fun (β : List (Fin 3)) => CKN.wordDeriv β f) (fun (β : List (Fin 3)) => CKN.wordDeriv β g) x ^ 2) MeasureTheory.volume) ∧ (CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.sobolevLeibnizFamily α (fun (β : List (Fin 3)) => CKN.wordDeriv β f) fun (β : List (Fin 3)) => CKN.wordDeriv β g) ≤ (C * CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α f) * CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α g

The ordered Leibniz family of two smooth H^m functions has square-integrable derivatives through order m ≥ 3, with an H^m algebra bound (eq:lps-Hm-energy).

source
theorem ESS.lps_smooth_product_normSq_high (m : ℕ) (hm : 3 ≤ m) :
∃ (C : ℝ), 0 ≤ C ∧ ∀ (f g : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) f → ContDiff ℝ (↑⊤) g → (∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) → (∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv α g) 2 MeasureTheory.volume) → (∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) 2 MeasureTheory.volume) ∧ (CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) ≤ (C * CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α f) * CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α g

Smooth multiplication is bounded in the ordered whole-space H^m norm for every integer m ≥ 3 (eq:lps-Hm-energy).