dist_summable — Mathlib

English

For any x,y in the product, the series i ↦ min((1/2)^encode i, dist(x_i,y_i)) is summable.

Русский

Для любых x,y в произведении ряд i ↦ min((1/2)^encode i, dist(x_i,y_i)) сходится.

LaTeX

$$$$\nSummable \\left(\\\\lambda i. \\\\min((\\\\tfrac12)^{\\\\encode i}, (\\\\dist(x_i,y_i)))\\\\right).$$$$

Lean4

theorem dist_summable (x y : ∀ i, F i) : Summable fun i : ι => min ((1 / 2) ^ encode i : ℝ) (dist (x i) (y i)) :=
  by
  refine .of_nonneg_of_le (fun i => ?_) (fun i => min_le_left _ _) summable_geometric_two_encode
  exact le_min (pow_nonneg (by simp) _) dist_nonneg

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