Continuous weak gradient as a classical gradient

The Sobolev ladder puts a solution and its weak derivatives in a Hölder class, so both are continuous. Continuity is what turns them back into classical derivatives: a function with a continuous weak gradient on an open set is Fréchet differentiable there, with that gradient.

The argument is mollification. Each mollification is smooth, its classical partials are the mollified weak gradient (EllipticPdes.Embedding.partialD_convolution_eq_of_hasWeakGradOn), and a mollification of a continuous function converges to it uniformly on a ball whose enlargement by the mollifier radius stays inside the region, since the function is uniformly continuous on the enlargement. Mathlib's hasFDerivAt_of_tendstoUniformlyOn then passes the derivative to the limit: derivatives converging uniformly and values converging pointwise identify the limit's derivative.

Uniform convergence is where the hypotheses are spent. Pointwise convergence of the mollifications alone would not do, since it says nothing about the derivatives, and the convergence of the mollified gradient has to be uniform in the base point for the limit theorem to see it.

Main declarations

• EllipticPdes.Embedding.gradCLM: a gradient tuple read as a continuous linear functional.
• EllipticPdes.Embedding.opNorm_le_sum_apply_single: the operator norm of a functional on EuclideanSpace ℝ (Fin d), bounded by its values on the coordinate directions.
• EllipticPdes.Embedding.tendstoUniformlyOn_indicator_convolution: mollifications of a continuous function converge uniformly on an interior ball.
• EllipticPdes.Embedding.hasFDerivAt_of_continuousOn_hasWeakGradOn: the classical derivative.

Gradient tuple as a functional

noncomputable def EllipticPdes.Embedding.gradCLM {d : ℕ} (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (y : EuclideanSpace ℝ (Fin d)) : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ

The continuous linear functional whose coordinate values are the entries of g at y. This is the shape HasFDerivAt asks for, assembled from the shape a weak gradient comes in.

Equations

• EllipticPdes.Embedding.gradCLM g y = ∑ k : Fin d, g k y • EuclideanSpace.proj k

@[simp]

theorem EllipticPdes.Embedding.gradCLM_apply_single {d : ℕ} (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (y : EuclideanSpace ℝ (Fin d)) (j : Fin d) : (gradCLM g y) (EuclideanSpace.single j 1) = g j y

theorem EllipticPdes.Embedding.opNorm_le_sum_apply_single {d : ℕ} (L : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : ‖L‖ ≤ ∑ k : Fin d, ‖L (EuclideanSpace.single k 1)‖

Control of a functional by its coordinate values. On EuclideanSpace ℝ (Fin d) every vector is the sum of its coordinates against the standard directions, so the operator norm is at most the sum of the absolute values of the coordinate readings.

Uniform convergence of the mollifications

theorem EllipticPdes.Embedding.tendstoUniformlyOn_indicator_convolution {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} (hBm : MeasurableSet B) {h : EuclideanSpace ℝ (Fin d) → ℝ} (hint : MeasureTheory.IntegrableOn h B MeasureTheory.volume) (hcont : ContinuousOn h B) {x : EuclideanSpace ℝ (Fin d)} {ρ σ : ℝ} (hsub : Metric.closedBall x (ρ + σ) ⊆ B) (φ : ℕ → ContDiffBump 0) (hφσ : ∀ (n : ℕ), (φ n).rOut ≤ σ) (hφ0 : Filter.Tendsto (fun (n : ℕ) => (φ n).rOut) Filter.atTop (nhds 0)) : TendstoUniformlyOn (fun (n : ℕ) (y : EuclideanSpace ℝ (Fin d)) => MeasureTheory.convolution (B.indicator h) ((φ n).normed MeasureTheory.volume) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume y) h Filter.atTop (Metric.ball x ρ)

Mollifications of a continuous function converge uniformly on an interior ball. The enlargement Metric.closedBall x (ρ + σ) is compact and sits inside the region, so the function is uniformly continuous there. Once the mollifier radius drops below the modulus of continuity, the mollification at every point of Metric.ball x ρ averages values within ε/2 of the value at that point, and the estimate is uniform because the modulus is.

The extension by zero is what the convolution reads, and it is invisible: every point the mollifier sees at radius at most σ lies in the enlargement, hence in the region.

Classical derivative

theorem EllipticPdes.Embedding.hasFDerivAt_of_continuousOn_hasWeakGradOn {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} (hBm : MeasurableSet B) (hBo : IsOpen B) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hui : MeasureTheory.IntegrableOn u B MeasureTheory.volume) (hgi : ∀ (k : Fin d), MeasureTheory.IntegrableOn (g k) B MeasureTheory.volume) (huc : ContinuousOn u B) (hgc : ∀ (k : Fin d), ContinuousOn (g k) B) (hw : HasWeakGradOn B u g) {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ B) : HasFDerivAt u (gradCLM g x) x

Continuous weak gradient as a classical derivative. On an open region, a function that is continuous and integrable, with a weak gradient that is continuous and integrable, is Fréchet differentiable at every point, with derivative the functional the gradient names.

The proof mollifies on a ball whose double closure sits inside the region. Each mollification is smooth, its partials are the mollified gradient components, and both converge uniformly on the ball. hasFDerivAt_of_tendstoUniformlyOn collects that into the derivative of the limit, and the limit is the function itself, since a mollification of a continuous function converges to it.