Weak derivatives on an interval

Let F be a Banach space and u, u' : ℝ → F locally integrable on the open interval (a, b). This file proves that u' is the weak derivative of u on (a, b) exactly when u is, almost everywhere, a constant plus the primitive of u':

u t = c + ∫ s in t₀..t, u' s for almost every t ∈ (a, b),

for any base point t₀ ∈ (a, b). When u' is integrable on the whole interval, u therefore has a representative v continuous on [a, b], every such representative satisfies the fundamental theorem of calculus v t - v s = ∫ r in s..t, u' r on [a, b], and, when a < b, it is bounded by

‖v t‖ ≤ ⨍ s in (a, b), ‖u s‖ + ∫ s in (a, b), ‖u' s‖.

This is the theory of the vector-valued Sobolev space W^{1,1}(a, b; F). It is the analytic input for evolution equations, whose solutions are functions of time t ∈ (0, T) with values in a function space F, and whose time derivatives are weak derivatives in this sense. The weak derivative is TauCeti.HasWeakLineDerivOn for Lebesgue measure on ℝ, the open set (a, b) and the direction 1, so the test functions are the real smooth functions with compact support in (a, b).

Proof

The primitive w t = ∫ s in t₀..t, u' s has weak derivative u': against a test function φ supported in [α, β] ⊆ (a, b), the integration by parts TauCeti.intervalIntegral.integral_deriv_smul_primitive_eq_sub_of_le, proved with Fubini's theorem, turns ∫ φ' t • ∫ s in α..t, u' s into -∫ φ s • u' s. Then u - w has weak derivative 0, so it is almost everywhere constant by the du Bois-Reymond lemma MeasureTheory.LocallyIntegrableOn.exists_ae_eq_const_Ioo_of_integral_deriv_smul_eq_zero.

Main declarations

• TauCeti.hasWeakLineDerivOn_intervalIntegral: the primitive of a locally integrable function is weakly differentiable, with weak derivative the function.
• TauCeti.hasWeakLineDerivOn_intervalIntegral_left: the same for the primitive from the left endpoint of the interval, when the function is integrable on the whole interval.
• TauCeti.HasWeakLineDerivOn.exists_ae_eq_const: a function with weak derivative 0 on an interval is almost everywhere constant there.
• TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral and TauCeti.hasWeakLineDerivOn_Ioo_iff_exists_ae_eq_add_intervalIntegral: a function is weakly differentiable on an interval exactly when it is almost everywhere a constant plus the primitive of its weak derivative.
• TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral_left: the same with the primitive taken from the left endpoint, when the weak derivative is integrable.
• TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral_top: the same on the whole line.
• TauCeti.HasWeakLineDerivOn.exists_continuousOn_ae_eq: if the weak derivative is integrable, the function has a representative continuous on the closed interval.
• TauCeti.HasWeakLineDerivOn.integral_eq_sub: the fundamental theorem of calculus for such a continuous representative.
• TauCeti.HasWeakLineDerivOn.absolutelyContinuousOnInterval and TauCeti.HasWeakLineDerivOn.ae_hasDerivAt: absolute continuity and identification of the classical derivative of a continuous representative.
• TauCeti.HasWeakLineDerivOn.integral_eq_zero_iff_exists_absolutelyContinuousOnInterval: zero integral of the weak derivative characterizes matching endpoint traces.
• TauCeti.HasWeakLineDerivOn.integral_deriv_smul_eq_sub: integration by parts against a C¹ function for such a continuous representative.
• TauCeti.HasWeakLineDerivOn.norm_le_setAverage_add_integral: for a < b, the pointwise bound ‖v t‖ ≤ ⨍ s in (a, b), ‖u s‖ + ∫ s in (a, b), ‖u' s‖ of a continuous representative v.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §5.9.2, Theorem 2.
• H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, §8.2, Theorem 8.2 and Lemmas 8.1 and 8.2 (the scalar case).

The primitive is weakly differentiable

theorem TauCeti.hasWeakLineDerivOn_intervalIntegral {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b t₀ : ℝ} {u' : ℝ → F} [CompleteSpace F] (hu' : MeasureTheory.LocallyIntegrableOn u' (Set.Ioo a b) MeasureTheory.volume) (ht₀ : t₀ ∈ Set.Ioo a b) : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } (fun (t : ℝ) => ∫ (s : ℝ) in t₀..t, u' s) u' 1

The primitive is weakly differentiable. If u' is locally integrable on Ioo a b and t₀ ∈ Ioo a b, then u' is the weak derivative of its primitive t ↦ ∫ s in t₀..t, u' s on Ioo a b.

theorem TauCeti.hasWeakLineDerivOn_intervalIntegral_left {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u' : ℝ → F} [CompleteSpace F] (hu' : MeasureTheory.IntegrableOn u' (Set.Ioo a b) MeasureTheory.volume) : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } (fun (t : ℝ) => ∫ (s : ℝ) in a..t, u' s) u' 1

The primitive from an endpoint is weakly differentiable. If u' is integrable on Ioo a b, then u' is the weak derivative of its primitive t ↦ ∫ s in a..t, u' s on Ioo a b.

The fundamental theorem of calculus

theorem TauCeti.HasWeakLineDerivOn.exists_ae_eq_const {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u : ℝ → F} (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u 0 1) : ∃ (c : F), u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] fun (x : ℝ) => c

The du Bois-Reymond lemma for weak derivatives. A function whose weak derivative on Ioo a b is 0 is almost everywhere equal to a constant on Ioo a b.

theorem TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b t₀ : ℝ} {u u' : ℝ → F} (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u' 1) (ht₀ : t₀ ∈ Set.Ioo a b) : ∃ (c : F), u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] fun (t : ℝ) => c + ∫ (s : ℝ) in t₀..t, u' s

The fundamental theorem of calculus for weak derivatives. If u' is the weak derivative of u on Ioo a b and t₀ ∈ Ioo a b, then u is almost everywhere on Ioo a b equal to a constant plus the primitive t ↦ ∫ s in t₀..t, u' s.

theorem TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral_left {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u u' : ℝ → F} (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u' 1) (hu' : MeasureTheory.IntegrableOn u' (Set.Ioo a b) MeasureTheory.volume) : ∃ (c : F), u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] fun (t : ℝ) => c + ∫ (s : ℝ) in a..t, u' s

The fundamental theorem of calculus for weak derivatives, from the left endpoint. If u' is the weak derivative of u on Ioo a b and u' is integrable on Ioo a b, then u is almost everywhere on Ioo a b equal to a constant plus the primitive t ↦ ∫ s in a..t, u' s.

theorem TauCeti.hasWeakLineDerivOn_Ioo_iff_exists_ae_eq_add_intervalIntegral {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b t₀ : ℝ} {u u' : ℝ → F} [CompleteSpace F] (hu' : MeasureTheory.LocallyIntegrableOn u' (Set.Ioo a b) MeasureTheory.volume) (ht₀ : t₀ ∈ Set.Ioo a b) : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u' 1 ↔ ∃ (c : F), u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] fun (t : ℝ) => c + ∫ (s : ℝ) in t₀..t, u' s

Weak derivatives on an interval. For u' locally integrable on Ioo a b and t₀ ∈ Ioo a b, u' is the weak derivative of u on Ioo a b exactly when u is almost everywhere on Ioo a b a constant plus the primitive t ↦ ∫ s in t₀..t, u' s.

theorem TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral_top {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {u u' : ℝ → F} (h : HasWeakLineDerivOn MeasureTheory.volume ⊤ u u' 1) (t₀ : ℝ) : ∃ (c : F), u =ᵐ[MeasureTheory.volume] fun (t : ℝ) => c + ∫ (s : ℝ) in t₀..t, u' s

The fundamental theorem of calculus for weak derivatives on the line. If u' is the weak derivative of u on all of ℝ, then u is almost everywhere equal to a constant plus the primitive t ↦ ∫ s in t₀..t, u' s, for any base point t₀.

theorem TauCeti.HasWeakLineDerivOn.exists_continuousOn_ae_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u u' : ℝ → F} (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u' 1) (hu' : MeasureTheory.IntegrableOn u' (Set.Ioo a b) MeasureTheory.volume) : ∃ (v : ℝ → F), ContinuousOn v (Set.Icc a b) ∧ u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] v

A continuous representative. If u' is the weak derivative of u on Ioo a b and u' is integrable on Ioo a b, then u agrees almost everywhere on Ioo a b with a function continuous on Icc a b.

theorem TauCeti.HasWeakLineDerivOn.integral_eq_sub {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u u' v : ℝ → F} (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u' 1) (hu' : MeasureTheory.IntegrableOn u' (Set.Ioo a b) MeasureTheory.volume) (hv : ContinuousOn v (Set.Icc a b)) (hae : u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] v) {s t : ℝ} (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) : ∫ (r : ℝ) in s..t, u' r = v t - v s

The fundamental theorem of calculus for a continuous representative. Let u' be the weak derivative of u on Ioo a b, integrable on Ioo a b, and let v be continuous on Icc a b and equal to u almost everywhere on Ioo a b. Then ∫ r in s..t, u' r = v t - v s for all s, t ∈ Icc a b.

theorem TauCeti.HasWeakLineDerivOn.absolutelyContinuousOnInterval {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u u' v : ℝ → F} (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u' 1) (hu' : MeasureTheory.IntegrableOn u' (Set.Ioo a b) MeasureTheory.volume) (hv : ContinuousOn v (Set.Icc a b)) (hae : u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] v) (hab : a ≤ b) : AbsolutelyContinuousOnInterval v a b

A continuous representative of a function with integrable weak derivative on an interval is absolutely continuous on the closed interval.

theorem TauCeti.HasWeakLineDerivOn.ae_hasDerivAt {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u u' v : ℝ → F} (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u' 1) (hv : ContinuousOn v (Set.Ioo a b)) (hae : u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] v) (hab : a ≤ b) : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt v (u' t) t

The classical derivative of a Sobolev representative continuous on the open interval agrees almost everywhere in the interval with its weak derivative.

theorem TauCeti.HasWeakLineDerivOn.integral_eq_zero_iff_exists_absolutelyContinuousOnInterval {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u u' : ℝ → F} (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u' 1) (hu' : MeasureTheory.IntegrableOn u' (Set.Ioo a b) MeasureTheory.volume) (hab : a ≤ b) : ∫ (t : ℝ) in a..b, u' t = 0 ↔ ∃ (v : ℝ → F), AbsolutelyContinuousOnInterval v a b ∧ u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] v ∧ v a = v b

The integral of an integrable weak derivative is zero exactly when the Sobolev function has an absolutely continuous representative whose endpoint values agree.

theorem TauCeti.HasWeakLineDerivOn.integral_deriv_smul_eq_sub {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u u' v : ℝ → F} (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u' 1) (hu' : MeasureTheory.IntegrableOn u' (Set.Ioo a b) MeasureTheory.volume) (hv : ContinuousOn v (Set.Icc a b)) (hae : u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] v) (hab : a ≤ b) {φ : ℝ → ℝ} (hφ : ContDiff ℝ 1 φ) : ∫ (t : ℝ) in a..b, deriv φ t • v t = φ b • v b - φ a • v a - ∫ (t : ℝ) in a..b, φ t • u' t

Integration by parts for a continuous representative. Let u' be the weak derivative of u on Ioo a b, a ≤ b, integrable on Ioo a b, and let v be continuous on Icc a b and equal to u almost everywhere on Ioo a b. Then for every C¹ function φ : ℝ → ℝ, ∫ t in a..b, φ' t • v t = φ b • v b - φ a • v a - ∫ t in a..b, φ t • u' t.

theorem TauCeti.HasWeakLineDerivOn.norm_le_setAverage_add_integral {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u u' v : ℝ → F} (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u' 1) (hab : a < b) (hu' : MeasureTheory.IntegrableOn u' (Set.Ioo a b) MeasureTheory.volume) (hv : ContinuousOn v (Set.Icc a b)) (hae : u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] v) {t : ℝ} (ht : t ∈ Set.Icc a b) : ‖v t‖ ≤ (⨍ (s : ℝ) in Set.Ioo a b, ‖u s‖) + ∫ (s : ℝ) in Set.Ioo a b, ‖u' s‖

The W^{1,1} bound. Let the weak derivative u' of u on Ioo a b, a < b, be integrable on Ioo a b, and let v be continuous on Icc a b and equal to u almost everywhere on Ioo a b. Then at every t ∈ Icc a b, ‖v t‖ ≤ ⨍ s in Ioo a b, ‖u s‖ + ∫ s in Ioo a b, ‖u' s‖.