Spatial differentiability of a characterized smooth periodic flow.

theorem AVenhance.Infra.Flow.SpatialC1.gronwallBound_zero_scale (L a c d : ℝ) : gronwallBound 0 L (c * a) d = c * gronwallBound 0 L a d

theorem AVenhance.Infra.Flow.flow_variational_quadratic_remainder_all_times_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (x : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ r ∈ Set.Icc s t, ∀ (h : Homogenization.Vec 2), ‖X r (x + h) s - X r x s - V r h s‖ ≤ C * ‖h‖ * ‖h‖

The nonlinear trajectory differs from its variational approximation by a quadratic amount in the initial displacement, for forward time.

theorem AVenhance.Infra.Flow.flow_variational_quadratic_remainder_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (x : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (h : Homogenization.Vec 2), ‖X t (x + h) s - X t x s - V t h s‖ ≤ C * ‖h‖ * ‖h‖

The nonlinear trajectory differs from its variational approximation by a quadratic amount at a fixed target time, as a consequence of the uniform forward-interval estimate.

theorem AVenhance.Infra.Flow.exists_flow_hasFDerivAt_spatial_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) : ∃ (V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (J : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2), IsFlow (linearizedFieldAlongFlow b X x s) V ∧ (∀ (v : Homogenization.Vec 2), J v = V t v s) ∧ HasFDerivAt (fun (y : Homogenization.Vec 2) => X t y s) J x

The spatial flow map is Fréchet differentiable at every point for forward time, with derivative given by the variational flow.

def AVenhance.Infra.Flow.SpatialC1.reverseTimeField (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2

Time reversal preserves smooth joint periodicity.

Equations

• AVenhance.Infra.Flow.SpatialC1.reverseTimeField b t x = -b (-t) x

def AVenhance.Infra.Flow.SpatialC1.reverseTimeFlow (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2

Flow with observation and starting times both reversed.

Equations

• AVenhance.Infra.Flow.SpatialC1.reverseTimeFlow X t x s = X (-t) x (-s)

theorem AVenhance.Infra.Flow.SpatialC1.smoothPeriodicField_reverseTime {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : SmoothPeriodicField (reverseTimeField b)

theorem AVenhance.Infra.Flow.SpatialC1.isFlow_reverseTime {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : IsFlow (reverseTimeField b) (reverseTimeFlow X)

theorem AVenhance.Infra.Flow.exists_flow_hasFDerivAt_spatial {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s t : ℝ) : ∃ (V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (J : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2), IsFlow (linearizedFieldAlongFlow b X x s) V ∧ (∀ (v : Homogenization.Vec 2), J v = V t v s) ∧ HasFDerivAt (fun (y : Homogenization.Vec 2) => X t y s) J x

Spatial differentiability holds at arbitrary target and initial times. The derivative is the unique variational flow along the characterized trajectory.