The primitive gradient PDE for every actual temperature iterate.

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

Temperature flux associated with a specified iterate.

Equations

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

theorem AVenhance.Infra.Section4.amnr_tIterates_gradient_pde {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (i : ℕ) (hi : i ≤ Nstar β) (p : Fin 2) : Set.EqOn (amnrOp (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) none (amnrTGradient (T i) p)) (fun (z : AmnrSpace) => κprev * ∑ q : Fin 2, amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) [some q, some q] (amnrTGradient (T i) p) z + ∑ q : Fin 2, amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) [some p, some q] (amnrIterateFlux I hΦ m κm κprev T i q) z - ∑ q : Fin 2, amnrVelocityGradient (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) q p z * amnrTGradient (T i) q z) (Set.Ioi 0 ×ˢ Set.univ)