zero_mem_lowerBounds_smoothingSeminormSeq_range

English

For every x ∈ R, the value 0 is a lower bound for the range of smoothingSeminormSeq μ x, i.e., ∀n, μ(x^n)^{1/n} ≥ 0.

Русский

Для каждого x ∈ R нуль является нижней гранью диапазона smoothingSeminormSeq μ x, то есть ∀n, μ(x^n)^{1/n} ≥ 0.

LaTeX

$$$0 \le μ(x^n)^{1/n}$ for all n ∈ ℕ_{+}$$

Lean4

/-- `0` is a lower bound of `smoothingSeminormSeq`. -/
theorem zero_mem_lowerBounds_smoothingSeminormSeq_range (x : R) :
    0 ∈ lowerBounds (Set.range fun n : ℕ+ => μ (x ^ (n : ℕ)) ^ (1 / (n : ℝ))) :=
  by
  rintro y ⟨n, rfl⟩
  exact rpow_nonneg (apply_nonneg μ _) _

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