Bridge from HasWeakDerivOn to HasWeakGradOn

The L² weak derivatives produced by interior_H2_estimate are pointwise weak gradients in the sense of the embedding layer, so the Morrey inequality consumes them directly at p = 2, hence in dimension one.

Higher dimensions need an Lᵖ bootstrap first, since Morrey asks for p > d. Dimensions two and three are covered in EllipticPdes.Embedding.GagliardoNirenberg, where the Gagliardo-Nirenberg-Sobolev inequality raises the gradient from L² to L⁶ at d = 3 and, over the finite measure of a ball, from L^{4/3} to L⁴ at d = 2. The three resulting Hölder estimates are EllipticPdes.Embedding.interior_holder_estimate_one, EllipticPdes.Embedding.interior_holder_estimate_two and EllipticPdes.Embedding.interior_holder_estimate.

Dimension four and above needs the step iterated, which uses a weak derivative per rung and so asks for more than the H² estimate supplies. EllipticPdes.Embedding.memLp_of_gradClosed runs that ladder on a family closed under differentiation.

theorem EllipticPdes.Embedding.hasWeakGradOn_of_hasWeakDerivOn {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} {u : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict B))} {g : Fin d → ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict B))} (h : ∀ (k : Fin d), Regularity.HasWeakDerivOn B k u (g k)) : HasWeakGradOn B (fun (x : EuclideanSpace ℝ (Fin d)) => ↑↑u x) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => ↑↑(g k) x

An L² weak gradient (componentwise HasWeakDerivOn) is a pointwise weak gradient. This connects interior_H2_estimate's output into morrey_ball.