Public statement.

noncomputable def AVenhance.Ingredients.Hm {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (Tm1 : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

HTilde_m := ∑_{r} HTilde_{m,r}, e.Hm.def (4241), summed over r = 0,…,Jcut β - 1.

Equations

• I.Hm hΦ m κm Tm1 t x = ∑ r ∈ Finset.range (AVenhance.Jcut β), I.Hmr hΦ m κm Tm1 r t x