# Documentation

Mathlib.Analysis.Calculus.LineDeriv.Measurable

# 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 : ) :
theorem measurable_lineDeriv {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} {v : E} [] [] (hf : ) :
Measurable fun x => 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 => lineDeriv 𝕜 f x v
theorem aestronglyMeasurable_lineDeriv {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} {v : E} (hf : ) (μ : ) :

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 | LineDifferentiableAt 𝕜 f p.fst p.snd}
theorem measurable_lineDeriv_uncurry {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} [] [] (hf : ) :
Measurable fun p => lineDeriv 𝕜 f p.fst p.snd
theorem stronglyMeasurable_lineDeriv_uncurry {𝕜 : Type u_1} {E : Type u_2} [] [] {F : Type u_3} [] [] {f : EF} (hf : ) :
MeasureTheory.StronglyMeasurable fun p => lineDeriv 𝕜 f p.fst p.snd
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 => lineDeriv 𝕜 f p.fst p.snd
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 => lineDeriv 𝕜 f p.fst p.snd) μ