Public statement.

noncomputable def AVenhance.Ingredients.Jhat {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (t : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

JHat^κ_m(t) := κ I + ∑_{n=0}^{N_*-1} L^κ_{m,n}(t) 𝐣^κ_{m,n}(t), e.Jhat (3056-3060).

Equations

• I.Jhat κ m t = κ • 1 + ∑ n ∈ Finset.range (AVenhance.Nstar β), I.LMN κ m n t • I.jMN κ m n t