Joint continuity in target time and base point of the spatial derivative.

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

Coordinate basis used to identify matrices with spatial linear maps.

Equations

• AVenhance.Infra.Flow.JointSpatialDerivative.flowSpatialBasis = Pi.basisFun ℝ (Fin 2)

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

Continuous linear equivalence between two-by-two matrices and spatial endomorphisms.

Equations

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

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_jointContinuousOn_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) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => fderiv ℝ (fun (z : Homogenization.Vec 2) => X p.1 z s) p.2) (Set.Icc s t ×ˢ Set.univ)

On a forward compact target-time interval, the spatial derivative depends jointly continuously on target time and base point, for fixed initial time.