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