English
If padicNorm p q ≠ padicNorm p r, then padicNorm p (q + r) equals the maximum of the two norms.
Русский
Если padicNorm p q не равно padicNorm p r, то padicNorm p (q + r) равно максимуму из двух норм.
LaTeX
$$$ padicNorm\ p\ q \neq padicNorm\ p\ r \rightarrow padicNorm\ p\ (q + r) = \max\left( padicNorm\ p\ q, padicNorm\ p\ r \right) $$$
Lean4
/-- If the `p`-adic norms of `q` and `r` are different, then the norm of `q + r` is equal to the max
of the norms of `q` and `r`. -/
theorem add_eq_max_of_ne {q r : ℚ} (hne : padicNorm p q ≠ padicNorm p r) :
padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r) :=
by
wlog hlt : padicNorm p r < padicNorm p q
· rw [add_comm, max_comm]
exact this hne.symm (hne.lt_or_gt.resolve_right hlt)
have : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r) :=
calc
padicNorm p q = padicNorm p (q + r + (-r)) := by ring_nf
_ ≤ max (padicNorm p (q + r)) (padicNorm p (-r)) := padicNorm.nonarchimedean
_ = max (padicNorm p (q + r)) (padicNorm p r) := by simp
have hnge : padicNorm p r ≤ padicNorm p (q + r) :=
by
apply le_of_not_gt
intro hgt
rw [max_eq_right_of_lt hgt] at this
exact not_lt_of_ge this hlt
have : padicNorm p q ≤ padicNorm p (q + r) := by rwa [max_eq_left hnge] at this
apply _root_.le_antisymm
· apply padicNorm.nonarchimedean
· rwa [max_eq_left_of_lt hlt]
