Identification of the four slow-factor estimates with the actual selected flow and the derivative-row matrix convention.

theorem AVenhance.Infra.Section5.slowFactorG_eq_mulVec (B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (T : Homogenization.Vec 2 → ℝ) (j : Fin 2) : slowFactorG B T j = fun (x : Homogenization.Vec 2) => (B x).mulVec (spaceGrad T x) j

theorem AVenhance.Infra.Section5.slowFactorDiv_eq_vecDiv (B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (T : Homogenization.Vec 2 → ℝ) : slowFactorDiv B T = vecDiv fun (x : Homogenization.Vec 2) => (B x).mulVec (spaceGrad T x)

theorem AVenhance.Infra.Section5.slowFactorGradDiv_eq_gradDiv (B : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (i : Fin 2) : slowFactorGradDiv (B t) (T t) i = fun (x : Homogenization.Vec 2) => gradDiv (fun (s : ℝ) (y : Homogenization.Vec 2) => (B s y).mulVec (spaceGrad (T s) y)) t x i

theorem AVenhance.Infra.Section5.SlowFactorBoundsSource.slowFactor_xFlow_right_inverse {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : I.xFlow hΦ m l t (I.xFlowInv hΦ m l t x) = x

theorem AVenhance.Infra.Section5.slowFactorG_eq_actual_G {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (l : ℤ) (t : ℝ) (hT : ContDiff ℝ (↑⊤) (T t)) (j : Fin 2) : slowFactorG (I.flowGrad hΦ m l t) (T t) j = fun (x : Homogenization.Vec 2) => G I hΦ m T l t x j

Exact pullback-gradient identity for the selected flow, proved rather than included as an analytic premise.

theorem AVenhance.Infra.Section5.slowFactorH_eq_actual_gradG {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (l : ℤ) (t : ℝ) (hT : ContDiff ℝ (↑⊤) (T t)) (i j : Fin 2) : slowFactorH (I.flowGrad hΦ m l t) (T t) i j = fun (x : Homogenization.Vec 2) => gradG I hΦ m T l t x i j

noncomputable def AVenhance.Infra.Section5.section5SlowChoice1 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (j : Fin 2) (x : Homogenization.Vec 2) : ℝ

e.fg.choice.1 with the actual l_k, including the K+s coefficient.

Equations

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

noncomputable def AVenhance.Infra.Section5.section5SlowChoice2 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (a j : Fin 2) (x : Homogenization.Vec 2) : ℝ

Cutoff-weighted Hessian slow factor for the Section 5 temperature estimate.

Equations

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

noncomputable def AVenhance.Infra.Section5.section5SlowChoice3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (a j : Fin 2) (x : Homogenization.Vec 2) : ℝ

Choice 3 uses the transpose required by the push-forward convention.

Equations

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

theorem AVenhance.Infra.Section5.section5SlowChoice1_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (j : Fin 2) : section5SlowChoice1 I hΦ m κ T k t j = slowFactorChoice1 (I.xiMK m k t) (I.flowGrad hΦ m (lIdx β I.Λ m k) t) (fun (x : Homogenization.Vec 2) => I.Kmat κ m t + I.sMat hΦ m κ t x) (T t) j