Iterates Flow Geometry

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_flowGrad_joint_smooth {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) : ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2

Joint smoothness of the actual matrix, assembled from its proved entries.

theorem AVenhance.Infra.Section4.iterate_flowGrad_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : IsZ2Periodic (I.flowGrad hΦ m l t)

Periodicity holds at every time, including the initial time.

theorem AVenhance.Infra.Section4.iterate_flowGrad_entry_eq_composed {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (i j : Fin 2) : (I.flowGrad hΦ m l t x - 1) i j = (constructionComposedFlowJacobian hΦ (m - 1) (↑l * tauPP β I.Λ m) (t - ↑l * tauPP β I.Λ m) x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) (Homogenization.basisVec i) j

Respect the transposed row/column convention when crossing to Section 2's continuous-linear-map Jacobian.

theorem AVenhance.Infra.Section4.iterate_flowGrad_barNorm {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {l : ℤ} {t : ℝ} (hne : I.hatXiML m l t ≠ 0) (n : ℕ) (i j : Fin 2) : (barNorm n (2 ^ 10 * (epsilon β I.Λ (m - 1))⁻¹) fun (x : Homogenization.Vec 2) => (I.flowGrad hΦ m l t x - 1) i j) ≤ ENNReal.ofReal 40

The actual active flow entries inherit the all-order composed seminorm.