Continuous weak derivatives are classical derivatives

A continuous function on an open domain with a continuous weak Fréchet derivative is C¹, and its classical derivative is the given weak derivative at every point of the domain. More generally, a Cᵏ weak derivative makes the function Cᵏ⁺¹. These results turn continuous representatives of Sobolev derivative fields into classical regularity, without imposing any boundary regularity or global integrability assumption.

The proof combines HasWeakFDerivOn.hasFDerivAt_indicator_convolution_normed with Mathlib's ContDiffBump.convolution_tendsto_right and hasFDerivAt_of_tendstoUniformlyOnFilter. The value converges pointwise, while the derivative converges uniformly near each point. Restriction to a relatively compact ball makes the zero extensions integrable; it does not assert a weak derivative identity across the boundary of that ball.

References

L. C. Evans, Partial Differential Equations, Chapter 5, Sections 5.3 and 5.6.

theorem TauCeti.HasWeakFDerivOn.hasFDerivAt_of_continuousOn {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {u : E → F} {U : E → E →L[ℝ] F} (h : HasWeakFDerivOn mu Omega u U) (hu : ContinuousOn u ↑Omega) (hU : ContinuousOn U ↑Omega) {x : E} (hx : x ∈ Omega) : HasFDerivAt u (U x) x

A continuous weak Fréchet derivative of a continuous function is its classical derivative at every point of the open domain. No global integrability or boundary regularity is needed.

theorem TauCeti.HasWeakFDerivOn.fderiv_eq_of_continuousOn {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {u : E → F} {U : E → E →L[ℝ] F} (h : HasWeakFDerivOn mu Omega u U) (hu : ContinuousOn u ↑Omega) (hU : ContinuousOn U ↑Omega) {x : E} (hx : x ∈ Omega) : fderiv ℝ u x = U x

The classical derivative agrees pointwise with a continuous weak derivative of a continuous function on an open domain.

theorem TauCeti.HasWeakFDerivOn.contDiffOn_succ {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {u : E → F} {U : E → E →L[ℝ] F} (h : HasWeakFDerivOn mu Omega u U) (hu : ContinuousOn u ↑Omega) {n : ℕ∞} (hU : ContDiffOn ℝ (↑n) U ↑Omega) : ContDiffOn ℝ (↑n + 1) u ↑Omega

If a continuous function has a Cᵏ weak derivative on an open domain, then it is Cᵏ⁺¹ there. The index includes smoothness, but not analyticity.