Joint measurability of the applied derivative

Mathlib proves that the derivative fderiv 𝕜 f of an arbitrary function is measurable (measurable_fderiv), and that so is x ↦ fderiv 𝕜 f x y for a fixed vector y (measurable_fderiv_apply_const). This file adds the joint statement in the point and the vector, so that fun_prop can prove the measurability of expressions such as x ↦ fderiv 𝕜 f x (g x) for a measurable g. It composes measurable_fderiv with the joint measurability of evaluation, ContinuousLinearMap.measurable_apply₂, under the same second-countability assumption.

For a self-map of a finite-dimensional space the Jacobian determinant x ↦ det (fderiv 𝕜 f x) is measurable as well, being a continuous function of the derivative.

An arbitrary function is continuous on its regular set {x | fderiv 𝕜 f x ≠ 0}, which is measurable, so the regular part of the preimage of a measurable set is measurable.

Main results

• TauCeti.measurable_fderiv_apply: the map (x, y) ↦ fderiv 𝕜 f x y is measurable.
• TauCeti.measurable_det_fderiv: the Jacobian determinant x ↦ det (fderiv 𝕜 f x) is measurable.
• TauCeti.measurableSet_preimage_inter_setOf_fderiv_ne_zero: the regular part f⁻¹(I) ∩ {Df ≠ 0} of the preimage of a measurable set is measurable.

theorem TauCeti.measurable_fderiv_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace E] [OpensMeasurableSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace F] [BorelSpace F] [SecondCountableTopologyEither (E →L[𝕜] F) E] (f : E → F) : Measurable fun (p : E × E) => (fderiv 𝕜 f p.1) p.2

The derivative of an arbitrary function, applied to a vector, is jointly measurable in the point and the vector. No differentiability is assumed, the derivative being 0 where f is not differentiable.

theorem TauCeti.measurable_det_fderiv (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace E] [OpensMeasurableSpace E] [CompleteSpace 𝕜] [MeasurableSpace 𝕜] [BorelSpace 𝕜] [FiniteDimensional 𝕜 E] (f : E → E) : Measurable fun (x : E) => (fderiv 𝕜 f x).det

The Jacobian determinant of an arbitrary self-map of a finite-dimensional space is measurable. No differentiability is assumed, the derivative being 0 where f is not differentiable.

theorem TauCeti.measurableSet_preimage_inter_setOf_fderiv_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace E] [OpensMeasurableSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace F] [BorelSpace F] {f : E → F} {I : Set F} (hI : MeasurableSet I) : MeasurableSet (f ⁻¹' I ∩ {x : E | fderiv 𝕜 f x ≠ 0})

The regular part f⁻¹(I) ∩ {Df ≠ 0} of the preimage of a measurable set is measurable, for every function f: the function is continuous on its regular set, which is measurable.