English
For f, g in PreTilt(O, p), the auxiliary valuation satisfies the non-Archimedean (ultrametric) inequality: valAux(K, v, O, p)(f + g) ≤ max(valAux(K, v, O, p)(f), valAux(K, v, O, p)(g)).
Русский
Для f, g из PreTilt(O, p) вспомогательная оценка удовлетворяет неархимовой (ультраметрической) неравенности: valAux(K, v, O, p)(f + g) ≤ max(valAux(K, v, O, p)(f), valAux(K, v, O, p)(g)).
LaTeX
$$$valAux(K,v,O,p)(f+g) \le \max\{ valAux(K,v,O,p)(f),\ valAux(K,v,O,p)(g)\}$$$
Lean4
theorem valAux_add (f g : PreTilt O p) : valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g) :=
by
by_cases hf : f = 0
· rw [hf, zero_add, valAux_zero, max_eq_right]; exact zero_le _
by_cases hg : g = 0
· rw [hg, add_zero, valAux_zero, max_eq_left]; exact zero_le _
by_cases hfg : f + g = 0
· rw [hfg, valAux_zero]; exact zero_le _
replace hf : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 fun h => hf <| Perfection.ext h
replace hg : ∃ n, coeff _ _ n g ≠ 0 := not_forall.1 fun h => hg <| Perfection.ext h
replace hfg : ∃ n, coeff _ _ n (f + g) ≠ 0 := not_forall.1 fun h => hfg <| Perfection.ext h
obtain ⟨m, hm⟩ := hf; obtain ⟨n, hn⟩ := hg; obtain ⟨k, hk⟩ := hfg
replace hm := coeff_ne_zero_of_le hm (le_trans (le_max_left m n) (le_max_left _ k))
replace hn := coeff_ne_zero_of_le hn (le_trans (le_max_right m n) (le_max_left _ k))
replace hk := coeff_ne_zero_of_le hk (le_max_right (max m n) k)
rw [valAux_eq hv hm, valAux_eq hv hn, valAux_eq hv hk, RingHom.map_add]
rcases le_max_iff.1 (ModP.preVal_add hv (coeff _ _ (max (max m n) k) f) (coeff _ _ (max (max m n) k) g)) with h | h
· exact le_max_of_le_left (pow_le_pow_left' h _)
· exact le_max_of_le_right (pow_le_pow_left' h _)
