Regularity of the ansatz θTilde_m: flow ingredients

Joint C^∞ regularity of the flow slices X_{m-1,l}, X⁻¹_{m-1,l}, the partial derivatives of the flow, and the chain rule for the transported gradient (t,x) ↦ ∇(T(t)∘X_{m-1,l}(t,·))(X⁻¹_{m-1,l}(t,x)) written as ∑_j ∂_i X^j(t, X⁻¹(t,x)) ∂_j T(t,x), jointly C^∞ on Ici 0 ×ˢ univ.

theorem AVenhance.Infra.Section5.Integration.AnsatzRegularityFlow.ansFlowSmooth {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) : Flow.SmoothPeriodicField (streamVel (Φ (m - 1)))

theorem AVenhance.Infra.Section5.Integration.AnsatzRegularityFlow.ansFlowIsFlow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) : IsFlow (streamVel (Φ (m - 1))) (flow (streamVel (Φ (m - 1))) ⋯ ⋯)

theorem AVenhance.Infra.Section5.Integration.xFlow_joint_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => I.xFlow hΦ m l p.1 p.2

The forward flow slice is jointly C^∞ in target time and position.

theorem AVenhance.Infra.Section5.Integration.xFlowInv_joint_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => I.xFlowInv hΦ m l p.1 p.2

The inverse flow slice is jointly C^∞ in target time and position.

Partial derivatives of a jointly smooth vector field

theorem AVenhance.Infra.Section5.Integration.gradMatrix_slice_eq {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ (↑⊤) F) (t : ℝ) (y : Homogenization.Vec 2) (i j : Fin 2) : gradMatrix (fun (z : Homogenization.Vec 2) => F (t, z)) y i j = (fderiv ℝ (fun (p : ℝ × Homogenization.Vec 2) => F p j) (t, y)) (0, Homogenization.basisVec i)

Entry (i,j) of the spatial Jacobian of a slice y ↦ F(t,y), as a partial derivative of the joint map.

theorem AVenhance.Infra.Section5.Integration.contDiff_partial {G : ℝ × Homogenization.Vec 2 → ℝ} (hG : ContDiff ℝ (↑⊤) G) (v : ℝ × Homogenization.Vec 2) : ContDiff ℝ ↑⊤ fun (q : ℝ × Homogenization.Vec 2) => (fderiv ℝ G q) v

Every partial derivative of a C^∞ real function on ℝ × Vec 2 is C^∞.

theorem AVenhance.Infra.Section5.Integration.spaceGrad_slice_eq {F : ℝ × Homogenization.Vec 2 → ℝ} {s : Set (ℝ × Homogenization.Vec 2)} (t : ℝ) (x : Homogenization.Vec 2) (hs : ∀ (y : Homogenization.Vec 2), (t, y) ∈ s) (hF : DifferentiableWithinAt ℝ F s (t, x)) (j : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => F (t, y)) x j = (fderivWithin ℝ F s (t, x)) (0, Homogenization.basisVec j)

The spatial gradient of a slice of a function that is C¹ on a set s containing the whole slice is the partial derivative of the joint map within s.

The transported gradient

theorem AVenhance.Infra.Section5.Integration.slice_contDiff_of_contDiffOn {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ (↑⊤) (T t)

A function that is C^∞ on Ici 0 ×ˢ univ is C^∞ on each slice at a nonnegative time.

theorem AVenhance.Infra.Section5.Integration.transportedGrad_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => T p.1 (I.xFlow hΦ m l p.1 y)) (I.xFlowInv hΦ m l p.1 p.2) i) (Set.Ici 0 ×ˢ Set.univ)

∇(T(t)∘X_{m-1,l}(t,·))(X⁻¹_{m-1,l}(t,x)) is, jointly in (t,x), a C^∞ function on Ici 0 ×ˢ univ, whenever T is.