seminormFromConst_seq_nonneg — Mathlib

English

Every term of the sequence n ↦ f(x c^n)/f(c^n) is nonnegative when f is nonnegative.

Русский

Каждый член последовательности $n \mapsto f(x c^n)/f(c^n)$ неотрицателен, если f неотрицательная.

LaTeX

$$$\forall n,\ 0 \le \dfrac{f(x c^n)}{f(c^n)}$$$

Lean4

/-- The terms in the sequence `seminormFromConst_seq c f x` are nonnegative. -/
theorem seminormFromConst_seq_nonneg (x : R) : 0 ≤ seminormFromConst_seq c f x := fun n ↦
  div_nonneg (apply_nonneg f (x * c ^ n)) (pow_nonneg (apply_nonneg f c) n)

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