Bounds on derivatives of a parametric integral over $[0,1]$

Proved

FiniteEnergyPlane.norm_iteratedFDeriv_intervalIntegral_le

by Mazecto · Nov 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysisnonlinear-analysis

Let $H$ be a finite-dimensional real normed space, $G$ a real Banach space, and $F : H \to \mathbb{R} \to G$ with $(x, t) \mapsto F(x, t)$ of class $C^\infty$ . If $\|D^k_x F(x, t)\| \le C$ for all $t \in [0, 1]$ , then $\big\|D^k\big(x \mapsto \int_0^1 F(x, t)\,dt\big)(x)\big\| \le C$ .

Role. Controls derivatives of Hadamard-type quotients $\int_0^1 Dk(x, \theta w)\,d\theta$ .

Preamble

import Mathlib

open Metric Set Filter Topology MeasureTheory
open scoped ContDiff

Formal statement

namespace FiniteEnergyPlane

/-- For `F : H → ℝ → G` jointly `C^∞` with `H` finite-dimensional, a bound on the `k`-th
`x`-derivative of `F x t` for `t ∈ [0, 1]` bounds the `k`-th derivative of `x ↦ ∫₀¹ F x t dt`. -/
theorem norm_iteratedFDeriv_intervalIntegral_le {H G : Type*} [NormedAddCommGroup H]
    [NormedSpace ℝ H] [FiniteDimensional ℝ H] [NormedAddCommGroup G] [NormedSpace ℝ G]
    [CompleteSpace G] {F : H → ℝ → G} (hF : ContDiff ℝ ∞ (Function.uncurry F)) (k : ℕ)
    (x : H) (C : ℝ) (hC : ∀ t ∈ Icc (0 : ℝ) 1, ‖iteratedFDeriv ℝ k (fun x => F x t) x‖ ≤ C) :
    ‖iteratedFDeriv ℝ k (fun x => ∫ t in (0 : ℝ)..1, F x t) x‖ ≤ C := by
  sorry

end FiniteEnergyPlane

Source

Toward U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. AMS 364 (2012), arXiv:0812.4076, Lemmas 6.10 and 6.20 (families of fast planes); operators in the setting of C. Wendl, Lectures on Holomorphic Curves in Symplectic and Contact Geometry, arXiv:1011.1690, Ch. 4

View graph

Bounds on derivatives of a parametric integral over [0,1][0,1][0,1]

Bounds on derivatives of a parametric integral over $[0,1]$