Factorial bounds for genuine operator-valued derivatives

These estimates use actual iterated Fréchet derivatives and bounded linear or bilinear maps. They transfer coefficient bounds to the time multipliers, transported variational forms, and right sides of the constructed inverses.

theorem EulerOperatorGevreyCalculus.majorant_radius_mono (R S : ℝ) (hR : 0 ≤ R) (hRS : R ≤ S) (d n : ℕ) : EulerGevrey.majorant R d n ≤ EulerGevrey.majorant S d n

Enlarging the radius enlarges the factorial majorant.

theorem EulerOperatorGevreyCalculus.const_bound {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (v : E) (R C : ℝ) (hR : 0 ≤ R) (hv : ‖v‖ ≤ C) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (x : P) => v) x‖ ≤ C * EulerGevrey.majorant R 0 n

A constant field satisfies the order-zero multiplier bound.

theorem EulerOperatorGevreyCalculus.linear_bound {P : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (R A : ℝ) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ A * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => L (f y)) x‖ ≤ ‖L‖ * A * EulerGevrey.majorant R d n

Bounded linear maps preserve every factorial shift.

theorem EulerOperatorGevreyCalculus.contraction_bound {P : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) (hL : ‖L‖ ≤ 1) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (R A : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ A * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => L (f y)) x‖ ≤ A * EulerGevrey.majorant R d n

A linear contraction does not enlarge a factorial multiplier constant.

theorem EulerOperatorGevreyCalculus.bilinear_bound {P : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) (hB : ‖B‖ ≤ 1) (f : P → E) (g : P → F) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (R A C : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hC : 0 ≤ C) (d e : ℕ) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ A * EulerGevrey.majorant R d n) (hc : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n g x‖ ≤ C * EulerGevrey.majorant R e n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (B (f y)) (g y)) x‖ ≤ 3 * A * C * EulerGevrey.majorant R (d + e) n

The shifted product bound for any bilinear contraction.

theorem EulerOperatorGevreyCalculus.clm_apply_bound {P : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : P → E →L[ℝ] F) (u : P → E) (hA : ContDiff ℝ (↑⊤) A) (hu : ContDiff ℝ (↑⊤) u) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (d e : ℕ) (hcoeff : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant R d n) (hfield : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n u x‖ ≤ D * EulerGevrey.majorant R e n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (A y) (u y)) x‖ ≤ 3 * C * D * EulerGevrey.majorant R (d + e) n

Actual operator application has the shifted factorial product bound.

theorem EulerOperatorGevreyCalculus.clm_comp_bound {P : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (A : P → F →L[ℝ] G) (B : P → E →L[ℝ] F) (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (d e : ℕ) (hcoeff : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant R d n) (hfield : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n B x‖ ≤ D * EulerGevrey.majorant R e n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => A y ∘SL B y) x‖ ≤ 3 * C * D * EulerGevrey.majorant R (d + e) n

Composition of actual parameterized operators has the same product bound.

theorem EulerOperatorGevreyCalculus.add_bound {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (f g : P → E) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (R A B : ℝ) (d : ℕ) (ha : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ A * EulerGevrey.majorant R d n) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n g x‖ ≤ B * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => f y + g y) x‖ ≤ (A + B) * EulerGevrey.majorant R d n

Adding actual jets adds the multiplier constants.

theorem EulerOperatorGevreyCalculus.sub_bound {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (f g : P → E) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (R A B : ℝ) (d : ℕ) (ha : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ A * EulerGevrey.majorant R d n) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n g x‖ ≤ B * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => f y - g y) x‖ ≤ (A + B) * EulerGevrey.majorant R d n

Subtracting actual jets adds the multiplier constants.

theorem EulerOperatorGevreyCalculus.clm_comp_const_right_bound {P : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (A : P → F →L[ℝ] G) (B : E →L[ℝ] F) (hA : ContDiff ℝ (↑⊤) A) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => A y ∘SL B) x‖ ≤ ‖B‖ * C * EulerGevrey.majorant R d n

Composition with a fixed operator on the right costs its operator norm.

theorem EulerOperatorGevreyCalculus.clm_comp_const_left_bound {P : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (A : F →L[ℝ] G) (B : P → E →L[ℝ] F) (hB : ContDiff ℝ (↑⊤) B) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n B x‖ ≤ C * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => A ∘SL B y) x‖ ≤ ‖A‖ * C * EulerGevrey.majorant R d n

Composition with a fixed operator on the left costs its operator norm.

theorem EulerOperatorGevreyCalculus.neg_bound {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : P → E) (R C : ℝ) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ C * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => -f y) x‖ ≤ C * EulerGevrey.majorant R d n

Negating a field leaves all factorial bounds unchanged.

theorem EulerOperatorGevreyCalculus.adjoint_bound {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A : P → U →L[ℝ] E) (hA : ContDiff ℝ (↑⊤) A) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => ContinuousLinearMap.adjoint (A y)) x‖ ≤ C * EulerGevrey.majorant R d n

Taking the actual Hilbert adjoint preserves the multiplier constant.