Global joint C³ regularity by reference-time factorization.

noncomputable def AVenhance.Infra.Flow.JointC3All.flowSpatialJacobianJointC2 (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.JointC3All.flowSpatialJacobianJointC2 X p = AVenhance.Infra.Flow.JointC1.flowSpatialDerivativeAt X p

theorem AVenhance.Infra.Flow.flow_spatialFDeriv_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 (JointC3All.flowSpatialJacobianJointC2 X)

The spatial Jacobian is jointly C² in target time, initial point, and start time. Reference-time factorization reduces the claim locally to a forward strip, where the variational equation gives C² regularity.

def AVenhance.Infra.Flow.JointC3All.flowTimeVelocityC2 (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.JointC3All.flowTimeVelocityC2 b X p = AVenhance.Infra.Flow.JointC1.flowTimeVelocity b X p

noncomputable def AVenhance.Infra.Flow.JointC3All.flowStartVelocityC2 (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.JointC3All.flowStartVelocityC2 b X p = AVenhance.Infra.Flow.JointC1.flowStartVelocity b X p

noncomputable def AVenhance.Infra.Flow.JointC3All.flowStartCLMC2 (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.JointC3All.flowStartCLMC2 b X p = AVenhance.Infra.Flow.JointC1.flowStartDerivativeCLM b X p

noncomputable def AVenhance.Infra.Flow.JointC3All.flowParameterDerivativeC2 (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.JointC3All.flowParameterDerivativeC2 b X p = AVenhance.Infra.Flow.JointC1.flowPairDerivativeAt b X p

noncomputable def AVenhance.Infra.Flow.JointC3All.flowJointDerivativeC2 (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.JointC3All.flowJointDerivativeC2 b X p = AVenhance.Infra.Flow.JointC1.flowJointDerivativeAt b X p

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

Joint C³ regularity of a smooth periodic flow in target time, initial position, and start time.

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

Joint C³ regularity of the inverse flow follows by permuting target and start times.