Finite-coordinate characterization of weak derivatives

Weak differentiation of a function with finite-dimensional real normed codomain is equivalent to weak differentiation of its scalar coordinates in any finite basis. Each direction includes local integrability and the distributional identity for every scalar coordinate, for any measure and open set, including a zero-dimensional codomain. For an arbitrary complete codomain, a locally integrable candidate is a weak derivative as soon as its images under all continuous linear functionals are, since these separate points (Hahn–Banach).

Main declarations

• hasWeakLineDerivOn_iff_coordinates: directional weak derivatives in scalar coordinates.
• hasWeakFDerivOn_iff_coordinates: the corresponding Fréchet weak derivative criterion.
• hasWeakLineDerivOn_of_forall_strongDual, hasWeakFDerivOn_of_forall_strongDual: the criteria by continuous linear functionals, for any complete codomain.

References

• L. C. Evans, Partial Differential Equations, Chapter 5, §5.2.

theorem TauCeti.hasWeakLineDerivOn_iff_coordinates {E : Type u_1} {F : Type u_2} {ι : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [Finite ι] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} (b : Module.Basis ι ℝ F) {u u' : E → F} {v : E} : HasWeakLineDerivOn μ Ω u u' v ↔ ∀ (i : ι), HasWeakLineDerivOn μ Ω (fun (x : E) => (b.coord i) (u x)) (fun (x : E) => (b.coord i) (u' x)) v

Weak directional differentiation with finite-dimensional codomain is equivalent to weak differentiation of all scalar coordinates.

theorem TauCeti.hasWeakFDerivOn_iff_coordinates {E : Type u_1} {F : Type u_2} {ι : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [Finite ι] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} (b : Module.Basis ι ℝ F) {u : E → F} {D : E → E →L[ℝ] F} : HasWeakFDerivOn μ Ω u D ↔ ∀ (i : ι), HasWeakFDerivOn μ Ω (fun (x : E) => (b.coord i) (u x)) fun (x : E) => LinearMap.toContinuousLinearMap (b.coord i) ∘SL D x

A finite-dimensional weak Fréchet derivative is detected by scalar coordinates in any finite basis of the codomain.

theorem TauCeti.hasWeakLineDerivOn_of_forall_strongDual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] {u u' : E → G} {v : E} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hu' : MeasureTheory.LocallyIntegrableOn u' (↑Ω) μ) (h : ∀ (ℓ : StrongDual ℝ G), HasWeakLineDerivOn μ Ω (fun (x : E) => ℓ (u x)) (fun (x : E) => ℓ (u' x)) v) : HasWeakLineDerivOn μ Ω u u' v

Continuous linear functionals detect weak directional derivatives: for locally integrable u and u' with complete codomain, it suffices that ℓ ∘ u' be a weak derivative of ℓ ∘ u for every ℓ. No finite-dimensionality is needed.

theorem TauCeti.hasWeakFDerivOn_of_forall_strongDual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] {u : E → G} {D : E → E →L[ℝ] G} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hD : ∀ (v : E), MeasureTheory.LocallyIntegrableOn (fun (x : E) => (D x) v) (↑Ω) μ) (h : ∀ (ℓ : StrongDual ℝ G), HasWeakFDerivOn μ Ω (fun (x : E) => ℓ (u x)) fun (x : E) => ℓ ∘SL D x) : HasWeakFDerivOn μ Ω u D

Continuous linear functionals detect weak Fréchet derivatives with complete codomain, given local integrability of the function and of each directional component of the candidate.