The actual flow solves its target-time-parameterized integral equation.

def AVenhance.Infra.Section4.amnrTimeParameterizedCurve {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s d α : ℝ) (z : ℝ × Homogenization.Vec 2) : C(↑(Set.Icc 0 1), ℝ × Homogenization.Vec 2)

The actual joint state path on the fixed unit interval.

Equations

• AVenhance.Infra.Section4.amnrTimeParameterizedCurve hX s d α z = { toFun := fun (τ : ↑(Set.Icc 0 1)) => (z.1, X (s + ↑τ * (d + α * z.1)) z.2 s), continuous_toFun := ⋯ }

theorem AVenhance.Infra.Section4.amnrTimeParameterizedCurve_continuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s d α : ℝ) : Continuous (amnrTimeParameterizedCurve hX s d α)

Joint continuity of the actual flow yields continuity into the uniform trajectory space before any parameter derivative is asserted.

theorem AVenhance.Infra.Section4.amnrTimeParameterizedCurve_hasDerivAt {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s d α : ℝ) (z : ℝ × Homogenization.Vec 2) (τ : ℝ) : HasDerivAt (fun (r : ℝ) => (z.1, X (s + r * (d + α * z.1)) z.2 s)) (amnrTimeParameterizedField b s d α (τ, z.1, X (s + τ * (d + α * z.1)) z.2 s)) τ

The actual parameterized path satisfies its actual augmented ODE.

theorem AVenhance.Infra.Section4.amnrTimeParameterizedCurve_residual_eq_const {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s d α : ℝ) (z : ℝ × Homogenization.Vec 2) : amnrCurveResidual (amnrTimeParameterizedField b s d α) ⋯ (amnrTimeCurve 0 1) (amnrCurveIntegral amnrTimeParameterizedCurve_residual_eq_const._proof_1 0 ⋯) (amnrTimeParameterizedCurve hX s d α z) = ContinuousMap.const (↑(Set.Icc 0 1)) z

The actual parameterized curve obeys the actual Volterra equation.