Gevrey Functions

theorem EulerGevreyFunctions.product_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f g : E → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (R A B : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) (hb₁ : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ A * EulerGevrey.majorant R 0 n) (hb₂ : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ B * EulerGevrey.majorant R 0 n) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (fun (y : E) => f y * g y) x‖ ≤ 3 * A * B * EulerGevrey.majorant R 0 n

theorem EulerGevreyFunctions.linear_composition_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (L : E →L[ℝ] ℝ) (R A C : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (_hC : 0 ≤ C) (hL : ‖L‖ ≤ C) (hb : ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n f x| ≤ A * EulerGevrey.majorant R 0 n) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (f ∘ ⇑L) x‖ ≤ A * EulerGevrey.majorant (R * C) 0 n

theorem EulerGevreyFunctions.affine_composition_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (L : E →L[ℝ] ℝ) (a R A C : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hC : 0 ≤ C) (hL : ‖L‖ ≤ C) (hb : ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n f x| ≤ A * EulerGevrey.majorant R 0 n) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (fun (y : E) => f (L y + a)) x‖ ≤ A * EulerGevrey.majorant (R * C) 0 n

theorem EulerGevreyFunctions.finite_product_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} (u : Finset ι) (f : ι → E → ℝ) (hf : ∀ i ∈ u, ContDiff ℝ (↑⊤) (f i)) (R A : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hb : ∀ i ∈ u, ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n (f i) x‖ ≤ A * EulerGevrey.majorant R 0 n) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (fun (y : E) => ∏ i ∈ u, f i y) x‖ ≤ (3 * A) ^ u.card * EulerGevrey.majorant R 0 n