Uniform base-point continuity estimates for the third variation.

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

theorem AVenhance.Infra.Flow.ThirdVariationContinuity.thirdCont_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.

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

The uniform base-point Lipschitz constant for the third variation on a forward compact target-time interval.

Equations

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

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

The third variational flow is Lipschitz in its initial point, uniformly over a forward compact target-time interval and all three directions.

theorem AVenhance.Infra.Flow.flow_thirdVariation_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 k l : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => flowThirdVariation hb hX p.2 s ⋯ h k l p.1 0 s) (Set.Icc s t ×ˢ Set.univ)

On a forward compact target-time interval, a fixed third spatial variation is jointly continuous in target time and initial point.