Smoothness of a family closed under differentiation

Put the two halves together. The Sobolev ladder raises every member of a family closed under weak differentiation from L² to L^{2d} on an inner ball, Morrey turns that into a Hölder representative, and the representatives inherit the weak gradients of the members they represent. A continuous function with a continuous weak gradient is classically differentiable, so each representative is differentiable with its derivative again in the family, and an induction on the order reads that as C^∞.

Only one ball is lost, at the Morrey step. The ladder shrinks internally between the two radii it is given, and the differentiability argument runs on the inner ball itself, since the derivative of a representative is a representative. Were the derivative to force a further shrinking, no fixed ball would serve every order.

Main declarations

• EllipticPdes.Embedding.contDiffOn_of_gradClosed: smooth representatives for a family closed under weak differentiation.

theorem EllipticPdes.Embedding.contDiffOn_of_gradClosed {d : ℕ} (hd : 0 < d) (c : EuclideanSpace ℝ (Fin d)) {r R : ℝ} (hr : 0 < r) (hrR : r < R) {ι : Type u_1} {F : ι → EuclideanSpace ℝ (Fin d) → ℝ} {nxt : ι → Fin d → ι} (hgrad : ∀ (i : ι), HasWeakGradOn (Metric.ball c R) (F i) fun (k : Fin d) => F (nxt i k)) (hmem : ∀ (i : ι), MeasureTheory.MemLp (F i) 2 (MeasureTheory.volume.restrict (Metric.ball c R))) : ∃ (v : ι → EuclideanSpace ℝ (Fin d) → ℝ), (∀ (i : ι), ContDiffOn ℝ (↑⊤) (v i) (Metric.ball c r)) ∧ ∀ (i : ι), v i =ᵐ[MeasureTheory.volume.restrict (Metric.ball c r)] F i

Smooth representatives of a family closed under weak differentiation. Let F assign a function to each index, let nxt i k name a weak k-derivative of F i on Metric.ball c R, and let every member lie in L² there. Then on any smaller concentric ball every member has a representative smooth to every order.

The representatives are produced together, one per index, because the derivative of the representative of F i has to be the representative of F (nxt i k) rather than some other function agreeing with it almost everywhere. Continuity is what makes the choice rigid: two continuous representatives of one class on an open ball are equal.