English
If f is not equivalent to zero, then the p-adic norm at the stationary point equals the norm at a larger index given by max(v2, v3) and the stationary point.
Русский
Если f не эквивалентна нулю, то норма в стационарной точке равна норме в более крупном индексе, получаемом как максимум из стационарной точки и max(v2, v3).
LaTeX
$$$\|f(\mathrm{stationaryPoint}(hf))\|_p = \|f(\max(\mathrm{stationaryPoint}(hf),\max(v_2,v_3)))\|_p$$$
Lean4
/-- An auxiliary lemma for manipulating sequence indices. -/
theorem lift_index_left_left {f : PadicSeq p} (hf : ¬f ≈ 0) (v2 v3 : ℕ) :
padicNorm p (f (stationaryPoint hf)) = padicNorm p (f (max (stationaryPoint hf) (max v2 v3))) :=
by
apply stationaryPoint_spec hf
· apply le_max_left
· exact le_rfl