smoothingFun_le — Mathlib

English

For any x and any positive n, smoothingFun μ x ≤ μ(x^n)^{1/n}.

Русский

Для любого x и положительного n, smoothingFun μ x ≤ μ(x^n)^{1/n}.

LaTeX

$$$smoothingFun μ x ≤ μ(x^n)^{1/n}$ for all n ∈ ℕ_{+}$$

Lean4

/-- For any `x` and any positive `n`, `smoothingFun μ x ≤ μ (x ^ (n : ℕ))^(1 / n : ℝ)`. -/
theorem smoothingFun_le (x : R) (n : PNat) : smoothingFun μ x ≤ μ (x ^ (n : ℕ)) ^ (1 / n : ℝ) :=
  ciInf_le (smoothingSeminormSeq_bddBelow μ x) _

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