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

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

The integrand (κ I + ψ_m(t,x) σ)(I + ∇Χ^κ_m(t,x)) of e.am.kappa.def (label 2971).

Equations

• I.fluxIntegrand κ m t x = (κ • 1 + I.psiM m t x • AVenhance.sigmaMat) * (1 + AVenhance.gradMatrix (I.chiM κ m t) x)