The linear variational equation along a characterized flow trajectory.

noncomputable def AVenhance.Infra.Flow.jointSpatialFDeriv (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

The spatial derivative of b written as the restriction of the joint time-space derivative to the spatial factor.

Equations

• AVenhance.Infra.Flow.jointSpatialFDeriv b t x = fderiv ℝ (Function.uncurry b) (t, x) ∘SL ContinuousLinearMap.inr ℝ ℝ (Homogenization.Vec 2)

theorem AVenhance.Infra.Flow.jointSpatialFDeriv_eq_slice {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (t : ℝ) (x : Homogenization.Vec 2) : jointSpatialFDeriv b t x = fderiv ℝ (fun (y : Homogenization.Vec 2) => b t y) x

The joint derivative restricted to the spatial factor is the derivative of the fixed-time spatial slice.

theorem AVenhance.Infra.Flow.jointSpatialFDeriv_continuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : Continuous fun (p : ℝ × Homogenization.Vec 2) => jointSpatialFDeriv b p.1 p.2

The joint spatial derivative varies continuously in its time and space arguments.

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

The joint spatial derivative is globally bounded for a smooth periodic field.

noncomputable def AVenhance.Infra.Flow.linearizedFieldAlongFlow (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (x : Homogenization.Vec 2) (s : ℝ) : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2

The coefficient field of the variational equation along a fixed characterized trajectory.

Equations

• AVenhance.Infra.Flow.linearizedFieldAlongFlow b X x s t v = (AVenhance.Infra.Flow.jointSpatialFDeriv b t (X t x s)) v

theorem AVenhance.Infra.Flow.linearizedFieldAlongFlow_continuous {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 : ℝ) : Continuous fun (t : ℝ) => jointSpatialFDeriv b t (X t x s)

The variational coefficient along a fixed flow trajectory is continuous.

theorem AVenhance.Infra.Flow.existsUnique_linearSystemFlow (A : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (hA : Continuous A) (M : ℝ) (hM : ∀ (t : ℝ), ‖A t‖ ≤ M) : ∃! V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2, IsFlow (fun (t : ℝ) (v : Homogenization.Vec 2) => (A t) v) V

A bounded continuous family of linear vector fields has a globally characterized flow.

theorem AVenhance.Infra.Flow.linearSystemFlow_zero (A : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (M : ℝ) (hLip : ∀ (t : ℝ) (u v : Homogenization.Vec 2), ‖(A t) u - (A t) v‖ ≤ M * ‖u - v‖) {V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hV : IsFlow (fun (t : ℝ) (v : Homogenization.Vec 2) => (A t) v) V) (s t : ℝ) : V t 0 s = 0

A vector solution of a homogeneous linear system vanishing initially is identically zero.

theorem AVenhance.Infra.Flow.VariationalEquation.linearSystemFlow_add_smul (A : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (M : ℝ) (hLip : ∀ (t : ℝ) (u v : Homogenization.Vec 2), ‖(A t) u - (A t) v‖ ≤ M * ‖u - v‖) {V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hV : IsFlow (fun (t : ℝ) (v : Homogenization.Vec 2) => (A t) v) V) (s : ℝ) : (∀ (t : ℝ) (v w : Homogenization.Vec 2), V t (v + w) s = V t v s + V t w s) ∧ ∀ (t c : ℝ) (v : Homogenization.Vec 2), V t (c • v) s = c • V t v s

Solutions of the linear variational equation depend linearly on their initial direction.

theorem AVenhance.Infra.Flow.exists_flow_variationalContinuousLinearMap (A : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (M : ℝ) (hM : ∀ (t : ℝ), ‖A t‖ ≤ M) {V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hV : IsFlow (fun (t : ℝ) (v : Homogenization.Vec 2) => (A t) v) V) (t s : ℝ) : ∃ (J : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2), ∀ (v : Homogenization.Vec 2), J v = V t v s

At each time, the variational solution in its initial vector is a continuous linear map.

theorem AVenhance.Infra.Flow.existsUnique_flow_variationalEquation {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 : ℝ) : ∃! V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2, IsFlow (linearizedFieldAlongFlow b X x s) V

Existence and uniqueness of the vector-valued variational solution along any characterized flow of a smooth periodic field.