lift_index_left — Mathlib

English

For nonzero f, the p-adic norm at the stationary point equals the norm at the index max(v1, max(stationaryPoint, v3)).

Русский

Для ненулевой последовательности f норма в стационарной точке равна норме в индексе max(v1, max(stationaryPoint, v3)).

LaTeX

$$$\|f(\mathrm{stationaryPoint}(hf))\|_p = \|f(\max(v_1, \max(\mathrm{stationaryPoint}(hf), v_3)))\|_p$$$

Lean4

/-- An auxiliary lemma for manipulating sequence indices. -/
theorem lift_index_left {f : PadicSeq p} (hf : ¬f ≈ 0) (v1 v3 : ℕ) :
    padicNorm p (f (stationaryPoint hf)) = padicNorm p (f (max v1 (max (stationaryPoint hf) v3))) :=
  by
  apply stationaryPoint_spec hf
  · apply le_trans
    · apply le_max_left _ v3
    · apply le_max_right
  · exact le_rfl

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