smoothingFun_one_le — Mathlib

English

If μ(1) ≤ 1, then smoothingFun μ 1 ≤ 1.

Русский

Если μ(1) ≤ 1,то smoothingFun μ 1 ≤ 1.

LaTeX

$$$smoothingFun μ 1 ≤ 1$$$

Lean4

/-- If `μ 1 ≤ 1`, then `smoothingFun μ 1 ≤ 1`. -/
theorem smoothingFun_one_le (hμ1 : μ 1 ≤ 1) : smoothingFun μ 1 ≤ 1 :=
  by
  apply le_of_tendsto (tendsto_smoothingFun_of_map_one_le_one μ hμ1 (1 : R))
  simp only [eventually_atTop, ge_iff_le]
  use 1
  rintro n hn
  simp only [smoothingSeminormSeq]
  rw [one_pow]
  conv_rhs => rw [← one_rpow (1 / n : ℝ)]
  have hn1 : 0 < (1 / n : ℝ) := by
    apply _root_.div_pos zero_lt_one
    rw [← cast_zero, cast_lt]
    exact succ_le_iff.mp hn
  exact (rpow_le_rpow_iff (apply_nonneg μ _) zero_le_one hn1).mpr hμ1

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