One family closed under differentiation

Higher interior regularity is proved order by order, so a solution with weak derivatives of every order arrives as one EllipticPdes.Regularity.HasIteratedWeakDerivOn per order, and nothing in the statement relates the entries two of them share. The Sobolev ladder needs the opposite: a single family, closed under differentiation, so that the derivative of a member is again a member.

Uniqueness of the weak gradient supplies the relation. On a ball inside the region the entries two families assign to one list of directions agree almost everywhere, by induction along the list, so reading each list off the family of its own length gives a family closed under differentiation up to a null set, which is all the ladder reads.

Main declarations

• EllipticPdes.Regularity.exists_gradClosed_of_hasIteratedWeakDerivOn: the closed family.
• EllipticPdes.Regularity.exists_gradClosed_of_hasIteratedWeakDerivOn_le: the same at a bounded order, where one family is the whole supply and no uniqueness is spent.

theorem EllipticPdes.Regularity.exists_gradClosed_of_hasIteratedWeakDerivOn {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (u : Sobolev.L2D V) (h : ∀ (k : ℕ), Nonempty (HasIteratedWeakDerivOn V k u)) {c : EuclideanSpace ℝ (Fin d)} {R : ℝ} (hBV : Metric.ball c R ⊆ V) : ∃ (F : List (Fin d) → EuclideanSpace ℝ (Fin d) → ℝ), (∀ (α : List (Fin d)), Embedding.HasWeakGradOn (Metric.ball c R) (F α) fun (k : Fin d) => F (k :: α)) ∧ (∀ (α : List (Fin d)), MeasureTheory.MemLp (F α) 2 (MeasureTheory.volume.restrict (Metric.ball c R))) ∧ F [] = ↑↑u

Weak derivatives of every order give one family closed under differentiation. On a ball inside the region, the functions F α read off the order-α.length family have, for each direction k, the function F (k :: α) as a weak k-derivative, and all of them lie in L². The empty list is the function itself, on the nose.

The induction along the list is where uniqueness is spent: the entries at α of two families agree almost everywhere by the inductive hypothesis, so the two weak gradients they have are weak gradients of one function, hence agree, which is the inductive step at k :: α.

theorem EllipticPdes.Regularity.exists_gradClosed_of_hasIteratedWeakDerivOn_le {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (u : Sobolev.L2D V) {m : ℕ} (H : HasIteratedWeakDerivOn V m u) {c : EuclideanSpace ℝ (Fin d)} {R : ℝ} (hBV : Metric.ball c R ⊆ V) : ∃ (F : List (Fin d) → EuclideanSpace ℝ (Fin d) → ℝ), (∀ (α : List (Fin d)), α.length < m → Embedding.HasWeakGradOn (Metric.ball c R) (F α) fun (k : Fin d) => F (k :: α)) ∧ (∀ (α : List (Fin d)), MeasureTheory.MemLp (F α) 2 (MeasureTheory.volume.restrict (Metric.ball c R))) ∧ F [] = ↑↑u

Weak derivatives up to order m give one family closed under differentiation as far as m. A single EllipticPdes.Regularity.HasIteratedWeakDerivOn at order m already assigns a class to every list of directions, so the family is that assignment and nothing has to be reconciled: D_step is the closure below order m, and membership at order 2 is inherited from the region by restriction.

The unbounded statement needs uniqueness of the weak gradient because it receives one family per order and has to identify the entries they share. Here there is one family, and the entries above order m are carried along unconstrained, which is all the bounded ladder reads of them.