English
The integral is defined as the value y if the function is integrable, and 0 otherwise.
Русский
Интеграл определяется как y, если функция интегрируема, иначе 0.
LaTeX
$$$\mathrm{integral}(I, l, f, vol) = \begin{cases} y, & \text{если } \mathrm{Integrable}(I, l, f, vol) \text{ holds with } y, \\ 0, & \text{иначе}. \end{cases}$$$
Lean4
/-- The integral of a function `f` over a box `I` along a filter `l` w.r.t. a volume `vol`.
Returns zero on non-integrable functions. -/
def integral (I : Box ι) (l : IntegrationParams) (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) :=
if h : Integrable I l f vol then h.choose
else
0
-- Porting note: using the above notation ℝⁿ here causes the theorem below to be silently ignored
-- see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Lean.204.20doesn't.20add.20lemma.20to.20the.20environment/near/363764522
-- and https://github.com/leanprover/lean4/issues/2257
