Differentiating an actual L²-valued family by dominated ordinary derivatives.

theorem EulerLpDerivative.hasFDerivAt_of_dominated {X : Type u_1} {P : Type u_2} {V : Type u_3} [MeasurableSpace X] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (μ : MeasureTheory.Measure X) (U : P → ↥(MeasureTheory.Lp V 2 μ)) (F : P → X → V) (hU : ∀ (a : P), ↑↑(U a) =ᵐ[μ] F a) (D : ↥(MeasureTheory.Lp (P →L[ℝ] V) 2 μ)) (hpoint : ∀ᵐ (x : X) ∂μ, HasFDerivAt (fun (a : P) => F a x) (↑↑D x) 0) (M : X → ℝ) (hM : MeasureTheory.MemLp M 2 μ) (hM0 : ∀ᵐ (x : X) ∂μ, 0 ≤ M x) (hbound : ∀ᶠ (a : P) in nhds 0, ∀ᵐ (x : X) ∂μ, ‖F a x - F 0 x‖ ≤ M x * ‖a‖) : HasFDerivAt U (derivativeMap μ D) 0

A pointwise derivative and a square-integrable increment bound give a genuine L² Fréchet derivative.