Quantitative all-order differentiation of a small linear fixed equation.

def AVenhance.Infra.Section4.amnrJacobianJetConstant (C : ℝ) : ℕ → ℝ

Constants for successive derivatives of a Jacobian fixed equation. They depend only on the finite primitive derivative bound and the order.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section4.amnrJacobianJetConstant C 0 = 2

theorem AVenhance.Infra.Section4.amnrJacobianJetConstant_two_le (C : ℝ) (n : ℕ) : 2 ≤ amnrJacobianJetConstant C n

theorem AVenhance.Infra.Section4.amnrJacobianJetConstant_mono (C : ℝ) : Monotone (amnrJacobianJetConstant C)

theorem AVenhance.Infra.Section4.amnrJacobianJet_absorb {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {J : E → E →L[ℝ] F} {W : E → F →L[ℝ] F} (hJ : ContDiff ℝ (↑⊤) J) (hW : ContDiff ℝ (↑⊤) W) (R : E →L[ℝ] F) (heq : ∀ (y : E), J y = R + W y ∘SL J y) (x : E) (n : ℕ) (hn : 1 ≤ n) (hsmall : ‖W x‖ ≤ 1 / 2) {B K : ℝ} (hB : 0 ≤ B) (hK : 0 ≤ K) (hcoeff : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i W x‖ ≤ B) (hlower : ∀ i < n, ‖iteratedFDeriv ℝ i J x‖ ≤ K) : ‖iteratedFDeriv ℝ n J x‖ ≤ 2 * 2 ^ n * B * K

Absorb the undifferentiated small coefficient after differentiating an actual linear fixed equation. Higher coefficient and lower solution jets are used only in the strictly lower terms of Leibniz's formula.

theorem AVenhance.Infra.Section4.amnrJacobianJet_norm_le_of_fixed_equation {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Q : E → F} {A : F → F →L[ℝ] F} (hQ : ContDiff ℝ (↑⊤) Q) (hA : ContDiff ℝ (↑⊤) A) (R : E →L[ℝ] F) (hR : ‖R‖ ≤ 1) (heq : ∀ (y : E), fderiv ℝ Q y = R + A (Q y) ∘SL fderiv ℝ Q y) (x : E) (hsmall : ‖A (Q x)‖ ≤ 1 / 2) {C : ℝ} {N : ℕ} (hprimitive : ∀ i ≤ N, ‖iteratedFDeriv ℝ i A (Q x)‖ ≤ C) (n : ℕ) (hbudget : n ≤ N) : ‖iteratedFDeriv ℝ n (fderiv ℝ Q) x‖ ≤ amnrJacobianJetConstant C n

All Jacobian jets of a smooth solution of the actual small linear fixed equation are bounded by finite primitive constants. This induction does not assume a bound for the highest derivative it proves.