A uniform bound at each fixed derivative order

On a compact set where every multi-index derivative is continuous, all derivatives of one fixed order k are bounded by a single constant, because there are finitely many multi-indices of order k. This starts the induction on the derivative order in the proof of thm:analytic:interior.

theorem CIV.finite_setOf_multiIndex_order (k : ℕ) : {γ : Fin 3 → ℕ | γ 0 + γ 1 + γ 2 = k}.Finite

The multi-indices of a fixed order form a finite set.

theorem CIV.exists_bound_multiPartial_of_continuousOn {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Kc : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hK : IsCompact Kc) (hcont : ∀ (γ : Fin 3 → ℕ), ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => multiPartial g γ z) Kc) (k : ℕ) : ∃ (N : ℝ), 0 ≤ N ∧ ∀ z ∈ Kc, ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k → |multiPartial g γ z| ≤ N

On a compact set where every multi-index derivative is continuous, the derivatives of one fixed order are bounded by one constant.