seminormFromConst_isNonarchimedean

English

The sequence n ↦ seminormFromConst_seq c f x is antitone in n, i.e., nonincreasing as n grows.

Русский

Последовательность $\operatorname{seminormFromConstSeq}(x)$ по n убывающая.

LaTeX

$$Antitone(\lambda n. seminormFromConst_seq c f x n)$$

Lean4

/-- The function `seminormFromConst' hf1 hc hpm` is nonarchimedean. -/
theorem seminormFromConst_isNonarchimedean (hna : IsNonarchimedean f) :
    IsNonarchimedean (seminormFromConst' hf1 hc hpm) := fun x y ↦
  by
  apply
    le_of_tendsto_of_tendsto' (seminormFromConst_isLimit hf1 hc hpm (x + y))
      ((seminormFromConst_isLimit hf1 hc hpm x).max (seminormFromConst_isLimit hf1 hc hpm y))
  intro n
  have hmax : f ((x + y) * c ^ n) ≤ max (f (x * c ^ n)) (f (y * c ^ n)) := by simp only [add_mul, hna _ _]
  rw [le_max_iff] at hmax ⊢
  unfold seminormFromConst_seq
  apply hmax.imp <;> intro <;> gcongr

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