Transported primitive contraction cancellation for the first increment.

theorem AVenhance.Infra.Section4.iterate_material_matrix_square_cancellation {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} {H : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hQ : ∀ (i j : Fin 2), ContDiffOn ℝ 1 (fun (p : AmnrSpace) => Q p.1 i j) (Set.Ici 0 ×ˢ Set.univ)) (hH : ∀ (i j : Fin 2), ContDiffOn ℝ 1 (fun (p : AmnrSpace) => H p.1 p.2 i j) (Set.Ici 0 ×ˢ Set.univ)) (hHs : ∀ (t : ℝ), 0 < t → ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => H t x i j) (hHp : ∀ (t : ℝ), 0 < t → ∀ (i j : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => H t x i j) {T : ℝ} (hT : 0 ≤ T) (hI : MeasureTheory.Integrable (fun (p : AmnrSpace) => (∑ i : Fin 2, ∑ j : Fin 2, Q p.1 i j * H p.1 p.2 i j) * deriv (fun (s : ℝ) => ∑ i : Fin 2, ∑ j : Fin 2, Q s i j * H s p.2 i j) p.1) ((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube))) (hG : MeasureTheory.Integrable (fun (p : AmnrSpace) => (∑ i : Fin 2, ∑ j : Fin 2, deriv (fun (s : ℝ) => Q s i j) p.1 * H p.1 p.2 i j) * ∑ i : Fin 2, ∑ j : Fin 2, Q p.1 i j * H p.1 p.2 i j) ((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube))) (hJ : MeasureTheory.Integrable (fun (p : AmnrSpace) => (∑ i : Fin 2, ∑ j : Fin 2, Q p.1 i j * amnrMaterial (streamVel φ) (fun (s : ℝ) (y : Homogenization.Vec 2) => H s y i j) p.1 p.2) * ∑ i : Fin 2, ∑ j : Fin 2, Q p.1 i j * H p.1 p.2 i j) ((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube))) : ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, (∑ i : Fin 2, ∑ j : Fin 2, deriv (fun (s : ℝ) => Q s i j) t * H t x i j) * ∑ i : Fin 2, ∑ j : Fin 2, Q t i j * H t x i j = ((l2NormSq fun (x : Homogenization.Vec 2) => ∑ i : Fin 2, ∑ j : Fin 2, Q T i j * H T x i j) - l2NormSq fun (x : Homogenization.Vec 2) => ∑ i : Fin 2, ∑ j : Fin 2, Q 0 i j * H 0 x i j) / 2 - ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, (∑ i : Fin 2, ∑ j : Fin 2, Q t i j * amnrMaterial (streamVel φ) (fun (s : ℝ) (y : Homogenization.Vec 2) => H s y i j) t x) * ∑ i : Fin 2, ∑ j : Fin 2, Q t i j * H t x i j

The first-increment contraction has a transported half-square cancellation. The endpoint energy is retained at an arbitrary terminal time. Joint C1 and smooth periodic spatial slices suffice; no quantitative estimate is assumed.

theorem AVenhance.Infra.Section4.iterateKmatPrimitive_entry_contDiff {β : ℝ} (I : Ingredients β) {κ : ℝ} (hκ : 0 < κ) {m : ℕ} (hm : 1 ≤ m) (i j : Fin 2) : ContDiff ℝ (↑(Nstar β) + 1) fun (t : ℝ) => iterateKmatPrimitive I κ m t i j

The actual primitive gains one time derivative over Kmat. This retains the finite approved regularity instead of assuming an infinitely smooth cutoff.

theorem AVenhance.Infra.Section4.iterateKmatPrimitive_entry_joint_contDiff {β : ℝ} (I : Ingredients β) {κ : ℝ} (hκ : 0 < κ) {m : ℕ} (hm : 1 ≤ m) (i j : Fin 2) : ContDiff ℝ 1 fun (p : AmnrSpace) => iterateKmatPrimitive I κ m p.1 i j

The primitive satisfies the joint C1 input of the transported contraction cancellation, as a proved property of the actual formula.