Measurability of almost-everywhere line derivatives

Let μ be a translation-invariant measure on a module E over a nontrivially normed field 𝕜, with continuous translations and scalar multiplication, measurable translations, and measurable open sets. Let u : E → F be a.e.-strongly measurable on an open set s, and suppose that at almost every x ∈ s it has a line derivative u' x in a fixed direction v. Then u' is a.e.-strongly measurable on s (MeasureTheory.AEStronglyMeasurable.of_ae_hasLineDerivAt), being the almost-everywhere limit of the difference quotients t⁻¹ • (u (x + t • v) - u x). If u is moreover locally Lipschitz on s and E is seminormed, then u' is essentially locally bounded there (near each point it is bounded almost everywhere by C * ‖v‖ for a local Lipschitz constant C), hence locally integrable provided μ is locally finite and SecondCountableTopologyEither E F holds (LocallyLipschitzOn.locallyIntegrableOn_of_ae_hasLineDerivAt).

Mathlib's aestronglyMeasurable_lineDeriv covers lineDeriv of a globally continuous function. The results here only ask for measurability on s and for a line derivative almost everywhere, with an arbitrary candidate u'; this is the form in which a.e. derivatives of locally Lipschitz functions (Rademacher's theorem) enter the theory of weak derivatives.

Finally, multiplying an integrable function by the directional derivative of a Lipschitz function keeps it integrable (LipschitzWith.integrable_lineDeriv_smul).

theorem MeasureTheory.AEStronglyMeasurable.of_ae_hasLineDerivAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [MeasurableSpace E] {μ : Measure E} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {v : E} {u u' : E → F} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousConstVAdd E E] [ContinuousSMul 𝕜 E] [OpensMeasurableSpace E] [MeasurableAdd E] [μ.IsAddRightInvariant] (hu : AEStronglyMeasurable u (μ.restrict s)) (hs : IsOpen s) (h : ∀ᵐ (x : E) ∂μ, x ∈ s → HasLineDerivAt 𝕜 u (u' x) x v) : AEStronglyMeasurable u' (μ.restrict s)

For a translation-invariant measure μ, an almost-everywhere line derivative of a function a.e.-strongly measurable on an open set s is a.e.-strongly measurable on s: it is the almost-everywhere limit of difference quotients.

theorem LocallyLipschitzOn.locallyIntegrableOn_of_ae_hasLineDerivAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {v : E} {u u' : E → F} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [OpensMeasurableSpace E] [MeasurableAdd E] [SecondCountableTopologyEither E F] [μ.IsAddRightInvariant] [MeasureTheory.IsLocallyFiniteMeasure μ] (hu : LocallyLipschitzOn s u) (hs : IsOpen s) (h : ∀ᵐ (x : E) ∂μ, x ∈ s → HasLineDerivAt 𝕜 u (u' x) x v) : MeasureTheory.LocallyIntegrableOn u' s μ

For a locally finite, translation-invariant measure μ, assuming SecondCountableTopologyEither E F, an almost-everywhere line derivative of a function locally Lipschitz on an open set s is locally integrable on s: it is measurable, and near each point it is bounded almost everywhere by C * ‖v‖ for a local Lipschitz constant C.

theorem LipschitzWith.integrable_lineDeriv_smul {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ν : MeasureTheory.Measure E} {g : E → F} {ψ : E → ℝ} {v : E} {K : NNReal} (hψ : LipschitzWith K ψ) (hg : MeasureTheory.Integrable g ν) : MeasureTheory.Integrable (fun (x : E) => lineDeriv ℝ ψ x v • g x) ν

Multiplying an integrable function by the directional derivative of a Lipschitz function keeps it integrable.