Iterated ifferentiation under the integral sign

theorem deriv_interval_integral_of_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → ℝ → E} {a b t : ℝ} (fc : ContDiff ℝ ⊤ (Function.uncurry f)) (ab : a ≤ b) : deriv (fun (t : ℝ) => ∫ (x : ℝ) in a..b, f t x) t = ∫ (x : ℝ) in a..b, deriv (fun (t : ℝ) => f t x) t

hasDerivAt_integral_of_dominated_loc_of_deriv_le for smooth functions

theorem iteratedDeriv_interval_integral_of_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → ℝ → E} {a b t : ℝ} (fc : ContDiff ℝ ⊤ (Function.uncurry f)) (ab : a ≤ b) (n : ℕ) : iteratedDeriv n (fun (t : ℝ) => ∫ (x : ℝ) in a..b, f t x) t = ∫ (x : ℝ) in a..b, iteratedDeriv n (fun (t : ℝ) => f t x) t

Iterated differentiation under the integral sign