Statement file: flux (Section3). This file contains exactly one declaration of the formalization's public statement surface.

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

e.am.kappa.def (label 2971): J^κ_m(t) = ⟨(κ I + ψ_m(t,·) σ)(I + ∇Χ^κ_m(t,·))⟩.

Equations

• I.flux κ m t = AVenhance.spaceAvgMat (I.fluxIntegrand κ m t)