Measurability of the line derivative #

We prove in measurable_lineDeriv that the line derivative of a function (with respect to a locally compact scalar field) is measurable, provided the function is continuous.

In measurable_lineDeriv_uncurry, assuming additionally that the source space is second countable, we show that (x, v) ↦ lineDeriv 𝕜 f x v is also measurable.

An assumption such as continuity is necessary, as otherwise one could alternate in a non-measurable way between differentiable and non-differentiable functions along the various lines directed by v.

Measurability of the line derivative lineDeriv 𝕜 f x v with respect to a fixed direction v.

theorem measurableSet_lineDifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} {v : E} (hf : ) :
MeasurableSet {x : E | }
theorem measurable_lineDeriv {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} {v : E} [] [] (hf : ) :
Measurable fun (x : E) => lineDeriv 𝕜 f x v
theorem stronglyMeasurable_lineDeriv {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} {v : E} (hf : ) :
theorem aemeasurable_lineDeriv {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} {v : E} [] [] (hf : ) (μ : ) :
AEMeasurable (fun (x : E) => lineDeriv 𝕜 f x v) μ
theorem aestronglyMeasurable_lineDeriv {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} {v : E} (hf : ) (μ : ) :
MeasureTheory.AEStronglyMeasurable (fun (x : E) => lineDeriv 𝕜 f x v) μ

Measurability of the line derivative lineDeriv 𝕜 f x v when varying both x and v. For this, we need an additional second countability assumption on E to make sure that open sets are measurable in E × E.

theorem measurableSet_lineDifferentiableAt_uncurry {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} (hf : ) :
MeasurableSet {p : E × E | LineDifferentiableAt 𝕜 f p.1 p.2}
theorem measurable_lineDeriv_uncurry {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} [] [] (hf : ) :
Measurable fun (p : E × E) => lineDeriv 𝕜 f p.1 p.2
theorem stronglyMeasurable_lineDeriv_uncurry {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} (hf : ) :
MeasureTheory.StronglyMeasurable fun (p : E × E) => lineDeriv 𝕜 f p.1 p.2
theorem aemeasurable_lineDeriv_uncurry {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} [] [] (hf : ) (μ : MeasureTheory.Measure (E × E)) :
AEMeasurable (fun (p : E × E) => lineDeriv 𝕜 f p.1 p.2) μ
theorem aestronglyMeasurable_lineDeriv_uncurry {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} (hf : ) (μ : MeasureTheory.Measure (E × E)) :
MeasureTheory.AEStronglyMeasurable (fun (p : E × E) => lineDeriv 𝕜 f p.1 p.2) μ