English
The norm is nonarchimedean: (f + g).norm ≤ max(f.norm, g.norm).
Русский
Норма неархимедова: (f+g).norm ≤ max(f.norm, g.norm).
LaTeX
$$(f + g).norm ≤ \max\{f.norm, g.norm\}$$
Lean4
theorem norm_nonarchimedean (f g : PadicSeq p) : (f + g).norm ≤ max f.norm g.norm := by
classical
exact
if hfg : f + g ≈ 0 then by
have : 0 ≤ max f.norm g.norm := le_max_of_le_left (norm_nonneg _)
simpa only [hfg, norm]
else
if hf : f ≈ 0 then
by
have hfg' : f + g ≈ g := by
change LimZero (f - 0) at hf
change LimZero (f + g - g); · simpa only [sub_zero, add_sub_cancel_right] using hf
have hcfg : (f + g).norm = g.norm := norm_equiv hfg'
have hcl : f.norm = 0 := (norm_zero_iff f).2 hf
have : max f.norm g.norm = g.norm := by rw [hcl]; exact max_eq_right (norm_nonneg _)
rw [this, hcfg]
else
if hg : g ≈ 0 then
by
have hfg' : f + g ≈ f := by
change LimZero (g - 0) at hg
change LimZero (f + g - f); · simpa only [add_sub_cancel_left, sub_zero] using hg
have hcfg : (f + g).norm = f.norm := norm_equiv hfg'
have hcl : g.norm = 0 := (norm_zero_iff g).2 hg
have : max f.norm g.norm = f.norm := by rw [hcl]; exact max_eq_left (norm_nonneg _)
rw [this, hcfg]
else norm_nonarchimedean_aux hfg hf hg
