Uniform-in-time comparison estimates for first spatial variations.

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

theorem AVenhance.Infra.Flow.SecondSpatial.linearFlow_norm_bound_on_Ico (A : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (M : ℝ) (hM : 0 ≤ M) (hA : ∀ (r : ℝ), ‖A r‖ ≤ M) {V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hV : IsFlow (fun (r : ℝ) (v : Homogenization.Vec 2) => (A r) v) V) (s t : ℝ) (_hst : s ≤ t) (v : Homogenization.Vec 2) (r : ℝ) : r ∈ Set.Ico s t → ‖V r v s‖ ≤ Real.exp (M * (t - s)) * ‖v‖

A homogeneous linear flow with operator norm at most M grows by at most exp (M * (t-s)) on a forward interval.

theorem AVenhance.Infra.Flow.exists_flow_variational_difference_bound_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) (L M C : ℝ) (hL₀ : 0 ≤ L) (hM₀ : 0 ≤ M) (hC₀ : 0 ≤ C) (hL : ∀ (q : ℝ) (u w : Homogenization.Vec 2), ‖b q u - b q w‖ ≤ L * ‖u - w‖) (hM : ∀ (q : ℝ) (z : Homogenization.Vec 2), ‖jointSpatialFDeriv b q z‖ ≤ M) (hC : ∀ (q : ℝ) (z w : Homogenization.Vec 2), ‖jointSpatialFDeriv b q z - jointSpatialFDeriv b q w‖ ≤ C * ‖z - w‖) (x y : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) : ∃ (Vx : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2), IsFlow (linearizedFieldAlongFlow b X x s) Vx ∧ ∃ (Vy : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2), IsFlow (linearizedFieldAlongFlow b X y s) Vy ∧ ∃ (K : ℝ), 0 ≤ K ∧ K = gronwallBound 0 M (C * Real.exp (L * (t - s)) * Real.exp (M * (t - s))) (t - s) ∧ ∀ r ∈ Set.Icc s t, ∀ (v : Homogenization.Vec 2), ‖Vy r v s - Vx r v s‖ ≤ K * ‖x - y‖ * ‖v‖

On a forward interval, the first variational solutions at two starting points differ by at most a constant times the starting-point distance and the initial direction norm. The constant is uniform in target time.

theorem AVenhance.Infra.Flow.exists_flow_second_spatial_derivative_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), IsFlow (linearizedFieldAlongFlow b X x s) V ∧ ∃ (B : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2), (∀ (h k : Homogenization.Vec 2), (B h) k = flowSecondVariation hb hX x s ⋯ h k t 0 s) ∧ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (h k : Homogenization.Vec 2), ‖(fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) (x + h)) k - (fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x) k - (B h) k‖ ≤ C * ‖h‖ * ‖h‖ * ‖k‖ ∧ ∀ q ∈ Set.Icc s t, ‖Classical.choose ⋯ q k s - V q k s - flowSecondVariation hb hX x s ⋯ h k q 0 s‖ ≤ C * ‖h‖ * ‖h‖ * ‖k‖

The spatial derivative of the flow has a quadratic Taylor remainder whose linear term is the continuous bilinear second variation.

theorem AVenhance.Infra.Flow.exists_flow_spatialFDeriv_hasFDerivAt_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), IsFlow (linearizedFieldAlongFlow b X x s) V ∧ ∃ (B : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2), (∀ (h k : Homogenization.Vec 2), (B h) k = flowSecondVariation hb hX x s ⋯ h k t 0 s) ∧ HasFDerivAt (fun (y : Homogenization.Vec 2) => fderiv ℝ (fun (z : Homogenization.Vec 2) => X t z s) y) B x

The first spatial derivative of a forward flow map is differentiable, and its derivative is the continuous bilinear second variation.

theorem AVenhance.Infra.Flow.flow_variational_direction_jointContinuous_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (h : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => (fderiv ℝ (fun (z : Homogenization.Vec 2) => X p.1 z s) p.2) h) (Set.Icc s t ×ˢ Set.univ)

On a forward compact time interval, each spatial direction of the first variation is jointly continuous in target time and base point.

theorem AVenhance.Infra.Flow.exists_global_spatialSecondDerivativeEval_lipschitz {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ) (x y h k : Homogenization.Vec 2), ‖spatialSecondDerivativeEval b t x h k - spatialSecondDerivativeEval b t y h k‖ ≤ C * ‖x - y‖ * ‖h‖ * ‖k‖

The second spatial derivative of the field is globally Lipschitz in its base point, with a constant uniform in time and both directions.

noncomputable def AVenhance.Infra.Flow.flowSecondVariationLipschitzConstant (L M Cjac C₂ C₃ s t : ℝ) : ℝ

The second variational flow depends Lipschitz continuously on the base point, uniformly over a forward time interval.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Flow.exists_flow_secondVariation_lipschitz_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) (L M Cjac C₂ C₃ : ℝ) (hL₀ : 0 ≤ L) (hM₀ : 0 ≤ M) (hCjac₀ : 0 ≤ Cjac) (hC₂₀ : 0 ≤ C₂) (hC₃₀ : 0 ≤ C₃) (hL : ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) (hM : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖jointSpatialFDeriv b t x‖ ≤ M) (hCjac : ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖jointSpatialFDeriv b t x - jointSpatialFDeriv b t y‖ ≤ Cjac * ‖x - y‖) (hC₂ : ∀ (t : ℝ) (x h k : Homogenization.Vec 2), ‖spatialSecondDerivativeEval b t x h k‖ ≤ C₂ * ‖h‖ * ‖k‖) (hC₃ : ∀ (t : ℝ) (x y h k : Homogenization.Vec 2), ‖spatialSecondDerivativeEval b t x h k - spatialSecondDerivativeEval b t y h k‖ ≤ C₃ * ‖x - y‖ * ‖h‖ * ‖k‖) (x y : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) (h k : Homogenization.Vec 2) : ∃ (C : ℝ), 0 ≤ C ∧ C = flowSecondVariationLipschitzConstant L M Cjac C₂ C₃ s t ∧ ∀ q ∈ Set.Icc s t, ‖flowSecondVariation hb hX y s ⋯ h k q 0 s - flowSecondVariation hb hX x s ⋯ h k q 0 s‖ ≤ C * ‖x - y‖ * ‖h‖ * ‖k‖