Exact flow-average form of the actual temperature forcing coefficient.

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

Matrix entry of the temperature coefficient after subtracting the previous diffusivity.

Equations

• AVenhance.Infra.Section4.amnrTemperatureCoefficient I hΦ m κm κprev i j z = (I.Kmat κm m z.1 - κprev • 1 + I.sMat hΦ m κm z.1 z.2) i j

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

The quadratic part of the left-Jacobian temperature coefficient, expressed through the mixed two-flow averages used in the source estimates.

Equations

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

theorem AVenhance.Infra.Section4.amnr_hatXi_average_sub_const {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (f : ℤ → ℝ) (d : ℝ) : ∑' (l : ℤ), I.hatXiML m l t * (f l - d) = ∑' (l : ℤ), I.hatXiML m l t * f l - d

The finite cutoff average preserves subtraction of a scalar constant.

theorem AVenhance.Infra.Section4.TemperatureCoefficientIdentity.amnr_temperature_quadratic_window_eq_average {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (i j : Fin 2) (z : AmnrSpace) : ∑' (l : ℤ), I.hatXiML m l z.1 * (((I.flowGrad hΦ m l z.1 z.2).transpose - 1) * (I.Kmat κm m z.1 - κm • 1) * I.flowGrad hΦ m l z.1 z.2) i j = amnrTemperatureQuadraticAverage I hΦ m κm i j z

The left-Jacobian quadratic window equals its contraction against the two-flow cutoff averages.

theorem AVenhance.Infra.Section4.amnrTemperatureCoefficient_eq_average {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm κprev : ℝ) (i j : Fin 2) (z : AmnrSpace) : amnrTemperatureCoefficient I hΦ m κm κprev i j z = (∑ p : Fin 2, I.Kmat κm m z.1 i p * amnrFlowAverage I hΦ m p j z - κprev * if i = j then 1 else 0) + amnrTemperatureQuadraticAverage I hΦ m κm i j z

The actual coefficient is the K-flow average plus the complete quadratic left-Jacobian contribution, minus the preceding diffusivity.