Bounded difference quotients give weak derivatives

For a locally integrable u : E → ℝ on an open set Ω, a direction v and a real t ≠ 0, the difference quotient of u is

t⁻¹ * (u (x + t • v) - u x).

This file proves the L² form of the difference-quotient criterion for weak differentiability: if the difference quotients of u in the direction v are bounded by C in L²(K) for arbitrarily small t, on every compact K ⊆ Ω, then u has a weak derivative in the direction v which lies in L²(Ω) with norm at most C. This is the step of the difference-quotient method that turns the uniform L² bounds on difference quotients of a weak solution into membership of its derivatives in L², as in the proof of interior H² regularity for elliptic equations.

The criterion combines two results of independent use.

• The difference quotients of u converge to its distributional derivative: paired with a test function φ, they tend to -∫ ∂_v φ * u as t → 0.
• A distributional derivative that is bounded against the L² norm of test functions is an L² function: this is TauCeti.exists_norm_le_hasWeakLineDerivOn_of_abs_integral_lineDeriv_mul_le, proved in TauCeti.Analysis.Sobolev.TestFunctionLp.

The criterion is stated for the exponent 2, where every bounded functional on L²(Ω) is represented by an element of L²(Ω).

Main declarations

• TauCeti.integral_inv_mul_sub_mul_tendsto_neg_integral_lineDeriv_mul: the difference quotients of a locally integrable function converge to its distributional derivative when paired with a test function.
• TauCeti.exists_norm_le_hasWeakLineDerivOn_of_frequently_eLpNorm_inv_mul_sub_le: the difference-quotient criterion.
• TauCeti.exists_integrable_eqOn_tsupport_add: a locally integrable function agrees with a globally integrable one on the support of a test function and on its small translates.

References

• L. C. Evans, Partial Differential Equations, §5.8.2, Theorem 3.
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Lemma 7.24.

theorem TauCeti.exists_integrable_eqOn_tsupport_add {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [BorelSpace E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] {u : E → F} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (φ : TestFunction Ω ℝ ⊤) (v : E) : ∃ (w : E → F), MeasureTheory.Integrable w μ ∧ Set.EqOn w u (tsupport ⇑φ) ∧ ∀ᶠ (t : ℝ) in nhdsWithin 0 {0}ᶜ, ∀ x ∈ tsupport ⇑φ, w (x + t • v) = u (x + t • v)

Localization of a locally integrable function at a test function. A function locally integrable on Ω agrees, on the support of a test function φ and on all small translates of that support in a direction v, with a function that is integrable on all of E: its truncation to a compact neighbourhood of tsupport φ inside Ω.

This replaces local integrability by genuine integrability in any argument that only sees u through φ and its small translates, so that the global integral theorems apply.

theorem TauCeti.integral_inv_mul_sub_mul_tendsto_neg_integral_lineDeriv_mul {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (φ : TestFunction Ω ℝ ⊤) (v : E) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : E), t⁻¹ * (u (x + t • v) - u x) * φ x ∂μ) (nhdsWithin 0 {0}ᶜ) (nhds (-∫ (x : E), lineDeriv ℝ (⇑φ) x v * u x ∂μ))

Difference quotients converge to the distributional derivative. If u is locally integrable on Ω and φ is a test function on Ω, then as t → 0 with t ≠ 0,

∫ t⁻¹ * (u (x + t • v) - u x) * φ x → -∫ ∂_v φ * u.

No differentiability of u is assumed: when u has a weak derivative u' in the direction v, the limit is ∫ φ * u'.

theorem TauCeti.exists_norm_le_hasWeakLineDerivOn_of_frequently_eLpNorm_inv_mul_sub_le {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (v : E) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ K ⊆ ↑Ω, IsCompact K → ∃ᶠ (t : ℝ) in nhdsWithin 0 {0}ᶜ, MeasureTheory.eLpNorm (fun (x : E) => t⁻¹ * (u (x + t • v) - u x)) 2 (μ.restrict K) ≤ ENNReal.ofReal C) : ∃ (g : ↥(MeasureTheory.Lp ℝ 2 (μ.restrict ↑Ω))), ‖g‖ ≤ C ∧ HasWeakLineDerivOn μ Ω u (↑↑g) v

The difference-quotient criterion for weak differentiability. Let u be locally integrable on Ω and C ≥ 0. Suppose that on every compact K ⊆ Ω the difference quotients of u in the direction v satisfy

‖t⁻¹ * (u (· + t • v) - u)‖_{L²(K)} ≤ C

for arbitrarily small t ≠ 0. Then u has a weak derivative in the direction v on Ω that lies in L²(Ω) and has norm at most C.

The hypothesis only asks for the bound frequently as t → 0; the usual hypothesis that it holds for all sufficiently small t ≠ 0 implies it by Filter.Eventually.frequently.