Derivative bounds for partial maps along a compact parameter

import Mathlib

open Metric Set Filter Topology BoundedContinuousFunction
open scoped ContDiff

namespace Nemytskii

/-- If `Ψ : P × E → F` is `C^∞` (with `P`, `E` proper) and `p : X → P` is continuous with values
in a compact set, then the partial maps `a ↦ Ψ (p x, a)` are `C^∞`, and each of their derivatives
is jointly continuous in `(x, a)` and bounded on `X × closedBall 0 R` for every `R`. -/
theorem iteratedFDeriv_bounds_of_comp_compact {X : Type*} [TopologicalSpace X]
    {P E F : Type*} [NormedAddCommGroup P] [NormedSpace ℝ P] [ProperSpace P]
    [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    (Ψ : P × E → F) (hΨ : ContDiff ℝ ∞ Ψ) (p : X → P) (hp : Continuous p) (K : Set P)
    (hK : IsCompact K) (hpK : ∀ x, p x ∈ K) :
    (∀ x, ContDiff ℝ ∞ ((fun x a => Ψ (p x, a)) x)) ∧
      (∀ k : ℕ, Continuous (fun y : X × E => iteratedFDeriv ℝ k ((fun x a => Ψ (p x, a)) y.1) y.2)) ∧
      ∀ (k : ℕ) (R : ℝ), ∃ C : ℝ, ∀ x, ∀ a ∈ closedBall (0 : E) R,
        ‖iteratedFDeriv ℝ k ((fun x a => Ψ (p x, a)) x) a‖ ≤ C := by
  sorry

end Nemytskii