Classical derivatives of smooth Sobolev representatives

A smooth representative of a weak Sobolev function has classical derivatives equal almost everywhere to its recorded weak derivatives. The nested iterated-gradient fields have exactly the same pointwise norms as Mathlib's multilinear derivatives. Consequently smooth Sobolev representatives satisfy the integrability hypotheses of classical higher-order cutoff estimates.

The weak-to-classical identification uses TauCeti.HasWeakFDerivOn.ae_eq_fderiv; the norm comparison uses Mathlib's norm_iteratedFDeriv_fderiv and the Riesz isometry. These are the identifications used in smooth approximation in Evans, Partial Differential Equations, §5.3.1.

theorem TauCeti.norm_iteratedFDeriv_iteratedGradientChain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (i k : ℕ) (x : E) : ‖iteratedFDeriv ℝ i (iteratedGradientChain f k) x‖ = ‖iteratedFDeriv ℝ (i + k + 1) f x‖

Taking i further derivatives of the kth iterated-gradient field has the same norm as taking i + k + 1 derivatives of the original scalar function. No smoothness is needed.

@[simp]

theorem TauCeti.norm_iteratedGradientChain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (k : ℕ) (x : E) : ‖iteratedGradientChain f k x‖ = ‖iteratedFDeriv ℝ (k + 1) f x‖

The nested iterated-gradient field has the same norm as the corresponding multilinear derivative of the scalar function.

@[simp]

theorem TauCeti.iteratedGradientChain_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g : E → ℝ} {x : E} (k : ℕ) (hf : ContDiffAt ℝ (↑k + 1) f x) (hg : ContDiffAt ℝ (↑k + 1) g x) : iteratedGradientChain (f - g) k x = iteratedGradientChain f k x - iteratedGradientChain g k x

Iterated-gradient fields through order k + 1 preserve subtraction of scalar functions that are C^{k+1} at the point of evaluation.

theorem TauCeti.norm_iteratedGradientChain_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g : E → ℝ} {x : E} (k : ℕ) (hf : ContDiffAt ℝ (↑k + 1) f x) (hg : ContDiffAt ℝ (↑k + 1) g x) : ‖iteratedGradientChain f k x - iteratedGradientChain g k x‖ = ‖iteratedFDeriv ℝ (k + 1) f x - iteratedFDeriv ℝ (k + 1) g x‖

The order-k + 1 iterated-gradient fields of two scalar functions that are C^{k+1} at a point have the same difference norm there as their multilinear derivatives. This identifies the error seminorms in smooth approximation.

theorem TauCeti.Wkp.iteratedGradient_ae_eq_of_contDiffOn {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) (u : Wkp mu Omega p (k + 1)) {f : E → ℝ} (hf : ContDiffOn ℝ (↑k + 1) f ↑Omega) (hu : ↑↑(value (k + 1) u) =ᵐ[mu.restrict ↑Omega] f) : ↑↑(iteratedGradient k u) =ᵐ[mu.restrict ↑Omega] iteratedGradientChain f k

The highest recorded weak derivative of a Sobolev representative that is C^{k+1} on the domain is its classical iterated-gradient field almost everywhere there.

theorem TauCeti.Wkp.memLp_iteratedFDeriv_of_contDiffOn {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (k : ℕ) (u : Wkp mu Omega p k) {f : E → ℝ} (hf : ContDiffOn ℝ (↑k) f ↑Omega) (hu : ↑↑(value k u) =ᵐ[mu.restrict ↑Omega] f) (i : ℕ) : i ≤ k → MeasureTheory.MemLp (iteratedFDeriv ℝ i f) p (mu.restrict ↑Omega)

Every classical derivative through order k of a W^{k,p} representative that is C^k on the domain belongs to Lᵖ there.