Joint first-order regularity of a smooth nonautonomous flow.

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

Spatial Fréchet derivative of the flow at a joint time-space-start-time point.

Equations

• AVenhance.Infra.Flow.JointC1.flowSpatialDerivativeAt X p = fderiv ℝ (fun (y : Homogenization.Vec 2) => X p.1 y p.2.2) p.2.1

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

Starting-time velocity given by minus the transported initial vector field.

Equations

• AVenhance.Infra.Flow.JointC1.flowStartVelocity b X p = -(AVenhance.Infra.Flow.JointC1.flowSpatialDerivativeAt X p) (b p.2.2 p.2.1)

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

Starting-time differential as a continuous linear map from real times.

Equations

• AVenhance.Infra.Flow.JointC1.flowStartDerivativeCLM b X p = ContinuousLinearMap.toSpanSingleton ℝ (AVenhance.Infra.Flow.JointC1.flowStartVelocity b X p)

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

Differential in the initial position and starting time with observation time fixed.

Equations

• AVenhance.Infra.Flow.JointC1.flowPairDerivativeAt b X p = (AVenhance.Infra.Flow.JointC1.flowSpatialDerivativeAt X p).coprod (AVenhance.Infra.Flow.JointC1.flowStartDerivativeCLM b X p)

def AVenhance.Infra.Flow.JointC1.flowTimeVelocity (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (p : ℝ × Homogenization.Vec 2 × ℝ) : Homogenization.Vec 2

Vector field evaluated at the endpoint of the flow.

Equations

• AVenhance.Infra.Flow.JointC1.flowTimeVelocity b X p = b p.1 (X p.1 p.2.1 p.2.2)

def AVenhance.Infra.Flow.JointC1.flowTimeDerivativeAt (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (p : ℝ × Homogenization.Vec 2 × ℝ) : ℝ →L[ℝ] Homogenization.Vec 2

Observation-time differential as a continuous linear map from real times.

Equations

• AVenhance.Infra.Flow.JointC1.flowTimeDerivativeAt b X p = ContinuousLinearMap.toSpanSingleton ℝ (AVenhance.Infra.Flow.JointC1.flowTimeVelocity b X p)

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

Joint differential assembled from observation-time, spatial, and starting-time parts.

Equations

• AVenhance.Infra.Flow.JointC1.flowJointDerivativeAt b X p = (AVenhance.Infra.Flow.JointC1.flowTimeDerivativeAt b X p).coprod (AVenhance.Infra.Flow.JointC1.flowPairDerivativeAt b X p)

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

Explicit joint differential formula for the three arguments of the flow.

Equations

• AVenhance.Infra.Flow.flowJointDerivativeFormula b X p = AVenhance.Infra.Flow.JointC1.flowJointDerivativeAt b X p

theorem AVenhance.Infra.Flow.JointC1.flowStartDerivativeCLM_continuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : Continuous (flowStartDerivativeCLM b X)

theorem AVenhance.Infra.Flow.JointC1.flowPairDerivativeAt_continuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : Continuous (flowPairDerivativeAt b X)

theorem AVenhance.Infra.Flow.JointC1.flowTimeDerivativeAt_continuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : Continuous (flowTimeDerivativeAt b X)

theorem AVenhance.Infra.Flow.JointC1.flow_fixedTarget_pair_hasStrictFDerivAt {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (t : ℝ) (x : Homogenization.Vec 2) (s : ℝ) : HasStrictFDerivAt (fun (q : Homogenization.Vec 2 × ℝ) => X t q.1 q.2) ((flowSpatialDerivativeAt X (t, x, s)).coprod (flowStartDerivativeCLM b X (t, x, s))) (x, s)

theorem AVenhance.Infra.Flow.flow_joint_hasFDerivAt {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 × ℝ) : HasFDerivAt (fun (q : ℝ × Homogenization.Vec 2 × ℝ) => X q.1 q.2.1 q.2.2) (JointC1.flowJointDerivativeAt b X p) p

The full time, position, and initial-time map of a smooth periodic flow is continuously Fréchet differentiable. Its partial derivatives are the vector field and the jointly continuous spatial/start-time derivative.

theorem AVenhance.Infra.Flow.flow_joint_hasFDerivAt_explicit {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 × ℝ) : HasFDerivAt (fun (q : ℝ × Homogenization.Vec 2 × ℝ) => X q.1 q.2.1 q.2.2) (flowJointDerivativeFormula b X p) p

Explicit form of the total derivative of the joint flow map, with the spatial and start-time components exposed for higher regularity bootstraps.

theorem AVenhance.Infra.Flow.flow_joint_contDiff_one {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 × ℝ) => X p.1 p.2.1 p.2.2

Joint C¹ regularity of a smooth periodic nonautonomous flow.

theorem AVenhance.Infra.Flow.flow_inverse_joint_contDiff_one {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 × ℝ) => X p.2.2 p.2.1 p.1

The inverse flow map is jointly C¹ in target time, point, and initial time; its spatial slice is the inverse of the forward flow map.