Initial-time differentiability for augmented jet flows.

theorem AVenhance.Infra.Flow.JetStartDerivative.hasDerivAt_diagonalIntervalIntegralOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {g : ℝ × ℝ → E} (hg : Continuous g) (a : ℝ) : HasDerivAt (fun (r : ℝ) => ∫ (u : ℝ) in r..a, g (u, r)) (-g (a, a)) a

theorem AVenhance.Infra.Flow.isFlowOn_initialTime_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : ℝ → E → E} {Y : ℝ → E → ℝ → E} (hY : IsFlowOn F Y) (hYcont : Continuous fun (p : ℝ × E × ℝ) => Y p.1 p.2.1 p.2.2) (hFcont : Continuous (Function.uncurry F)) (z : E) (a : ℝ) : HasDerivAt (fun (r : ℝ) => Y a z r) (-F a z) a

A continuous characterized flow has the usual derivative with respect to its initial-time parameter.

theorem AVenhance.Infra.Flow.isFlowOn_startTime_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : ℝ → E → E} {Y : ℝ → E → ℝ → E} (hY : IsFlowOn F Y) (hYcont : Continuous fun (p : ℝ × E × ℝ) => Y p.1 p.2.1 p.2.2) (hFcont : Continuous (Function.uncurry F)) (hYstate : ∀ (s t : ℝ), ContDiff ℝ 1 fun (z : E) => Y t z s) (hgroup : ∀ (z : E) (s r t : ℝ), Y t (Y r z s) r = Y t z s) (z : E) (s t : ℝ) : HasDerivAt (fun (r : ℝ) => Y t z r) (-(fderiv ℝ (fun (w : E) => Y t w s) z) (F s z)) s

Start-time differentiability of a characterized flow with a C¹ spatial state map and the flow composition law.

theorem AVenhance.Infra.Flow.JetStartDerivative.firstJetFlow_continuous_joint {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : Continuous fun (p : ℝ × (Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)) × ℝ) => firstJetFlow X p.1 p.2.1 p.2.2

theorem AVenhance.Infra.Flow.firstJetFlow_initialTime_hasDerivAt {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (z : Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)) (s t : ℝ) : HasDerivAt (fun (r : ℝ) => firstJetFlow X t z r) (-(fderiv ℝ (fun (w : Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)) => firstJetFlow X t w s) z) (firstJetField b s z)) s

The augmented first-jet flow has the standard initial-time derivative, with its smooth augmented vector field.

noncomputable def AVenhance.Infra.Flow.firstJetFlowStateDerivativeAt (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (p : ℝ × (Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)) × ℝ) : Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2) →L[ℝ] Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)

The state derivative of the first-jet flow, written in terms of the spatial Jacobian and Hessian of the base flow.

Equations

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

theorem AVenhance.Infra.Flow.firstJetFlow_state_fderiv_eq {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (p : ℝ × (Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)) × ℝ) : fderiv ℝ (fun (w : Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)) => firstJetFlow X p.1 w p.2.2) p.2.1 = firstJetFlowStateDerivativeAt X p

The first-jet state derivative is the actual spatial Fréchet derivative of the augmented flow.

noncomputable def AVenhance.Infra.Flow.firstJetFlowStateStartDerivativeAt (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (p : ℝ × (Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)) × ℝ) : Homogenization.Vec 2 × (Fin 2 → Homogenization.Vec 2)

The start-time derivative of the augmented flow, using its state derivative and the augmented vector field.

Equations

• AVenhance.Infra.Flow.firstJetFlowStateStartDerivativeAt b X p = -(AVenhance.Infra.Flow.firstJetFlowStateDerivativeAt X p) (AVenhance.Infra.Flow.firstJetField b p.2.2 p.2.1)

noncomputable def AVenhance.Infra.Flow.flowSpatialFDerivApplyStartDerivativeAt (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (v : Homogenization.Vec 2) (p : ℝ × Homogenization.Vec 2 × ℝ) : Homogenization.Vec 2

The initial-time derivative of the spatial Jacobian applied to a fixed direction.

Equations

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

noncomputable def AVenhance.Infra.Flow.flowSpatialFDerivApplySpaceDerivativeAt (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (v : Homogenization.Vec 2) (p : ℝ × Homogenization.Vec 2 × ℝ) : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

The parameter derivative of the spatial Jacobian applied to a direction, when varying the initial point.

Equations

• AVenhance.Infra.Flow.flowSpatialFDerivApplySpaceDerivativeAt X v p = (AVenhance.Infra.Flow.flowSecondSpatialDerivative X p.1 p.2.1 p.2.2).flip v

theorem AVenhance.Infra.Flow.JetStartDerivative.flowSpatialFDerivApplySpaceDerivativeAt_continuous {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) : Continuous fun (p : ℝ × Homogenization.Vec 2 × ℝ) => flowSpatialFDerivApplySpaceDerivativeAt X v p

theorem AVenhance.Infra.Flow.JetStartDerivative.flowSpatialFDerivApplyStartDerivativeAt_continuous {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) : Continuous fun (p : ℝ × Homogenization.Vec 2 × ℝ) => flowSpatialFDerivApplyStartDerivativeAt b X v p

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_apply_initialTime_hasDerivAt {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (v x : Homogenization.Vec 2) (s t : ℝ) : HasDerivAt (fun (r : ℝ) => (fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y r) x) v) (flowSpatialFDerivApplyStartDerivativeAt b X v (t, x, s)) s

Initial-time differentiation of the Jacobian follows by applying the augmented-flow derivative to a direction column.

theorem AVenhance.Infra.Flow.JetStartDerivative.flowSpatialFDerivApply_space_hasFDerivAt {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) (t : ℝ) (x : Homogenization.Vec 2) (s : ℝ) : HasFDerivAt (fun (y : Homogenization.Vec 2) => (fderiv ℝ (fun (z : Homogenization.Vec 2) => X t z s) y) v) (flowSpatialFDerivApplySpaceDerivativeAt X v (t, x, s)) x

theorem AVenhance.Infra.Flow.JetStartDerivative.flowSpatialFDerivApply_space_hasStrictFDerivAt {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) (t : ℝ) (x : Homogenization.Vec 2) (s : ℝ) : HasStrictFDerivAt (fun (y : Homogenization.Vec 2) => (fderiv ℝ (fun (z : Homogenization.Vec 2) => X t z s) y) v) (flowSpatialFDerivApplySpaceDerivativeAt X v (t, x, s)) x

theorem AVenhance.Infra.Flow.JetStartDerivative.flowSpatialFDerivApply_contDiff_start_space {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) (t : ℝ) : ContDiff ℝ 1 fun (q : ℝ × Homogenization.Vec 2) => (fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y q.1) q.2) v

For a fixed target time, each variational direction is jointly C¹ in start time and initial point.

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_apply_contDiff_one_all {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) : ContDiff ℝ 1 fun (p : ℝ × ℝ × Homogenization.Vec 2) => (fderiv ℝ (fun (y : Homogenization.Vec 2) => X p.1 y p.2.1) p.2.2) v

Every fixed-direction value of the spatial Jacobian is jointly C¹ in target time, initial point, and start time.

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

The spatial Jacobian is jointly C¹ in all flow variables.