Smooth representatives of all-order weak families

lem:lps-Bochner-joint-smooth: a whole-space function whose weak derivative family exists to every order has a C^∞ representative, and the sup norm of each ordered derivative is controlled by the Sobolev norm of the family.

noncomputable def ESS.lpsEmbC (k : ℕ) : ℝ

The embedding constant of lps_sobolevFamily_contDiff_rep at order k.

Equations

• ESS.lpsEmbC k = Classical.choose ⋯

theorem ESS.lpsEmbC_nonneg (k : ℕ) : 0 ≤ lpsEmbC k

theorem ESS.lps_eq_of_continuous_ae_eq {g₁ g₂ : CKN.Foundation.Parabolic.Vec3 → ℝ} (h₁ : Continuous g₁) (h₂ : Continuous g₂) (h : g₁ =ᵐ[MeasureTheory.volume] g₂) : g₁ = g₂

Two continuous functions that agree almost everywhere agree everywhere.

theorem ESS.lps_sobolevFamily_smooth_rep {f : CKN.Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (h : ∀ (m : ℕ), CKN.IsSobolevFamilyOn m Set.univ f D) : ∃ (g : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) g ∧ g =ᵐ[MeasureTheory.volume] f ∧ (∀ (α : List (Fin 3)), CKN.wordDeriv α g =ᵐ[MeasureTheory.volume] D α) ∧ ∀ (k : ℕ) (α : List (Fin 3)), α.length ≤ k → ∀ (x : CKN.Foundation.Parabolic.Vec3), |CKN.wordDeriv α g x| ≤ lpsEmbC k * √(CKN.sobolevNormSqOn (k + 2) Set.univ D)

lem:lps-Bochner-joint-smooth: a function with weak families of every order has a C^∞ representative whose ordered derivatives represent the family, with sup norms controlled by the Sobolev norm at each order.