Iterates Actual Primitive Flat

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_increment_gradient_primitive_flat_component {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hm : 1 ≤ m) (hκm : 0 < κm) (i : ℕ) (hi : i + 1 ≤ Nstar β) (w : List (Fin 2)) (j k : Fin 2) {s : ℝ} (hs : 0 ≤ s) (hs1 : s ≤ 1) : have u := fun (t : ℝ) => iterateSpatialWord w (iterateIncrement T (i + 1) t); have v := fun (t : ℝ) => iterateSpatialWord w (iterateIncrement T i t); have b := streamVel (Φ (m - 1)); have q := fun (t : ℝ) => iterateKmatPrimitive I κm m t j k; ∫ (z : AmnrSpace) in iterateTruncatedCell s, (I.Kmat κm m z.1 j k - timeAvgMat (I.Kmat κm m) j k) * spaceGrad (u z.1) z.2 j * spaceGrad (v z.1) z.2 k = ((∫ (x : Homogenization.Vec 2) in unitCube, spaceGrad (u s) x j * (q s * spaceGrad (v s) x k)) - ∫ (z : AmnrSpace) in iterateTruncatedCell s, q z.1 * spaceGrad (u z.1) z.2 j * amnrMaterial b (fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (v t) x k) z.1 z.2) - ∫ (z : AmnrSpace) in iterateTruncatedCell s, q z.1 * spaceGrad (v z.1) z.2 k * amnrMaterial b (fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (u t) x j) z.1 z.2

The actual scalar primitive identity on the terminal space-time cell; all three component pairings have natural integrability.