Encode target-time variation as an actual constant state parameter.

def AVenhance.Infra.Section4.amnrTimeParameterizedField (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (s d α : ℝ) (z : ℝ × ℝ × Homogenization.Vec 2) : ℝ × Homogenization.Vec 2

The actual field for an ODE on a fixed unit time interval. Its first state coordinate stays constant and determines the actual target time.

Equations

• AVenhance.Infra.Section4.amnrTimeParameterizedField b s d α z = (0, (d + α * z.2.1) • b (s + z.1 * (d + α * z.2.1)) z.2.2)

theorem AVenhance.Infra.Section4.amnrTimeParameterizedField_contDiff {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (s d α : ℝ) : ContDiff ℝ (↑⊤) (amnrTimeParameterizedField b s d α)

The augmented primitive field is smooth by ordinary joint composition.

theorem AVenhance.Infra.Section4.amnrTimeParameterizedField_stateDerivative_apply {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (s d α τ : ℝ) (x : Homogenization.Vec 2) (h : ℝ × Homogenization.Vec 2) : (amnrStateDerivative (amnrTimeParameterizedField b s d α) (τ, 0, x)) h = (0, (α * h.1) • b (s + τ * d) x + d • (fderiv ℝ (Function.uncurry b) (s + τ * d, x)) (τ * (α * h.1), h.2))

The actual state derivative at zero parameter is an explicit operator with the small time-interval Jacobian on its spatial diagonal.

theorem AVenhance.Infra.Section4.amnrTimeParameterizedField_stateDerivative_norm_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (s d α τ : ℝ) (x : Homogenization.Vec 2) {B₀ B₁ M : ℝ} (hB₀ : 0 ≤ B₀) (hB₁ : 0 ≤ B₁) (hM : 0 ≤ M) (hvel : ‖b (s + τ * d) x‖ ≤ B₀) (hjoint : ‖fderiv ℝ (Function.uncurry b) (s + τ * d, x)‖ ≤ B₁) (hstate : ‖Flow.jointSpatialFDeriv b (s + τ * d) x‖ ≤ M) (hτ : |τ| ≤ 1) : ‖amnrStateDerivative (amnrTimeParameterizedField b s d α) (τ, 0, x)‖ ≤ |d| * M + |α| * (B₀ + |d| * B₁)

Actual primitive bounds make the augmented state Jacobian small. The parameter column can be made small by choosing its scale α.