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}
[NontriviallyNormedField 𝕜]
[LocallyCompactSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
{v : E}
(hf : Continuous f)
:
MeasurableSet {x : E | LineDifferentiableAt 𝕜 f x v}
theorem
measurable_lineDeriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[LocallyCompactSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
{v : E}
[MeasurableSpace F]
[BorelSpace F]
(hf : Continuous f)
:
Measurable fun (x : E) => lineDeriv 𝕜 f x v
theorem
stronglyMeasurable_lineDeriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[LocallyCompactSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
{v : E}
[SecondCountableTopologyEither E F]
(hf : Continuous f)
:
MeasureTheory.StronglyMeasurable fun (x : E) => lineDeriv 𝕜 f x v
theorem
aemeasurable_lineDeriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[LocallyCompactSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
{v : E}
[MeasurableSpace F]
[BorelSpace F]
(hf : Continuous f)
(μ : MeasureTheory.Measure E)
:
AEMeasurable (fun (x : E) => lineDeriv 𝕜 f x v) μ
theorem
aestronglyMeasurable_lineDeriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[LocallyCompactSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
{v : E}
[SecondCountableTopologyEither E F]
(hf : Continuous f)
(μ : MeasureTheory.Measure E)
:
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}
[NontriviallyNormedField 𝕜]
[LocallyCompactSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
[SecondCountableTopology E]
(hf : Continuous f)
:
MeasurableSet {p : E × E | LineDifferentiableAt 𝕜 f p.1 p.2}
theorem
measurable_lineDeriv_uncurry
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[LocallyCompactSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
[SecondCountableTopology E]
[MeasurableSpace F]
[BorelSpace F]
(hf : Continuous f)
:
Measurable fun (p : E × E) => lineDeriv 𝕜 f p.1 p.2
theorem
stronglyMeasurable_lineDeriv_uncurry
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[LocallyCompactSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
[SecondCountableTopology E]
(hf : Continuous f)
:
MeasureTheory.StronglyMeasurable fun (p : E × E) => lineDeriv 𝕜 f p.1 p.2
theorem
aemeasurable_lineDeriv_uncurry
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[LocallyCompactSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
[SecondCountableTopology E]
[MeasurableSpace F]
[BorelSpace F]
(hf : Continuous f)
(μ : MeasureTheory.Measure (E × E))
:
AEMeasurable (fun (p : E × E) => lineDeriv 𝕜 f p.1 p.2) μ
theorem
aestronglyMeasurable_lineDeriv_uncurry
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[LocallyCompactSpace 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
[SecondCountableTopology E]
(hf : Continuous f)
(μ : MeasureTheory.Measure (E × E))
:
MeasureTheory.AEStronglyMeasurable (fun (p : E × E) => lineDeriv 𝕜 f p.1 p.2) μ