dist_integralSum_integral_le_of_memBaseSet

English

If h is Integrable and π is a tagged partition with c in base set, the distance between integralSum and integral is ≤ ε.

Русский

Если h интегрируем, и π образует базовый набор, расстояние между integralSum и integral не превышает ε.

LaTeX

$$$\text{dist}(\text{integralSum } f vol π, \text{integral } I l f vol) ≤ ε$$$

Lean4

theorem dist_integralSum_integral_le_of_memBaseSet (h : Integrable I l f vol) (h₀ : 0 < ε)
    (hπ : l.MemBaseSet I c (h.convergenceR ε c) π) (hπp : π.IsPartition) :
    dist (integralSum f vol π) (integral I l f vol) ≤ ε :=
  by
  rw [convergenceR, dif_pos h₀] at hπ
  exact (hasIntegral_iff.1 h.hasIntegral ε h₀).choose_spec.2 c _ hπ hπp

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