Joint C² regularity of the nonautonomous flow.

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

Spatial Jacobian used in the joint C² bootstrap.

Equations

• AVenhance.Infra.Flow.JointC2All.flowJacobianC1 X p = AVenhance.Infra.Flow.JointC1.flowSpatialDerivativeAt X p

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

Observation-time velocity used in the joint C² bootstrap.

Equations

• AVenhance.Infra.Flow.JointC2All.flowTimeVelocityC1 b X p = AVenhance.Infra.Flow.JointC1.flowTimeVelocity b X p

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

Starting-time velocity used in the joint C² bootstrap.

Equations

• AVenhance.Infra.Flow.JointC2All.flowStartVelocityC1 b X p = AVenhance.Infra.Flow.JointC1.flowStartVelocity b X p

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

Continuous linear starting-time differential used in the joint C² bootstrap.

Equations

• AVenhance.Infra.Flow.JointC2All.flowStartCLMC1 b X p = AVenhance.Infra.Flow.JointC1.flowStartDerivativeCLM b X p

noncomputable def AVenhance.Infra.Flow.JointC2All.flowParameterDerivativeC1 (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

Position and starting-time differential used in the joint C² bootstrap.

Equations

• AVenhance.Infra.Flow.JointC2All.flowParameterDerivativeC1 b X p = AVenhance.Infra.Flow.JointC1.flowPairDerivativeAt b X p

noncomputable def AVenhance.Infra.Flow.JointC2All.flowJointDerivativeC1 (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

Full joint differential used in the joint C² bootstrap.

Equations

• AVenhance.Infra.Flow.JointC2All.flowJointDerivativeC1 b X p = AVenhance.Infra.Flow.JointC1.flowJointDerivativeAt b X p

theorem AVenhance.Infra.Flow.JointC2All.flowJacobianC1_contDiff {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : ContDiff ℝ 1 (flowJacobianC1 X)

theorem AVenhance.Infra.Flow.JointC2All.flowTimeVelocityC1_contDiff {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : ContDiff ℝ 1 (flowTimeVelocityC1 b X)

theorem AVenhance.Infra.Flow.JointC2All.flowStartCLMC1_contDiff {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : ContDiff ℝ 1 (flowStartCLMC1 b X)

theorem AVenhance.Infra.Flow.JointC2All.flowParameterDerivativeC1_contDiff {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : ContDiff ℝ 1 (flowParameterDerivativeC1 b X)

theorem AVenhance.Infra.Flow.JointC2All.flowJointDerivativeC1_contDiff {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : ContDiff ℝ 1 (flowJointDerivativeC1 b X)

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

Joint C² regularity of the smooth flow in target time, initial point, and start time.