Mollifier contraction for weak Sobolev data #
The restart datum is an H^m equivalence class, not a smooth field.
Transporting each weak derivative through convolution gives the same
scale-independent ordered Sobolev contraction at the initial time.
theorem
ESS.lps_wordDeriv_convolution_weak_family
{κ f : CKN.Foundation.Parabolic.Vec3 → ℝ}
{D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ}
(hκ : ContDiff ℝ (↑⊤) κ)
(hκc : HasCompactSupport κ)
{m : ℕ}
(hD : CKN.IsSobolevFamilyOn m Set.univ f D)
(α : List (Fin 3))
(hα : α.length ≤ m)
:
Every ordered classical derivative of the mollified base field is
convolution of the corresponding specified weak derivative
(eq:lps-Hm-energy).
theorem
ESS.lps_sobolevNormSq_convolution_weak_le
{κ f : CKN.Foundation.Parabolic.Vec3 → ℝ}
{D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ}
(hκ : ContDiff ℝ (↑⊤) κ)
(hκc : HasCompactSupport κ)
(hκnonneg : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 ≤ κ x)
(hκone : ∫ (x : CKN.Foundation.Parabolic.Vec3), κ x = 1)
{m : ℕ}
(hD : CKN.IsSobolevFamilyOn m Set.univ f D)
:
(CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) =>
CKN.wordDeriv α (MeasureTheory.convolution κ (D []) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)) ≤ CKN.sobolevNormSqOn m Set.univ D
Normalized convolution contracts the full ordered H^m energy
of a weak Sobolev family (eq:lps-Hm-energy).
theorem
ESS.lps_sobolevNormSq_convolution_weak_input_le
{κ f : CKN.Foundation.Parabolic.Vec3 → ℝ}
{D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ}
(hκ : ContDiff ℝ (↑⊤) κ)
(hκc : HasCompactSupport κ)
(hκnonneg : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 ≤ κ x)
(hκone : ∫ (x : CKN.Foundation.Parabolic.Vec3), κ x = 1)
{m : ℕ}
(hD : CKN.IsSobolevFamilyOn m Set.univ f D)
:
(CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) =>
CKN.wordDeriv α (MeasureTheory.convolution κ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)) ≤ CKN.sobolevNormSqOn m Set.univ D
Replacing the Sobolev family's order-zero representative by its
underlying field leaves the mollification unchanged and preserves
the H^m contraction (eq:lps-Hm-energy).