Integrability of dominated iterated derivatives

If the iterated derivatives of a smooth function have integrable envelopes, uniformly on unit translates, each derivative below the available differentiability order is continuously differentiable and integrable, and its first derivative has an integrable envelope on unit translates (ContDiff.iteratedFDeriv_dominated). These properties supply the analytic data for repeated differentiation under the integral sign.

theorem ContDiff.iteratedFDeriv_dominated {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SecondCountableTopology E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} {N : ℕ∞} {f : E → F} (hf : ContDiff 𝕜 (↑N) f) (hfφ : ∀ (n : ℕ), ↑n ≤ N → ∃ (φ : E → ℝ), MeasureTheory.Integrable φ μ ∧ ∀ (z h : E), ‖h‖ ≤ 1 → ‖iteratedFDeriv 𝕜 n f (z + h)‖ ≤ φ z) {n : ℕ} (hn : ↑(n + 1) ≤ N) : ContDiff 𝕜 1 (iteratedFDeriv 𝕜 n f) ∧ MeasureTheory.Integrable (iteratedFDeriv 𝕜 n f) μ ∧ ∃ (φ : E → ℝ), MeasureTheory.Integrable φ μ ∧ ∀ (z h : E), ‖h‖ ≤ 1 → ‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) (z + h)‖ ≤ φ z

If a C^N function has integrable envelopes for its iterated derivatives on unit translates, then each derivative of order n with n + 1 ≤ N is C¹ and integrable, and its first derivative has an integrable envelope on unit translates.