Preparatory ODE systems for higher spatial variations of a smooth flow.

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

def AVenhance.Infra.Flow.HigherVariation.spatialDirections (h k : Homogenization.Vec 2) : Fin 2 → ℝ × Homogenization.Vec 2

The pair of spatial directions, embedded into the joint time-space domain.

Equations

• AVenhance.Infra.Flow.HigherVariation.spatialDirections h k i = if i = 0 then (0, h) else (0, k)

noncomputable def AVenhance.Infra.Flow.spatialSecondDerivativeEval (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x h k : Homogenization.Vec 2) : Homogenization.Vec 2

The second spatial derivative of a joint field, evaluated on spatial directions.

Equations

• AVenhance.Infra.Flow.spatialSecondDerivativeEval b t x h k = (iteratedFDeriv ℝ 2 (Function.uncurry b) (t, x)) (AVenhance.Infra.Flow.HigherVariation.spatialDirections h k)

theorem AVenhance.Infra.Flow.spatialSecondDerivativeEval_eq_joint (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x h k : Homogenization.Vec 2) : spatialSecondDerivativeEval b t x h k = ((fderiv ℝ (fderiv ℝ (Function.uncurry b)) (t, x)) (0, h)) (0, k)

The second spatial derivative evaluation is the iterated derivative of the full time-space field restricted to spatial directions.

theorem AVenhance.Infra.Flow.spatialSecondDerivativeEval_eq_spatialJacobianFDeriv_apply {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (t : ℝ) (x h k : Homogenization.Vec 2) : spatialSecondDerivativeEval b t x h k = (fderiv ℝ (fun (z : Homogenization.Vec 2) => (jointSpatialFDeriv b t z) k) x) h

The second spatial derivative of the field is the base-point derivative of its spatial Jacobian, evaluated on the second direction.

theorem AVenhance.Infra.Flow.spatialSecondDerivativeEval_comm {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (t : ℝ) (x h k : Homogenization.Vec 2) : spatialSecondDerivativeEval b t x h k = spatialSecondDerivativeEval b t x k h

The second spatial derivative evaluation is symmetric in its directions.

theorem AVenhance.Infra.Flow.spatialSecondDerivativeEval_add_left (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x h₁ h₂ k : Homogenization.Vec 2) : spatialSecondDerivativeEval b t x (h₁ + h₂) k = spatialSecondDerivativeEval b t x h₁ k + spatialSecondDerivativeEval b t x h₂ k

The second spatial derivative evaluation is bilinear in its directions.

theorem AVenhance.Infra.Flow.spatialSecondDerivativeEval_add_right (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x h k₁ k₂ : Homogenization.Vec 2) : spatialSecondDerivativeEval b t x h (k₁ + k₂) = spatialSecondDerivativeEval b t x h k₁ + spatialSecondDerivativeEval b t x h k₂

The second spatial derivative evaluation is linear in its second direction.

theorem AVenhance.Infra.Flow.spatialSecondDerivativeEval_smul_left (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t c : ℝ) (x h k : Homogenization.Vec 2) : spatialSecondDerivativeEval b t x (c • h) k = c • spatialSecondDerivativeEval b t x h k

The second spatial derivative evaluation is homogeneous in its first direction.

theorem AVenhance.Infra.Flow.spatialSecondDerivativeEval_smul_right (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t c : ℝ) (x h k : Homogenization.Vec 2) : spatialSecondDerivativeEval b t x h (c • k) = c • spatialSecondDerivativeEval b t x h k

The second spatial derivative evaluation is homogeneous in its second direction.

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

Periodicity gives a uniform bilinear operator bound for the second spatial derivative of the field.

theorem AVenhance.Infra.Flow.existsUnique_forcedLinearSystemFlow (A : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (F : ℝ → Homogenization.Vec 2) (hA : Continuous A) (hF : Continuous F) (M : ℝ) (hM : ∀ (t : ℝ), ‖A t‖ ≤ M) : ∃! W : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2, IsFlow (fun (t : ℝ) (w : Homogenization.Vec 2) => (A t) w + F t) W

A continuous affine linear system with uniformly bounded linear part has a unique global flow.

theorem AVenhance.Infra.Flow.existsUnique_flow_secondVariationCandidate {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 : ℝ) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (h k : Homogenization.Vec 2) : ∃! W : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2, IsFlow (fun (t : ℝ) (w : Homogenization.Vec 2) => (jointSpatialFDeriv b t (X t x s)) w + spatialSecondDerivativeEval b t (X t x s) (V t h s) (V t k s)) W

The second variational equation along a smooth flow has a global solution. Its forcing is the second spatial derivative of the field applied to the two first variational solutions. This constructs the candidate second variation; the identification with the derivative of the first variation is a separate regularity step.

noncomputable def AVenhance.Infra.Flow.flowSecondVariation {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 : ℝ) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (h k : Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2

The selected global flow solving the second variational equation.

Equations

• AVenhance.Infra.Flow.flowSecondVariation hb hX x s hV h k = Classical.choose ⋯

theorem AVenhance.Infra.Flow.flowSecondVariation_isFlow {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 : ℝ) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (h k : Homogenization.Vec 2) : IsFlow (fun (t : ℝ) (w : Homogenization.Vec 2) => (jointSpatialFDeriv b t (X t x s)) w + spatialSecondDerivativeEval b t (X t x s) (V t h s) (V t k s)) (flowSecondVariation hb hX x s hV h k)

The selected second variation solves its defining affine system.

theorem AVenhance.Infra.Flow.HigherVariation.variationalFlow_addDirection {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (x : Homogenization.Vec 2) (s t : ℝ) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (h₁ h₂ : Homogenization.Vec 2) : V t (h₁ + h₂) s = V t h₁ s + V t h₂ s

theorem AVenhance.Infra.Flow.HigherVariation.variationalFlow_smulDirection {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (x : Homogenization.Vec 2) (s t c : ℝ) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (h : Homogenization.Vec 2) : V t (c • h) s = c • V t h s

theorem AVenhance.Infra.Flow.flowSecondVariation_add_left {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 : ℝ) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (h₁ h₂ k : Homogenization.Vec 2) (t : ℝ) : flowSecondVariation hb hX x s hV (h₁ + h₂) k t 0 s = flowSecondVariation hb hX x s hV h₁ k t 0 s + flowSecondVariation hb hX x s hV h₂ k t 0 s

The zero-initial-data second variational solution is additive in its first direction.

theorem AVenhance.Infra.Flow.flowSecondVariation_comm {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 : ℝ) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (h k : Homogenization.Vec 2) (t : ℝ) : flowSecondVariation hb hX x s hV h k t 0 s = flowSecondVariation hb hX x s hV k h t 0 s

The zero-initial-data second variational solution is symmetric in its directions.

theorem AVenhance.Infra.Flow.flowSecondVariation_add_right {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 : ℝ) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (h k₁ k₂ : Homogenization.Vec 2) (t : ℝ) : flowSecondVariation hb hX x s hV h (k₁ + k₂) t 0 s = flowSecondVariation hb hX x s hV h k₁ t 0 s + flowSecondVariation hb hX x s hV h k₂ t 0 s

The zero-initial-data second variational solution is additive in its second direction.

theorem AVenhance.Infra.Flow.flowSecondVariation_smul_left {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 c : ℝ) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (h k : Homogenization.Vec 2) (t : ℝ) : flowSecondVariation hb hX x s hV (c • h) k t 0 s = c • flowSecondVariation hb hX x s hV h k t 0 s

The zero-initial-data second variational solution is homogeneous in its first direction.

theorem AVenhance.Infra.Flow.flowSecondVariation_smul_right {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 c : ℝ) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) (h k : Homogenization.Vec 2) (t : ℝ) : flowSecondVariation hb hX x s hV h (c • k) t 0 s = c • flowSecondVariation hb hX x s hV h k t 0 s

The zero-initial-data second variational solution is homogeneous in its second direction.

theorem AVenhance.Infra.Flow.flowSecondVariation_bound_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) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (h k : Homogenization.Vec 2), ‖flowSecondVariation hb hX x s hV h k t 0 s‖ ≤ K * ‖h‖ * ‖k‖

The second variational solution has a uniform bilinear bound on forward time intervals.

theorem AVenhance.Infra.Flow.flowSecondVariation_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) (M C : ℝ) (hM₀ : 0 ≤ M) (hM : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖jointSpatialFDeriv b t x‖ ≤ M) (hC₀ : 0 ≤ C) (hC : ∀ (t : ℝ) (x h k : Homogenization.Vec 2), ‖spatialSecondDerivativeEval b t x h k‖ ≤ C * ‖h‖ * ‖k‖) {V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (x : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) (hV : IsFlow (linearizedFieldAlongFlow b X x s) V) : ∃ (K : ℝ), 0 ≤ K ∧ K = gronwallBound 0 M (C * Real.exp (M * (t - s)) * Real.exp (M * (t - s))) (t - s) ∧ ∀ r ∈ Set.Icc s t, ∀ (h k : Homogenization.Vec 2), ‖flowSecondVariation hb hX x s hV h k r 0 s‖ ≤ K * ‖h‖ * ‖k‖

The second variation obeys its bilinear growth bound uniformly over every target time in a forward interval.

theorem AVenhance.Infra.Flow.exists_flowSecondVariationContinuousBilinear_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) : ∃ (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 hV h k t 0 s

On a forward interval, the second variational solution is represented by a continuous bilinear map in its two directions.