One-dimensional weak derivatives

These results identify locally integrable functions from their distributional time derivatives on an open interval.

def CKN.IsIntervalTest (U : Set ℝ) (φ : ℝ → ℝ) : Prop

A compact smooth test supported in an open interval.

Equations

• CKN.IsIntervalTest U φ = (ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ ∧ tsupport φ ⊆ U)

def CKN.HasWeakDerivOn (U : Set ℝ) (f g : ℝ → ℝ) : Prop

The distributional derivative of f on U is represented by g.

Equations

• CKN.HasWeakDerivOn U f g = ∀ (φ : ℝ → ℝ), CKN.IsIntervalTest U φ → ∫ (x : ℝ) in U, f x * deriv φ x = -∫ (x : ℝ) in U, g x * φ x

theorem CKN.exists_ae_eq_const_of_weakDeriv_zero {a b : ℝ} (hab : a < b) {F : ℝ → ℝ} (hF : MeasureTheory.LocallyIntegrableOn F (Set.Ioo a b) MeasureTheory.volume) (hweak : HasWeakDerivOn (Set.Ioo a b) F fun (x : ℝ) => 0) : ∃ (C : ℝ), ∀ᵐ (x : ℝ), x ∈ Set.Ioo a b → F x = C

A locally integrable function with zero distributional derivative is constant almost everywhere.

theorem CKN.exists_ae_eq_const_add_intervalIntegral_of_weakDeriv {a b t₀ : ℝ} (hab : a < b) (ht₀ : t₀ ∈ Set.Ioo a b) {f g : ℝ → ℝ} (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioo a b) MeasureTheory.volume) (hg : MeasureTheory.LocallyIntegrableOn g (Set.Ioo a b) MeasureTheory.volume) (hweak : HasWeakDerivOn (Set.Ioo a b) f g) : ∃ (C : ℝ), ∀ᵐ (x : ℝ), x ∈ Set.Ioo a b → f x = C + ∫ (s : ℝ) in t₀..x, g s

A locally integrable weak derivative determines the function up to a constant.

theorem CKN.eq_const_add_intervalIntegral_of_continuous_weakDeriv {a b t₀ : ℝ} (hab : a < b) (ht₀ : t₀ ∈ Set.Ioo a b) {f g : ℝ → ℝ} (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioo a b) MeasureTheory.volume) (hg : MeasureTheory.LocallyIntegrableOn g (Set.Ioo a b) MeasureTheory.volume) (hweak : HasWeakDerivOn (Set.Ioo a b) f g) (hfcont : ContinuousOn f (Set.Ioo a b)) : ∃ (C : ℝ), ∀ x ∈ Set.Ioo a b, f x = C + ∫ (s : ℝ) in t₀..x, g s

Continuity upgrades the weak-derivative representation to every point.

theorem CKN.abs_sq_le_time_integral_sq_of_continuous_weakDeriv {τ : ℝ} (hτ : 0 < τ) {f g : ℝ → ℝ} (hfcont : ContinuousOn f (Set.Ico 0 τ)) (hfzero : f 0 = 0) (hgL2 : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ioo 0 τ))) (hweak : HasWeakDerivOn (Set.Ioo 0 τ) f g) (t : ℝ) : 0 < t → t < τ → |f t| ^ 2 ≤ t * ∫ (s : ℝ) in 0..t, |g s| ^ 2

The zero initial trace gives the one-dimensional small-time energy bound.