The third variational affine system along a smooth flow.

def AVenhance.Infra.Flow.Existence.spatialDirections3 (h k l : Homogenization.Vec 2) : Fin 3 → ℝ × Homogenization.Vec 2

Three spatial directions embedded into the joint time-space domain.

Equations

• AVenhance.Infra.Flow.Existence.spatialDirections3 h k l i = if i = 0 then (0, h) else if i = 1 then (0, k) else (0, l)

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

Two spatial directions embedded into the joint time-space domain.

Equations

• AVenhance.Infra.Flow.Existence.spatialDirections2 h k i = Fin.cases (0, h) (fun (x : Fin 1) => (0, k)) i

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

The third derivative of the vector field evaluated in spatial directions.

Equations

• AVenhance.Infra.Flow.spatialThirdDerivativeEval b t x h k l = (iteratedFDeriv ℝ 3 (Function.uncurry b) (t, x)) (AVenhance.Infra.Flow.Existence.spatialDirections3 h k l)

def AVenhance.Infra.Flow.Existence.spatialDirections3Vec (h k l : Homogenization.Vec 2) : Fin 3 → Homogenization.Vec 2

Ordered triple of spatial directions for a third derivative evaluation.

Equations

• AVenhance.Infra.Flow.Existence.spatialDirections3Vec h k l i = if i = 0 then h else if i = 1 then k else l

theorem AVenhance.Infra.Flow.spatialThirdDerivativeEval_eq_slice {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (t : ℝ) (x h k l : Homogenization.Vec 2) : spatialThirdDerivativeEval b t x h k l = (iteratedFDeriv ℝ 3 (fun (y : Homogenization.Vec 2) => b t y) x) (Existence.spatialDirections3Vec h k l)

theorem AVenhance.Infra.Flow.spatialThirdDerivativeEval_add_left {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (t : ℝ) (x h₁ h₂ k l : Homogenization.Vec 2) : spatialThirdDerivativeEval b t x (h₁ + h₂) k l = spatialThirdDerivativeEval b t x h₁ k l + spatialThirdDerivativeEval b t x h₂ k l

theorem AVenhance.Infra.Flow.spatialThirdDerivativeEval_add_middle {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (t : ℝ) (x h k₁ k₂ l : Homogenization.Vec 2) : spatialThirdDerivativeEval b t x h (k₁ + k₂) l = spatialThirdDerivativeEval b t x h k₁ l + spatialThirdDerivativeEval b t x h k₂ l

theorem AVenhance.Infra.Flow.spatialThirdDerivativeEval_add_right {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (t : ℝ) (x h k l₁ l₂ : Homogenization.Vec 2) : spatialThirdDerivativeEval b t x h k (l₁ + l₂) = spatialThirdDerivativeEval b t x h k l₁ + spatialThirdDerivativeEval b t x h k l₂

theorem AVenhance.Infra.Flow.spatialThirdDerivativeEval_smul_left {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (t : ℝ) (x : Homogenization.Vec 2) (c : ℝ) (h k l : Homogenization.Vec 2) : spatialThirdDerivativeEval b t x (c • h) k l = c • spatialThirdDerivativeEval b t x h k l

theorem AVenhance.Infra.Flow.spatialThirdDerivativeEval_smul_middle {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (t : ℝ) (x : Homogenization.Vec 2) (c : ℝ) (h k l : Homogenization.Vec 2) : spatialThirdDerivativeEval b t x h (c • k) l = c • spatialThirdDerivativeEval b t x h k l

theorem AVenhance.Infra.Flow.spatialThirdDerivativeEval_smul_right {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (t : ℝ) (x : Homogenization.Vec 2) (c : ℝ) (h k l : Homogenization.Vec 2) : spatialThirdDerivativeEval b t x h k (c • l) = c • spatialThirdDerivativeEval b t x h k l

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

Periodicity gives a uniform trilinear bound for the third spatial derivative of the field.

theorem AVenhance.Infra.Flow.exists_global_spatialThirdDerivativeEval_lipschitz {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (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‖

The third spatial derivative evaluation is globally Lipschitz in its base point, with a constant uniform in time and the three directions.

theorem AVenhance.Infra.Flow.Existence.continuous_spatialSecondDerivativeEval_along {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 : ℝ) (u v : ℝ → Homogenization.Vec 2) (hu : Continuous u) (hv : Continuous v) : Continuous fun (q : ℝ) => spatialSecondDerivativeEval b q (X q x s) (u q) (v q)

theorem AVenhance.Infra.Flow.existsUnique_flow_thirdVariationCandidate {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 l : 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 + spatialThirdDerivativeEval b t (X t x s) (V t h s) (V t k s) (V t l s) + spatialSecondDerivativeEval b t (X t x s) (flowSecondVariation hb hX x s hV h k t 0 s) (V t l s) + spatialSecondDerivativeEval b t (X t x s) (flowSecondVariation hb hX x s hV h l t 0 s) (V t k s) + spatialSecondDerivativeEval b t (X t x s) (flowSecondVariation hb hX x s hV k l t 0 s) (V t h s)) W

The third variational equation has a unique global solution. Its forcing is the sum of the third field derivative on three first variations and the three second-derivative/second-variation terms.

noncomputable def AVenhance.Infra.Flow.flowThirdVariation {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 l : Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2

The selected global third variational flow.

Equations

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

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

The selected third variation solves its defining affine system.