Infrastructure for the AMNR tensors: bridge from the recursion to the actual flow data.

theorem AVenhance.Infra.Section4.Amnr_zero_factors {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (n : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (i j k : Fin 2) : I.Amnr hΦ m κ n T 0 t x i j k = ∑ p : Fin 2, amnrSeedMultiplierA0Plus I hΦ m κ n j k i p (t, x) * spaceGrad (T t) x p

zero-level identity in primitive multiplier form. This is an identity for the actual finite cutoff sum, not an assumption about A.

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

The primitive multiplier of the seed; it contains the memory coefficient and both flow factors inside the cutoff average.

Equations

• AVenhance.Infra.Section4.amnrSeedMultiplier I hΦ m κ n j k i p z = AVenhance.Infra.Section4.amnrSeedMultiplierA0Plus I hΦ m κ n j k i p z

noncomputable def AVenhance.Infra.Section4.amnrVelocityGradient (b : AmnrSpace → Homogenization.Vec 2) (i p : Fin 2) (z : AmnrSpace) : ℝ

Coordinate derivative of one velocity component at a time-space point.

Equations

• AVenhance.Infra.Section4.amnrVelocityGradient b i p z = AVenhance.spaceGrad (fun (y : Homogenization.Vec 2) => b (z.1, y) i) z.2 p

noncomputable def AVenhance.Infra.Section4.amnrTGradient (T : ℝ → Homogenization.Vec 2 → ℝ) (p : Fin 2) (z : AmnrSpace) : ℝ

Coordinate derivative of the temperature at a time-space point.

Equations

• AVenhance.Infra.Section4.amnrTGradient T p z = AVenhance.spaceGrad (T z.1) z.2 p

theorem AVenhance.Infra.Section4.Amnr_contDiffOn_of_factors {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (n : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) {U : Set AmnrSpace} (hU : IsOpen U) {N : ℕ} (j k : Fin 2) (hb : ContDiffOn ℝ (↑N) (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) U) (hB : ∀ (i p : Fin 2), ContDiffOn ℝ (↑N) (amnrVelocityGradient (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) i p) U) (hf : ∀ (i p : Fin 2), ContDiffOn ℝ (↑N) (amnrSeedMultiplier I hΦ m κ n j k i p) U) (hg : ∀ (p : Fin 2), ContDiffOn ℝ (↑N) (amnrTGradient T p) U) {r a : ℕ} (hr : a + r ≤ N) (i : Fin 2) : ContDiffOn ℝ (↑a) (fun (z : AmnrSpace) => I.Amnr hΦ m κ n T r z.1 z.2 i j k) U

Regularity of the actual recursion, derived before replacing its partial time and spatial derivatives by the joint material direction.

theorem AVenhance.Infra.Section4.Amnr_mixed_induction_of_factors {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (n : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) {U : Set AmnrSpace} (hU : IsOpen U) {μ : MeasureTheory.Measure AmnrSpace} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict U)) (j k : Fin 2) (hb : ContDiffOn ℝ (↑(Nstar β)) (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) U) (hB : ∀ (i p : Fin 2), ContDiffOn ℝ (↑(Nstar β)) (amnrVelocityGradient (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) i p) U) (hf : ∀ (i p : Fin 2), ContDiffOn ℝ (↑(Nstar β)) (amnrSeedMultiplier I hΦ m κ n j k i p) U) (hg : ∀ (p : Fin 2), ContDiffOn ℝ (↑(Nstar β)) (amnrTGradient T p) U) {S H F G Cb : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hF : 0 ≤ F) (hG : 0 ≤ G) (hCb : 0 ≤ Cb) (hfb : ∀ (i p : Fin 2) (w : List (Option (Fin 2))), IsAmnrMixedWord w → amnrBudget w ≤ Nstar β → ∀ z ∈ U, |amnrWord (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) w (amnrSeedMultiplier I hΦ m κ n j k i p) z| ≤ F * amnrWeight S H w) (hgb : ∀ (p : Fin 2) (w : List (Option (Fin 2))), IsAmnrMixedWord w → amnrBudget w ≤ Nstar β → MeasureTheory.eLpNorm (amnrWord (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) w (amnrTGradient T p)) 2 μ ≤ ENNReal.ofReal (G * amnrWeight S H w)) (hBb : ∀ (i p : Fin 2) (w : List (Option (Fin 2))), IsAmnrMixedWord w → amnrBudget w + 2 ≤ Nstar β → ∀ z ∈ U, |amnrWord (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) w (amnrVelocityGradient (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) i p) z| ≤ Cb * H * amnrWeight S H w) (r : ℕ) (hr : r ≤ Jcut β) (α : List (Fin 2)) (ℓ : ℕ) (hbudget : α.length + 2 * ℓ ≤ Nstar β - 2 * r) (i : Fin 2) : MeasureTheory.eLpNorm (amnrWord (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) (amnrMixedWord α ℓ) fun (z : AmnrSpace) => I.Amnr hΦ m κ n T r z.1 z.2 i j k) 2 μ ≤ ENNReal.ofReal (2 ^ (Nstar β + 1) * F * G * (1 + 2 ^ (Nstar β + 1) * Cb) ^ Jcut β * S ^ α.length * H ^ (ℓ + r))

The higher mixed-derivative induction for the actual tensor. Its inputs are bounds on the primitive seed multiplier, gradient of T and velocity gradient, never bounds on A. The constant is uniform over r ≤ Jcut. Discharging the primitive mixed bounds from the paper's preceding estimates is a separate dependency from this contraction induction.