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

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

e.Kbarm.def (label 2983): KBar^κ_m := ∫_0^1 J^κ_m(t) dt, as a matrix.

Equations

• I.Khom κ m = AVenhance.timeAvgMat fun (t : ℝ) => I.flux κ m t