lift_index_right — Mathlib

English

If hf is a witness that f ≈ 0 is false, then the norm at stationaryPoint equals the norm at max(v1, max(v2, stationaryPoint)).

Русский

Если hf доказывает, что f ≈ 0 ложно, то норма в стационарной точке равна норме в max(v1, max(v2, stationaryPoint)).

LaTeX

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

Lean4

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

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