Component estimates for the four Appendix C slow factors, including order zero. The matrix contractions follow the derivative-row convention.

noncomputable def AVenhance.Infra.Section5.slowFactorChoice1 (ξ : ℝ) (Q B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (T : Homogenization.Vec 2 → ℝ) (j : Fin 2) : Homogenization.Vec 2 → ℝ

Slow factor formed by contracting the flow matrix with the gradient-divergence term.

Equations

• AVenhance.Infra.Section5.slowFactorChoice1 ξ Q B T j = ξ • ∑ i : Fin 2, (fun (x : Homogenization.Vec 2) => Q x j i) * AVenhance.Infra.Section5.slowFactorGradDiv B T i

noncomputable def AVenhance.Infra.Section5.slowFactorContractH (A Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (T : Homogenization.Vec 2 → ℝ) (a j : Fin 2) : Homogenization.Vec 2 → ℝ

This is the contraction arising when matDiv differentiates a matrix product: its i-th derivative pairs with the i-th row of A.

Equations

• AVenhance.Infra.Section5.slowFactorContractH A Q T a j = ∑ i : Fin 2, (fun (x : Homogenization.Vec 2) => A x i a) * AVenhance.Infra.Section5.slowFactorH Q T i j

noncomputable def AVenhance.Infra.Section5.slowFactorChoice2 (ξ κ : ℝ) (A Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (T : Homogenization.Vec 2 → ℝ) (a j : Fin 2) : Homogenization.Vec 2 → ℝ

Slow factor formed by contracting the Hessian contribution with two matrix fields.

Equations

• AVenhance.Infra.Section5.slowFactorChoice2 ξ κ A Q T a j = ξ • κ • AVenhance.Infra.Section5.slowFactorContractH A Q T a j

noncomputable def AVenhance.Infra.Section5.slowFactorChoice3 (ξ : ℝ) (Y Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (T : Homogenization.Vec 2 → ℝ) (a j : Fin 2) : Homogenization.Vec 2 → ℝ

The actual corrected push-forward factor uses Y=1-Q.transpose.

Equations

• AVenhance.Infra.Section5.slowFactorChoice3 ξ Y Q T a j = ξ • AVenhance.Infra.Section5.slowFactorContractH Y Q T a j

theorem AVenhance.Infra.Section5.slowFactorContractH_word_bound {Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {T : Homogenization.Vec 2 → ℝ} (hQ : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => Q x i j) (hT : ContDiff ℝ (↑⊤) T) {CQ M L : ℝ} (hCQ : 0 ≤ CQ) (hM : 0 ≤ M) (hL : 0 ≤ L) (μ : MeasureTheory.Measure (Homogenization.Vec 2)) (hQb : ∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2), |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => Q y i j) x| ≤ CQ * ↑w.length.factorial * L ^ w.length) (hTb : ∀ (w : List (Fin 2)), 0 < w.length → MeasureTheory.eLpNorm (Section4.amnrSpaceWord w T) 2 μ ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length)) {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hA : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => A x i j) {CA : ℝ} (hCA : 0 ≤ CA) (hAb : ∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2), |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => A y i j) x| ≤ CA * ↑w.length.factorial * L ^ w.length) (a j : Fin 2) (w : List (Fin 2)) : MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (slowFactorContractH A Q T a j)) 2 μ ≤ ENNReal.ofReal (64 * CA * CQ * M * L ^ 2 * ↑w.length.factorial * (16 * L) ^ w.length)

theorem AVenhance.Infra.Section5.slowFactorChoice1_word_bound {Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {T : Homogenization.Vec 2 → ℝ} (hQ : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => Q x i j) (hT : ContDiff ℝ (↑⊤) T) {CQ M L : ℝ} (hCQ : 0 ≤ CQ) (hM : 0 ≤ M) (hL : 0 ≤ L) (μ : MeasureTheory.Measure (Homogenization.Vec 2)) (hQb : ∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2), |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => Q y i j) x| ≤ CQ * ↑w.length.factorial * L ^ w.length) (hTb : ∀ (w : List (Fin 2)), 0 < w.length → MeasureTheory.eLpNorm (Section4.amnrSpaceWord w T) 2 μ ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length)) {B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hB : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => B x i j) {CB ξ : ℝ} (hCB : 0 ≤ CB) (hξ : |ξ| ≤ 1) (hBb : ∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2), |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => B y i j) x| ≤ CB * ↑w.length.factorial * L ^ w.length) (j : Fin 2) (w : List (Fin 2)) : MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (slowFactorChoice1 ξ Q B T j)) 2 μ ≤ ENNReal.ofReal (2048 * CQ * CB * M * L ^ 3 * ↑w.length.factorial * (16 * L) ^ w.length)

theorem AVenhance.Infra.Section5.slowFactorChoice3_word_bound {Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {T : Homogenization.Vec 2 → ℝ} (hQ : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => Q x i j) (hT : ContDiff ℝ (↑⊤) T) {CQ M L : ℝ} (hCQ : 0 ≤ CQ) (hM : 0 ≤ M) (hL : 0 ≤ L) (μ : MeasureTheory.Measure (Homogenization.Vec 2)) (hQb : ∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2), |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => Q y i j) x| ≤ CQ * ↑w.length.factorial * L ^ w.length) (hTb : ∀ (w : List (Fin 2)), 0 < w.length → MeasureTheory.eLpNorm (Section4.amnrSpaceWord w T) 2 μ ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length)) {Y : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hY : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => Y x i j) {CY ξ : ℝ} (hCY : 0 ≤ CY) (hξ : |ξ| ≤ 1) (hYb : ∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2), |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => Y y i j) x| ≤ CY * ↑w.length.factorial * L ^ w.length) (a j : Fin 2) (w : List (Fin 2)) : MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (slowFactorChoice3 ξ Y Q T a j)) 2 μ ≤ ENNReal.ofReal (64 * CY * CQ * M * L ^ 2 * ↑w.length.factorial * (16 * L) ^ w.length)