The characterized flow as an actual compact-time solution curve.

def AVenhance.Infra.Section4.amnrTimeCurve (a b : ℝ) : C(↑(Set.Icc a b), ℝ)

The actual time coordinate on a compact interval.

Equations

• AVenhance.Infra.Section4.amnrTimeCurve a b = { toFun := Subtype.val, continuous_toFun := ⋯ }

def AVenhance.Infra.Section4.amnrFlowCurve {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s a c : ℝ) (x : Homogenization.Vec 2) : C(↑(Set.Icc a c), Homogenization.Vec 2)

The actual characterized flow trajectory, retaining its initial point.

Equations

• AVenhance.Infra.Section4.amnrFlowCurve hX s a c x = { toFun := fun (t : ↑(Set.Icc a c)) => X (↑t) x s, continuous_toFun := ⋯ }

theorem AVenhance.Infra.Section4.amnrFlowCurve_lipschitz {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {L : ℝ} (hL₀ : 0 ≤ L) (hL : ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) {s a c : ℝ} (hs : s ∈ Set.Icc a c) : LipschitzWith (Real.exp (L * (c - a))).toNNReal (amnrFlowCurve hX s a c)

Grönwall gives actual uniform continuity of the solution-curve family with respect to its initial point, before proving any flow derivatives.

theorem AVenhance.Infra.Section4.amnrFlowCurve_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 a c : ℝ} (hac : a ≤ c) (hs : s ∈ Set.Icc a c) (x : Homogenization.Vec 2) : amnrCurveResidual (Function.uncurry b) ⋯ (amnrTimeCurve a c) (amnrCurveIntegral hac s hs) (amnrFlowCurve hX s a c x) = ContinuousMap.const (↑(Set.Icc a c)) x

The actual flow curves solve the actual compact-time integral equation. The clamped extension is used only outside the integration interval.

theorem AVenhance.Infra.Section4.amnrFlowCurve_contDiff_infty_of_short {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {M : ℝ} (hM : 0 ≤ M) (hstate : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b t x‖ ≤ M) {s a c : ℝ} (hac : a ≤ c) (hs : s ∈ Set.Icc a c) (hshort : (c - a) * M < 1) : ContDiff ℝ (↑⊤) (amnrFlowCurve hX s a c)

On a short interval, the actual solution-curve family is smooth in its initial point. The flow equation and Grönwall, rather than a flow regularity premise, discharge the two solution-family inputs.

theorem AVenhance.Infra.Section4.amnr_flow_spatial_contDiff_infty_of_short {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {M : ℝ} (hM : 0 ≤ M) (hstate : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b t x‖ ≤ M) {s a c t : ℝ} (hac : a ≤ c) (hs : s ∈ Set.Icc a c) (ht : t ∈ Set.Icc a c) (hshort : (c - a) * M < 1) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => X t x s

Evaluation of the smooth actual solution curve gives every spatial order of the actual fixed-time flow map on the same short interval.