Joint C¹ regularity of the variational flow on forward regions.

@[instance_reducible]

def AVenhance.Infra.Flow.avInfraFlowVariationalJointC1NormedAddCommGroup1 : NormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ)

Equip the spatial matrix space with its coordinate supremum norm.

Equations

• AVenhance.Infra.Flow.avInfraFlowVariationalJointC1NormedAddCommGroup1 = Matrix.normedAddCommGroup

@[instance_reducible]

noncomputable def AVenhance.Infra.Flow.avInfraFlowVariationalJointC1NormedSpace2 : NormedSpace ℝ (Matrix (Fin 2) (Fin 2) ℝ)

Real normed-space structure for spatial matrices with the coordinate supremum norm.

Equations

• AVenhance.Infra.Flow.avInfraFlowVariationalJointC1NormedSpace2 = Matrix.normedSpace

noncomputable def AVenhance.Infra.Flow.VariationalJointC1.jacobianMatrixBasis : Module.Basis (Fin 2) ℝ (Homogenization.Vec 2)

Coordinate basis used to represent the variational Jacobian by a matrix.

Equations

• AVenhance.Infra.Flow.VariationalJointC1.jacobianMatrixBasis = Pi.basisFun ℝ (Fin 2)

noncomputable def AVenhance.Infra.Flow.VariationalJointC1.jacobianMatrixToCLM : Matrix (Fin 2) (Fin 2) ℝ ≃L[ℝ] Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

Continuous linear equivalence from Jacobian matrices to spatial endomorphisms.

Equations

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

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_apply_hasDerivAt {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 : ℝ) (v : Homogenization.Vec 2) : HasDerivAt (fun (r : ℝ) => (fderiv ℝ (fun (z : Homogenization.Vec 2) => X r z s) x) v) ((jointSpatialFDeriv b t (X t x s)) ((fderiv ℝ (fun (z : Homogenization.Vec 2) => X t z s) x) v)) t

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_target_hasDerivAt {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 : ℝ) : HasDerivAt (fun (r : ℝ) => fderiv ℝ (fun (z : Homogenization.Vec 2) => X r z s) x) (jointSpatialFDeriv b t (X t x s) ∘SL fderiv ℝ (fun (z : Homogenization.Vec 2) => X t z s) x) t

On a compact forward target-time interval, the Fréchet derivative of the spatial Jacobian in target time is the variational equation in operator form.

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_contDiffOn_one_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s T : ℝ) (hst : s < T) : ContDiffOn ℝ 1 (fun (p : ℝ × Homogenization.Vec 2) => fderiv ℝ (fun (y : Homogenization.Vec 2) => X p.1 y s) p.2) (Set.Ioo s T ×ˢ Set.univ)

The spatial Jacobian is jointly C¹ in target time and initial point on a forward open strip with fixed initial time.

noncomputable def AVenhance.Infra.Flow.VariationalJointC1.flowFixedStartDerivativeAt (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (s : ℝ) (q : ℝ × Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

Joint time-space differential of the flow with its starting time fixed.

Equations

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

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_contDiff_one {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s : ℝ) : ContDiff ℝ 1 fun (p : ℝ × Homogenization.Vec 2) => fderiv ℝ (fun (y : Homogenization.Vec 2) => X p.1 y s) p.2

For a fixed start time, the spatial Jacobian is jointly C¹ across both target-time orientations.