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

noncomputable def AVenhance.timeAvgMat (F : ℝ → Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ

Entrywise ⟨⟨F⟩⟩ = ∫_0^1 F dt (line 922; e.Kbarm.def, label 2983: ∫_0^1 J dt = ⟨⟨·⟩⟩).

Equations

• AVenhance.timeAvgMat F = Matrix.of fun (i j : Fin 2) => ∫ (t : ℝ) in 0..1, F t i j