Statement file: corrTime (Section3).
This file contains exactly one declaration of the formalization's public statement surface.
noncomputable def
AVenhance.Ingredients.corrTime
{β : ℝ}
(I : Ingredients β)
(κ : ℝ)
(m : ℕ)
(k : ℤ)
(t : ℝ)
:
The time integral in e.Chimk.formula (label 2831):
∫_{-∞}^t ζ̂_{m,l_k}(s) ζ_{m,k}(s) exp(4π²κ/ε_m² (s-t)) ds.