Actual jointly smooth spatial Jacobians and inverse-flow compositions.

theorem AVenhance.Infra.Section4.amnrStateDerivative_eq_slice {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ × E → F} {t : ℝ} {x : E} (hf : DifferentiableAt ℝ f (t, x)) : amnrStateDerivative f (t, x) = fderiv ℝ (fun (y : E) => f (t, y)) x

Spatial restriction of the actual joint derivative equals the actual fixed-time spatial derivative, whenever the joint function is differentiable.

theorem AVenhance.Infra.Section4.amnr_pulledFlowJacobian_contDiffAt_of_short {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {M : ℝ} (hM : 0 ≤ M) (hstate : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b t x‖ ≤ M) (s t : ℝ) (x : Homogenization.Vec 2) (hshort : |t - s| * M ≤ 1 / 4) : ContDiffAt ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => fderiv ℝ (fun (y : Homogenization.Vec 2) => X z.1 y s) (X s z.2 z.1)) (t, x)

The actual pulled spatial flow Jacobian is jointly smooth on the same short interval as the actual forward and inverse flow.

theorem AVenhance.Infra.Section4.amnr_pulledFlowGradientEntry_contDiffAt_of_short {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {M : ℝ} (hM : 0 ≤ M) (hstate : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b t x‖ ≤ M) (s t : ℝ) (x : Homogenization.Vec 2) (hshort : |t - s| * M ≤ 1 / 4) (i j : Fin 2) : ContDiffAt ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => gradMatrix (fun (y : Homogenization.Vec 2) => X z.1 y s) (X s z.2 z.1) i j) (t, x)

Each actual source matrix entry inherits the actual pulled-Jacobian joint smoothness, in the row convention.