Base infrastructure for the AMNR tensors.

noncomputable def AVenhance.Infra.Section4.amnrFlowAverageGen {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (Q : ℤ → ℝ × Homogenization.Vec 2 → Fin 2 → Fin 2 → ℝ) (j k i p : Fin 2) (z : ℝ × Homogenization.Vec 2) : ℝ

A cutoff-flow average with a freely chosen factor in each summand.

Equations

• AVenhance.Infra.Section4.amnrFlowAverageGen I hΦ m Q j k i p z = ∑' (l : ℤ), I.hatXiML m l z.1 * (Q l z i j * I.flowGrad hΦ m l z.1 z.2 k p)

noncomputable def AVenhance.Infra.Section4.amnrSeedMultiplierGen {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (n : ℕ) (Q : ℤ → ℝ × Homogenization.Vec 2 → Fin 2 → Fin 2 → ℝ) (j k i p : Fin 2) (z : ℝ × Homogenization.Vec 2) : ℝ

A general memory multiplier for a cutoff-flow factor.

Equations

• AVenhance.Infra.Section4.amnrSeedMultiplierGen I hΦ m κ n Q j k i p z = -I.LMN κ m n z.1 * AVenhance.Infra.Section4.amnrFlowAverageGen I hΦ m Q j k i p z

noncomputable def AVenhance.Infra.Section4.amnrSeedMultiplierA0Plus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (n : ℕ) (j k i p : Fin 2) (z : ℝ × Homogenization.Vec 2) : ℝ

The left-Jacobian seed factor, with (F_l)ᵀ_{ij} inside the same cutoff sum as (F_l)_{kp}.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section4.amnrFlowAverageA0Plus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (j k i p : Fin 2) (z : ℝ × Homogenization.Vec 2) : ℝ

Cutoff average in the left-Jacobian seed.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section4.Amnr_succ {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (n : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (t : ℝ) (x : Homogenization.Vec 2) (i j k : Fin 2) : I.Amnr hΦ m κ n T (r + 1) t x i j k = amnrMaterial (streamVel (Φ (m - 1))) (fun (s : ℝ) (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r s y i j k) t x - ∑ p : Fin 2, spaceGrad (fun (y : Homogenization.Vec 2) => streamVel (Φ (m - 1)) t y i) x p * I.Amnr hΦ m κ n T r t x p j k

Exact recurrence, with its minus sign and tensor contraction.

theorem AVenhance.Infra.Section4.Jcut_budget {β : ℝ} (hN : 1 ≤ Nstar β) : 2 * Jcut β + 1 ≤ Nstar β

The corrected truncation leaves one spatial derivative at the remainder.

theorem AVenhance.Infra.Section4.flowGrad_measurable {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (k p : Fin 2) : Measurable fun (z : ℝ × Homogenization.Vec 2) => I.flowGrad hΦ m l z.1 z.2 k p

Measurability of the flow-gradient entries follows from joint flow continuity.

noncomputable def AVenhance.Infra.Section4.amnrMemoryConstant (β C₀ : ℝ) : ℝ

Explicit finite-order memory constant, uniform in n and the scale.

Equations

• AVenhance.Infra.Section4.amnrMemoryConstant β C₀ = ↑(AVenhance.Nstar β).factorial * 2 ^ AVenhance.Nstar β * 2 ^ AVenhance.Nstar β * C₀ ^ 2 / (2 * Real.pi ^ 2)