English
HasIntegral I l f vol y is the property that the integral sums converge to y along the filter l. In other words, the limit of integralSum f vol along l converges to y.
Русский
HasIntegral I l f vol y означает, что интегральные суммы сходятся к y вдоль фильтра l.
LaTeX
$$$\mathrm{HasIntegral}(I, l, f, vol, y) \;\Longleftrightarrow\; \operatorname{Tendsto}(\mathrm{integralSum} f vol)\,(l.toFilteriUnion I \top)\,(\mathcal{N} y)$$$
Lean4
/-- The predicate `HasIntegral I l f vol y` says that `y` is the integral of `f` over `I` along `l`
w.r.t. volume `vol`. This means that integral sums of `f` tend to `𝓝 y` along
`BoxIntegral.IntegrationParams.toFilteriUnion I ⊤`. -/
def HasIntegral (I : Box ι) (l : IntegrationParams) (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (y : F) : Prop :=
Tendsto (integralSum f vol) (l.toFilteriUnion I ⊤) (𝓝 y)
