Smooth parameter dependence from the actual local Volterra equation.
theorem
AVenhance.Infra.Section4.amnrCurveJointCompose_hasFDerivAt_local
{K E : Type}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{f : ℝ × E → E}
(hf : ContDiff ℝ (↑⊤) f)
(η : C(K, ℝ))
(u : C(K, E))
:
HasFDerivAt (amnrCurveJointCompose f ⋯ η) (amnrCurveOperator (amnrCurveJointCompose (amnrStateDerivative f) ⋯ η u)) u
The substitution derivative is the actual pointwise primitive state Jacobian operator, with no global derivative bound premise.
theorem
AVenhance.Infra.Section4.amnrCurveResidual_contDiff_infty_local
{K E : Type}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{f : ℝ × E → E}
(hf : ContDiff ℝ (↑⊤) f)
(η : C(K, ℝ))
(V : C(K, E) →L[ℝ] C(K, E))
:
ContDiff ℝ (↑⊤) (amnrCurveResidual f ⋯ η V)
The actual residual is smooth on trajectories from local field smoothness.
theorem
AVenhance.Infra.Section4.amnrCurveResidual_hasFDerivAt_local
{K E : Type}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{f : ℝ × E → E}
(hf : ContDiff ℝ (↑⊤) f)
(η : C(K, ℝ))
(V : C(K, E) →L[ℝ] C(K, E))
(u : C(K, E))
:
HasFDerivAt (amnrCurveResidual f ⋯ η V) (1 - amnrCurveJacobianCoefficient f hf η V u) u
The actual residual derivative follows from the local substitution rule.
theorem
AVenhance.Infra.Section4.amnrCurveResidual_solution_contDiffAt_local
{K E P : Type}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[CompleteSpace E]
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{f : ℝ × E → E}
(hf : ContDiff ℝ (↑⊤) f)
(η : C(K, ℝ))
(V : C(K, E) →L[ℝ] C(K, E))
{Q R : P → C(K, E)}
{x : P}
(hQ : ContinuousAt Q x)
(hR : ContDiffAt ℝ (↑⊤) R x)
(heq : ∀ (y : P), amnrCurveResidual f ⋯ η V (Q y) = R y)
(hsmall : ‖amnrCurveJacobianCoefficient f hf η V (Q x)‖ < 1)
:
ContDiffAt ℝ (↑⊤) Q x
A continuous family solving the actual integral equation is smooth whenever the actual linearized Volterra operator is small at the reference curve. This is a local calculus criterion, not a flow regularity assumption.
theorem
AVenhance.Infra.Section4.amnrCurveJacobianCoefficient_norm_le_along
{K E : Type}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : ℝ × E → E}
(hf : ContDiff ℝ (↑⊤) f)
(η : C(K, ℝ))
(V : C(K, E) →L[ℝ] C(K, E))
(u : C(K, E))
{M : ℝ}
(hM : 0 ≤ M)
(hstate : ∀ (t : K), ‖amnrStateDerivative f (η t, u t)‖ ≤ M)
:
Primitive Jacobian bounds along a single actual reference trajectory control the local linearized Volterra operator.