approx_le_one — Mathlib

English

For every n and x, the nth approximation is at most 1.

Русский

Для любого n и x аппроксимация не превышает 1.

LaTeX

$$$\\forall c\\,\\forall n\\,\\forall x:\\ a_{n}(x) \\le 1$$$

Lean4

theorem approx_le_one (c : CU P) (n : ℕ) (x : X) : c.approx n x ≤ 1 := by
  induction n generalizing c with
  | zero => exact indicator_apply_le' (fun _ => le_rfl) fun _ => zero_le_one
  | succ n ihn =>
    simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]
    have := add_le_add (ihn (left c)) (ihn (right c))
    norm_num at this
    exact Iff.mpr (div_le_one zero_lt_two) this

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