Documentation

Mathlib.Analysis.Calculus.FDeriv.Measurable

Derivative is measurable #

In this file we prove that the derivative of any function with complete codomain is a measurable function. Namely, we prove:

We also show the same results for the right derivative on the real line (see measurable_derivWithin_Ici and measurable_derivWithin_Ioi), following the same proof strategy.

We also prove measurability statements for functions depending on a parameter: for f : Ξ± β†’ E β†’ F, we show the measurability of (p : Ξ± Γ— E) ↦ fderiv π•œ (f p.1) p.2. This requires additional assumptions. We give versions of the above statements (appending with_param to their names) when f is continuous and E is locally compact.

Implementation #

We give a proof that avoids second-countability issues, by expressing the differentiability set as a function of open sets in the following way. Define A (L, r, Ρ) to be the set of points where, on a ball of radius roughly r around x, the function is uniformly approximated by the linear map L, up to Ρ r. It is an open set. Let also B (L, r, s, Ρ) = A (L, r, Ρ) ∩ A (L, s, Ρ): we require that at two possibly different scales r and s, the function is well approximated by the linear map L. It is also open.

We claim that the differentiability set of f is exactly D = β‹‚ Ξ΅ > 0, ⋃ Ξ΄ > 0, β‹‚ r, s < Ξ΄, ⋃ L, B (L, r, s, Ξ΅). In other words, for any Ξ΅ > 0, we require that there is a size Ξ΄ such that, for any two scales below this size, the function is well approximated by a linear map, common to the two scales.

The set ⋃ L, B (L, r, s, Ξ΅) is open, as a union of open sets. Converting the intersections and unions to countable ones (using real numbers of the form 2 ^ (-n)), it follows that the differentiability set is measurable.

To prove the claim, there are two inclusions. One is trivial: if the function is differentiable at x, then x belongs to D (just take L to be the derivative, and use that the differentiability exactly says that the map is well approximated by L). This is proved in mem_A_of_differentiable and differentiable_set_subset_D.

For the other direction, the difficulty is that L in the union may depend on Ξ΅, r, s. The key point is that, in fact, it doesn't depend too much on them. First, if x belongs both to A (L, r, Ξ΅) and A (L', r, Ξ΅), then L and L' have to be close on a shell, and thus β€–L - L'β€– is bounded by Ξ΅ (see norm_sub_le_of_mem_A). Assume now x ∈ D. If one has two maps L and L' such that x belongs to A (L, r, Ξ΅) and to A (L', r', Ξ΅'), one deduces that L is close to L' by arguing as follows. Consider another scale s smaller than r and r'. Take a linear map L₁ that approximates f around x both at scales r and s w.r.t. Ξ΅ (it exists as x belongs to D). Take also Lβ‚‚ that approximates f around x both at scales r' and s w.r.t. Ξ΅'. Then L₁ is close to L (as they are close on a shell of radius r), and Lβ‚‚ is close to L₁ (as they are close on a shell of radius s), and L' is close to Lβ‚‚ (as they are close on a shell of radius r'). It follows that L is close to L', as we claimed.

It follows that the different approximating linear maps that show up form a Cauchy sequence when Ξ΅ tends to 0. When the target space is complete, this sequence converges, to a limit f'. With the same kind of arguments, one checks that f is differentiable with derivative f'.

To show that the derivative itself is measurable, add in the definition of B and D a set K of continuous linear maps to which L should belong. Then, when K is complete, the set D K is exactly the set of points where f is differentiable with a derivative in K.

Tags #

derivative, measurable function, Borel Οƒ-algebra

theorem ContinuousLinearMap.measurable_applyβ‚‚ {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField π•œ] [NormedAddCommGroup E] [NormedSpace π•œ E] [NormedAddCommGroup F] [NormedSpace π•œ F] [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither (E β†’L[π•œ] F) E] [MeasurableSpace F] [BorelSpace F] :
Measurable fun p => ↑p.fst p.snd
def FDerivMeasurableAux.A {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) (L : E β†’L[π•œ] F) (r : ℝ) (Ξ΅ : ℝ) :
Set E

The set A f L r Ξ΅ is the set of points x around which the function f is well approximated at scale r by the linear map L, up to an error Ξ΅. We tweak the definition to make sure that this is an open set.

Instances For
    def FDerivMeasurableAux.B {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) (K : Set (E β†’L[π•œ] F)) (r : ℝ) (s : ℝ) (Ξ΅ : ℝ) :
    Set E

    The set B f K r s Ξ΅ is the set of points x around which there exists a continuous linear map L belonging to K (a given set of continuous linear maps) that approximates well the function f (up to an error Ξ΅), simultaneously at scales r and s.

    Instances For
      def FDerivMeasurableAux.D {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) (K : Set (E β†’L[π•œ] F)) :
      Set E

      The set D f K is a complicated set constructed using countable intersections and unions. Its main use is that, when K is complete, it is exactly the set of points where f is differentiable, with a derivative in K.

      Instances For
        theorem FDerivMeasurableAux.isOpen_A {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (L : E β†’L[π•œ] F) (r : ℝ) (Ξ΅ : ℝ) :
        theorem FDerivMeasurableAux.isOpen_B {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {K : Set (E β†’L[π•œ] F)} {r : ℝ} {s : ℝ} {Ξ΅ : ℝ} :
        theorem FDerivMeasurableAux.A_mono {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (L : E β†’L[π•œ] F) (r : ℝ) {Ξ΅ : ℝ} {Ξ΄ : ℝ} (h : Ξ΅ ≀ Ξ΄) :
        theorem FDerivMeasurableAux.le_of_mem_A {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {r : ℝ} {Ξ΅ : ℝ} {L : E β†’L[π•œ] F} {x : E} (hx : x ∈ FDerivMeasurableAux.A f L r Ξ΅) {y : E} {z : E} (hy : y ∈ Metric.closedBall x (r / 2)) (hz : z ∈ Metric.closedBall x (r / 2)) :
        β€–f z - f y - ↑L (z - y)β€– ≀ Ξ΅ * r
        theorem FDerivMeasurableAux.mem_A_of_differentiable {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {Ξ΅ : ℝ} (hΞ΅ : 0 < Ξ΅) {x : E} (hx : DifferentiableAt π•œ f x) :
        βˆƒ R, R > 0 ∧ βˆ€ (r : ℝ), r ∈ Set.Ioo 0 R β†’ x ∈ FDerivMeasurableAux.A f (fderiv π•œ f x) r Ξ΅
        theorem FDerivMeasurableAux.norm_sub_le_of_mem_A {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {c : π•œ} (hc : 1 < β€–cβ€–) {r : ℝ} {Ξ΅ : ℝ} (hΞ΅ : 0 < Ξ΅) (hr : 0 < r) {x : E} {L₁ : E β†’L[π•œ] F} {Lβ‚‚ : E β†’L[π•œ] F} (h₁ : x ∈ FDerivMeasurableAux.A f L₁ r Ξ΅) (hβ‚‚ : x ∈ FDerivMeasurableAux.A f Lβ‚‚ r Ξ΅) :
        β€–L₁ - Lβ‚‚β€– ≀ 4 * β€–cβ€– * Ξ΅
        theorem FDerivMeasurableAux.differentiable_set_subset_D {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (K : Set (E β†’L[π•œ] F)) :
        {x | DifferentiableAt π•œ f x ∧ fderiv π•œ f x ∈ K} βŠ† FDerivMeasurableAux.D f K

        Easy inclusion: a differentiability point with derivative in K belongs to D f K.

        theorem FDerivMeasurableAux.D_subset_differentiable_set {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {K : Set (E β†’L[π•œ] F)} (hK : IsComplete K) :
        FDerivMeasurableAux.D f K βŠ† {x | DifferentiableAt π•œ f x ∧ fderiv π•œ f x ∈ K}

        Harder inclusion: at a point in D f K, the function f has a derivative, in K.

        theorem FDerivMeasurableAux.differentiable_set_eq_D {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (K : Set (E β†’L[π•œ] F)) (hK : IsComplete K) :
        {x | DifferentiableAt π•œ f x ∧ fderiv π•œ f x ∈ K} = FDerivMeasurableAux.D f K
        theorem measurableSet_of_differentiableAt_of_isComplete (π•œ : Type u_1) [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) [MeasurableSpace E] [OpensMeasurableSpace E] {K : Set (E β†’L[π•œ] F)} (hK : IsComplete K) :
        MeasurableSet {x | DifferentiableAt π•œ f x ∧ fderiv π•œ f x ∈ K}

        The set of differentiability points of a function, with derivative in a given complete set, is Borel-measurable.

        theorem measurableSet_of_differentiableAt (π•œ : Type u_1) [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) [MeasurableSpace E] [OpensMeasurableSpace E] [CompleteSpace F] :
        MeasurableSet {x | DifferentiableAt π•œ f x}

        The set of differentiability points of a function taking values in a complete space is Borel-measurable.

        theorem measurable_fderiv (π•œ : Type u_1) [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) [MeasurableSpace E] [OpensMeasurableSpace E] [CompleteSpace F] :
        Measurable (fderiv π•œ f)
        theorem measurable_fderiv_apply_const (π•œ : Type u_1) [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) [MeasurableSpace E] [OpensMeasurableSpace E] [CompleteSpace F] [MeasurableSpace F] [BorelSpace F] (y : E) :
        Measurable fun x => ↑(fderiv π•œ f x) y
        theorem measurable_deriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [MeasurableSpace π•œ] [OpensMeasurableSpace π•œ] [MeasurableSpace F] [BorelSpace F] (f : π•œ β†’ F) :
        theorem stronglyMeasurable_deriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [MeasurableSpace π•œ] [OpensMeasurableSpace π•œ] [h : SecondCountableTopologyEither π•œ F] (f : π•œ β†’ F) :
        theorem aemeasurable_deriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [MeasurableSpace π•œ] [OpensMeasurableSpace π•œ] [MeasurableSpace F] [BorelSpace F] (f : π•œ β†’ F) (ΞΌ : MeasureTheory.Measure π•œ) :
        theorem aestronglyMeasurable_deriv {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace F] [MeasurableSpace π•œ] [OpensMeasurableSpace π•œ] [SecondCountableTopologyEither π•œ F] (f : π•œ β†’ F) (ΞΌ : MeasureTheory.Measure π•œ) :
        def RightDerivMeasurableAux.A {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : ℝ β†’ F) (L : F) (r : ℝ) (Ξ΅ : ℝ) :

        The set A f L r Ξ΅ is the set of points x around which the function f is well approximated at scale r by the linear map h ↦ h β€’ L, up to an error Ξ΅. We tweak the definition to make sure that this is open on the right.

        Instances For
          def RightDerivMeasurableAux.B {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : ℝ β†’ F) (K : Set F) (r : ℝ) (s : ℝ) (Ξ΅ : ℝ) :

          The set B f K r s Ξ΅ is the set of points x around which there exists a vector L belonging to K (a given set of vectors) such that h β€’ L approximates well f (x + h) (up to an error Ξ΅), simultaneously at scales r and s.

          Instances For

            The set D f K is a complicated set constructed using countable intersections and unions. Its main use is that, when K is complete, it is exactly the set of points where f is differentiable, with a derivative in K.

            Instances For
              theorem RightDerivMeasurableAux.B_mem_nhdsWithin_Ioi {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ β†’ F} {K : Set F} {r : ℝ} {s : ℝ} {Ξ΅ : ℝ} {x : ℝ} (hx : x ∈ RightDerivMeasurableAux.B f K r s Ξ΅) :
              theorem RightDerivMeasurableAux.A_mono {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ β†’ F} (L : F) (r : ℝ) {Ξ΅ : ℝ} {Ξ΄ : ℝ} (h : Ξ΅ ≀ Ξ΄) :
              theorem RightDerivMeasurableAux.le_of_mem_A {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ β†’ F} {r : ℝ} {Ξ΅ : ℝ} {L : F} {x : ℝ} (hx : x ∈ RightDerivMeasurableAux.A f L r Ξ΅) {y : ℝ} {z : ℝ} (hy : y ∈ Set.Icc x (x + r / 2)) (hz : z ∈ Set.Icc x (x + r / 2)) :
              β€–f z - f y - (z - y) β€’ Lβ€– ≀ Ξ΅ * r
              theorem RightDerivMeasurableAux.mem_A_of_differentiable {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ β†’ F} {Ξ΅ : ℝ} (hΞ΅ : 0 < Ξ΅) {x : ℝ} (hx : DifferentiableWithinAt ℝ f (Set.Ici x) x) :
              βˆƒ R, R > 0 ∧ βˆ€ (r : ℝ), r ∈ Set.Ioo 0 R β†’ x ∈ RightDerivMeasurableAux.A f (derivWithin f (Set.Ici x) x) r Ξ΅
              theorem RightDerivMeasurableAux.norm_sub_le_of_mem_A {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ β†’ F} {r : ℝ} {x : ℝ} (hr : 0 < r) (Ξ΅ : ℝ) {L₁ : F} {Lβ‚‚ : F} (h₁ : x ∈ RightDerivMeasurableAux.A f L₁ r Ξ΅) (hβ‚‚ : x ∈ RightDerivMeasurableAux.A f Lβ‚‚ r Ξ΅) :
              β€–L₁ - Lβ‚‚β€– ≀ 4 * Ξ΅

              Easy inclusion: a differentiability point with derivative in K belongs to D f K.

              Harder inclusion: at a point in D f K, the function f has a derivative, in K.

              The set of right differentiability points of a function, with derivative in a given complete set, is Borel-measurable.

              The set of right differentiability points of a function taking values in a complete space is Borel-measurable.

              The set of right differentiability points of a function taking values in a complete space is Borel-measurable.

              theorem FDerivMeasurableAux.isOpen_A_with_param {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] [LocallyCompactSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {Ξ± : Type u_4} [TopologicalSpace Ξ±] {f : Ξ± β†’ E β†’ F} {r : ℝ} {s : ℝ} (hf : Continuous (Function.uncurry f)) (L : E β†’L[π•œ] F) :
              IsOpen {p | p.snd ∈ FDerivMeasurableAux.A (f p.fst) L r s}
              theorem FDerivMeasurableAux.isOpen_B_with_param {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] [LocallyCompactSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {Ξ± : Type u_4} [TopologicalSpace Ξ±] {f : Ξ± β†’ E β†’ F} {r : ℝ} {s : ℝ} {t : ℝ} (hf : Continuous (Function.uncurry f)) (K : Set (E β†’L[π•œ] F)) :
              IsOpen {p | p.snd ∈ FDerivMeasurableAux.B (f p.fst) K r s t}
              theorem measurableSet_of_differentiableAt_of_isComplete_with_param {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] [LocallyCompactSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {Ξ± : Type u_4} [TopologicalSpace Ξ±] [MeasurableSpace Ξ±] [MeasurableSpace E] [OpensMeasurableSpace Ξ±] [OpensMeasurableSpace E] {f : Ξ± β†’ E β†’ F} (hf : Continuous (Function.uncurry f)) {K : Set (E β†’L[π•œ] F)} (hK : IsComplete K) :
              MeasurableSet {p | DifferentiableAt π•œ (f p.fst) p.snd ∧ fderiv π•œ (f p.fst) p.snd ∈ K}
              theorem measurableSet_of_differentiableAt_with_param (π•œ : Type u_1) [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] [LocallyCompactSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {Ξ± : Type u_4} [TopologicalSpace Ξ±] [MeasurableSpace Ξ±] [MeasurableSpace E] [OpensMeasurableSpace Ξ±] [OpensMeasurableSpace E] {f : Ξ± β†’ E β†’ F} [CompleteSpace F] (hf : Continuous (Function.uncurry f)) :
              MeasurableSet {p | DifferentiableAt π•œ (f p.fst) p.snd}

              The set of differentiability points of a continuous function depending on a parameter taking values in a complete space is Borel-measurable.

              theorem measurable_fderiv_with_param (π•œ : Type u_1) [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] [LocallyCompactSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {Ξ± : Type u_4} [TopologicalSpace Ξ±] [MeasurableSpace Ξ±] [MeasurableSpace E] [OpensMeasurableSpace Ξ±] [OpensMeasurableSpace E] {f : Ξ± β†’ E β†’ F} [CompleteSpace F] (hf : Continuous (Function.uncurry f)) :
              Measurable fun p => fderiv π•œ (f p.fst) p.snd
              theorem measurable_fderiv_apply_const_with_param (π•œ : Type u_1) [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] [LocallyCompactSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {Ξ± : Type u_4} [TopologicalSpace Ξ±] [MeasurableSpace Ξ±] [MeasurableSpace E] [OpensMeasurableSpace Ξ±] [OpensMeasurableSpace E] {f : Ξ± β†’ E β†’ F} [CompleteSpace F] [MeasurableSpace F] [BorelSpace F] (hf : Continuous (Function.uncurry f)) (y : E) :
              Measurable fun p => ↑(fderiv π•œ (f p.fst) p.snd) y
              theorem measurable_deriv_with_param {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {Ξ± : Type u_4} [TopologicalSpace Ξ±] [MeasurableSpace Ξ±] [OpensMeasurableSpace Ξ±] [CompleteSpace F] [LocallyCompactSpace π•œ] [MeasurableSpace π•œ] [OpensMeasurableSpace π•œ] [MeasurableSpace F] [BorelSpace F] {f : Ξ± β†’ π•œ β†’ F} (hf : Continuous (Function.uncurry f)) :
              Measurable fun p => deriv (f p.fst) p.snd
              theorem stronglyMeasurable_deriv_with_param {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {Ξ± : Type u_4} [TopologicalSpace Ξ±] [MeasurableSpace Ξ±] [OpensMeasurableSpace Ξ±] [CompleteSpace F] [LocallyCompactSpace π•œ] [MeasurableSpace π•œ] [OpensMeasurableSpace π•œ] [h : SecondCountableTopologyEither Ξ± F] {f : Ξ± β†’ π•œ β†’ F} (hf : Continuous (Function.uncurry f)) :
              MeasureTheory.StronglyMeasurable fun p => deriv (f p.fst) p.snd
              theorem aemeasurable_deriv_with_param {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {Ξ± : Type u_4} [TopologicalSpace Ξ±] [MeasurableSpace Ξ±] [OpensMeasurableSpace Ξ±] [CompleteSpace F] [LocallyCompactSpace π•œ] [MeasurableSpace π•œ] [OpensMeasurableSpace π•œ] [MeasurableSpace F] [BorelSpace F] {f : Ξ± β†’ π•œ β†’ F} (hf : Continuous (Function.uncurry f)) (ΞΌ : MeasureTheory.Measure (Ξ± Γ— π•œ)) :
              AEMeasurable fun p => deriv (f p.fst) p.snd
              theorem aestronglyMeasurable_deriv_with_param {π•œ : Type u_1} [NontriviallyNormedField π•œ] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {Ξ± : Type u_4} [TopologicalSpace Ξ±] [MeasurableSpace Ξ±] [OpensMeasurableSpace Ξ±] [CompleteSpace F] [LocallyCompactSpace π•œ] [MeasurableSpace π•œ] [OpensMeasurableSpace π•œ] [SecondCountableTopologyEither Ξ± F] {f : Ξ± β†’ π•œ β†’ F} (hf : Continuous (Function.uncurry f)) (ΞΌ : MeasureTheory.Measure (Ξ± Γ— π•œ)) :
              MeasureTheory.AEStronglyMeasurable (fun p => deriv (f p.fst) p.snd) ΞΌ