Second-order weak differentiability from directional derivatives

An element of W^{2,p}(Ω) is an element of W^{1,p}(Ω) together with an Lᵖ weak Fréchet derivative of its weak gradient. Checking that a given u ∈ W^{1,p}(Ω) has one means producing a single Lᵖ field of linear maps; this file reduces that to the componentwise data that a difference-quotient argument actually supplies, namely an Lᵖ weak derivative of each scalar component ⟪∇u, e_j⟫ in each basis direction e_i (TauCeti.W1p.exists_lowerOrder_eq_of_forall_hasWeakLineDerivOn).

The assembly is the obvious one: the candidate Hessian is x ↦ ∑ i, ∑ j, gᵢⱼ(x) ⟪eᵢ, ·⟫ eⱼ, whose value on eᵢ is the vector ∑ j, gᵢⱼ eⱼ obtained by recombining the components of the ith directional derivative (TauCeti.W1p.hasWeakLineDerivOn_gradient_of_forall_inner). Weak differentiability in every direction then follows from the basis directions by Module.Basis.hasWeakFDerivOn_of_forall.

No boundedness or boundary regularity of Ω is used.

Main declarations

• TauCeti.W1p.hasWeakLineDerivOn_gradient_of_forall_inner: a weak directional derivative of the weak gradient, reassembled from its orthonormal components.
• TauCeti.W1p.exists_lowerOrder_eq_of_forall_hasWeakLineDerivOn: componentwise second weak derivatives in Lᵖ(Ω) place a W^{1,p}(Ω) function in W^{2,p}(Ω).

theorem TauCeti.W1p.hasWeakLineDerivOn_gradient_of_forall_inner {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)] {ι : Type u_2} [Fintype ι] (u : ↥(W1p mu Omega p)) (b : OrthonormalBasis ι ℝ E) (v : E) (g : ι → ↥(MeasureTheory.Lp ℝ p (mu.restrict ↑Omega))) (hg : ∀ (j : ι), HasWeakLineDerivOn mu Omega (fun (x : E) => inner ℝ (↑↑(gradient u) x) (b j)) (↑↑(g j)) v) : HasWeakLineDerivOn mu Omega (↑↑(gradient u)) (fun (x : E) => ∑ j : ι, ↑↑(g j) x • b j) v

Recombining the components of a directional derivative of the gradient. If, in the direction v, each scalar component ⟪∇u, eⱼ⟫ of the weak gradient of u ∈ W^{1,p}(Ω) has the weak derivative gⱼ ∈ Lᵖ(Ω), then ∇u itself has the weak derivative ∑ j, gⱼ eⱼ.

theorem TauCeti.W1p.exists_lowerOrder_eq_of_forall_hasWeakLineDerivOn {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)] {ι : Type u_2} [Fintype ι] (u : ↥(W1p mu Omega p)) (b : OrthonormalBasis ι ℝ E) (h : ∀ (i j : ι), ∃ (g : ↥(MeasureTheory.Lp ℝ p (mu.restrict ↑Omega))), HasWeakLineDerivOn mu Omega (fun (x : E) => inner ℝ (↑↑(gradient u) x) (b j)) (↑↑g) (b i)) : ∃ (U : Wkp mu Omega p 2), Wkp.lowerOrder 1 U = u

Second-order weak differentiability from directional derivatives. Fix an orthonormal basis e of E. If, for every pair of indices i, j, the scalar component ⟪∇u, eⱼ⟫ of the weak gradient of u ∈ W^{1,p}(Ω) has a weak derivative in Lᵖ(Ω) in the direction eᵢ, then u is the first-order part of an element of W^{2,p}(Ω).

This is how a difference-quotient argument, which produces exactly these componentwise derivatives, certifies membership in the second-order Sobolev space.