Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.Amnr.CurveJacobian

The actual linearized Volterra operator and its primitive jets.

source
@[instance_reducible]
noncomputable instance AVenhance.Infra.Section4.CurveJacobian.amnrCurveEndNorm {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] :
NormedAddCommGroup (C(K, E) →L[ℝ] C(K, E))
Equations
source
@[instance_reducible]
noncomputable instance AVenhance.Infra.Section4.CurveJacobian.amnrCurveEndSpace {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] :
NormedSpace ℝ (C(K, E) →L[ℝ] C(K, E))
Equations
source
@[instance_reducible]
noncomputable instance AVenhance.Infra.Section4.CurveJacobian.amnrOperatorCurveNorm {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] :
NormedAddCommGroup C(K, E →L[ℝ] E)
Equations
source
@[instance_reducible]
noncomputable instance AVenhance.Infra.Section4.CurveJacobian.amnrOperatorCurveSpace {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] :
NormedSpace ℝ C(K, E →L[ℝ] E)
Equations
source
noncomputable def AVenhance.Infra.Section4.amnrCurveJacobianCoefficient {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)) :
C(K, E) →L[ℝ] C(K, E)

The linearized Volterra coefficient at an actual continuous trajectory.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AVenhance.Infra.Section4.amnrCurveJacobian_lift_norm_le {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (V : C(K, E) →L[ℝ] C(K, E)) :
    ‖(ContinuousLinearMap.compL ℝ C(K, E) C(K, E) C(K, E)) V ∘SL amnrCurveOperatorMap‖ ≤ ‖V‖

    Lifting an operator curve and composing with time integration is linear with norm at most the integration norm.

    source
    theorem AVenhance.Infra.Section4.amnrCurveJacobianCoefficient_contDiff {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 ℝ (↑⊤) (amnrCurveJacobianCoefficient f hf η V)

    Primitive joint derivative bounds prove smoothness of the linearized coefficient, including when its state is an actual flow curve.

    source
    theorem AVenhance.Infra.Section4.amnrCurveJacobianCoefficient_iteratedFDeriv_norm_le {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)) (n : ℕ) (u : C(K, E)) {B : ℝ} (hB : 0 ≤ B) (hstate : ∀ (t : K) (x : E), ‖iteratedFDeriv ℝ n (fun (y : E) => amnrStateDerivative f (η t, y)) x‖ ≤ B) :
    ‖iteratedFDeriv ℝ n (amnrCurveJacobianCoefficient f hf η V) u‖ ≤ ‖V‖ * B

    Every coefficient jet has only the time-integration norm as additional cost, beyond the actual primitive state-Jacobian jet.

    source
    theorem AVenhance.Infra.Section4.amnrCurveResidual_solution_jacobian_equation {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)) {Q : E → C(K, E)} (hQ : ContDiff ℝ (↑⊤) Q) (heq : ∀ (y : E), amnrCurveResidual f ⋯ η V (Q y) = ContinuousMap.const K y) (x : E) :
    fderiv ℝ Q x = ContinuousLinearMap.const ℝ K + amnrCurveJacobianCoefficient f hf η V (Q x) ∘SL fderiv ℝ Q x

    Differentiating the actual Volterra equation yields the Jacobian fixed equation. Its highest derivative is derived, never imposed as a premise.