convergenceR_cond — Mathlib

English

If h is Integrable, then l.convergenceR ε c satisfies the RCond predicate.

Русский

Если h интегрируем, то l.convergenceR ε c удовлетворяет предикату RCond.

LaTeX

$$$l.RCond (h.convergenceR ε c)$$$

Lean4

theorem convergenceR_cond (h : Integrable I l f vol) (ε : ℝ) (c : ℝ≥0) : l.RCond (h.convergenceR ε c) :=
  by
  rw [convergenceR]; split_ifs with h₀
  exacts [(hasIntegral_iff.1 h.hasIntegral ε h₀).choose_spec.1 _, fun _ x => rfl]

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