Integrable — Mathlib

English

A function is integrable on box I with respect to l and vol if there exists a y such that HasIntegral I l f vol y holds.

Русский

Функция интегрируема на коробке I по отношению к l и vol, если существует y с HasIntegral I l f vol y.

LaTeX

$$$\mathrm{Integrable}(I, l, f, vol) \iff \exists y\,\mathrm{HasIntegral}(I, l, f, vol, y)$$$

Lean4

/-- A function is integrable if there exists a vector that satisfies the `HasIntegral`
predicate. -/
def Integrable (I : Box ι) (l : IntegrationParams) (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) :=
  ∃ y, HasIntegral I l f vol y

Похожие утверждения