Local smoothness of actual solution curves from their integral equation.

theorem AVenhance.Infra.Section4.amnr_contDiffAt_of_invertible_left_equation {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {P : F → F} {Q R : E → F} {x : E} (hQ : ContinuousAt Q x) (hP : ContDiffAt ℝ (↑⊤) P (Q x)) (e : F ≃L[ℝ] F) (hD : HasFDerivAt P (↑e) (Q x)) (hR : ContDiffAt ℝ (↑⊤) R x) (heq : ∀ (y : E), P (Q y) = R y) : ContDiffAt ℝ (↑⊤) Q x

A continuous family solving a smooth equation with invertible derivative is smooth. Only continuity of the solution family is assumed; its derivatives are obtained from the inverse function theorem and the actual equation.

def AVenhance.Infra.Section4.amnrCurveResidual {K E : Type} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ × E → E) (hf : Continuous f) (η : C(K, ℝ)) (V : C(K, E) →L[ℝ] C(K, E)) (u : C(K, E)) : C(K, E)

The actual nonlinear Volterra residual whose zero equation determines an ODE curve from its constant initial data.

Equations

• AVenhance.Infra.Section4.amnrCurveResidual f hf η V u = u - V (AVenhance.Infra.Section4.amnrCurveJointCompose f hf η u)

theorem AVenhance.Infra.Section4.amnrCurveResidual_contDiff_infty {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × E → E} (hf : ContDiff ℝ (↑⊤) f) (hbound : ∀ (j : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ j f z‖ ≤ C) (η : C(K, ℝ)) (V : C(K, E) →L[ℝ] C(K, E)) : ContDiff ℝ (↑⊤) (amnrCurveResidual f ⋯ η V)

The actual residual inherits all-order smoothness from proved primitive field bounds and the actual bounded time-integration operator.

theorem AVenhance.Infra.Section4.amnrCurveResidual_hasFDerivAt {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × E → E} (hf : ContDiff ℝ (↑⊤) f) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ 2 f z‖ ≤ C) (η : C(K, ℝ)) (V : C(K, E) →L[ℝ] C(K, E)) (u : C(K, E)) : HasFDerivAt (amnrCurveResidual f ⋯ η V) (1 - V ∘SL amnrCurveOperator (amnrCurveJointCompose (amnrStateDerivative f) ⋯ η u)) u

Differentiating the residual gives identity minus the linear Volterra operator along the actual trajectory.

theorem AVenhance.Infra.Section4.amnrCurveResidual_solution_contDiffAt {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ × E → E} (hf : ContDiff ℝ (↑⊤) f) (hbound : ∀ (j : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ j f z‖ ≤ C) (η : C(K, ℝ)) (V : C(K, E) →L[ℝ] C(K, E)) {M : ℝ} (hM : 0 ≤ M) (hstate : ∀ (z : ℝ × E), ‖amnrStateDerivative f z‖ ≤ M) (hsmall : ‖V‖ * M < 1) {Q : E → C(K, E)} {x : E} (hQ : ContinuousAt Q x) (heq : ∀ (y : E), amnrCurveResidual f ⋯ η V (Q y) = ContinuousMap.const K y) : ContDiffAt ℝ (↑⊤) Q x

A continuous family solving the actual Volterra equation is smooth in its initial datum on a short interval. Only the primitive field derivative and integration length are used to prove invertibility.