English
If f.norm ≠ g.norm, then (f + g).norm = max f.norm g.norm.
Русский
Если нормы различны, то сумма имеет норму равную максимуму из норм.
LaTeX
$$f.norm ≠ g.norm → (f + g).norm = \max\{f.norm, g.norm\}$$
Lean4
theorem add_eq_max_of_ne {f g : PadicSeq p} (hfgne : f.norm ≠ g.norm) : (f + g).norm = max f.norm g.norm := by
classical
have hfg : ¬f + g ≈ 0 := mt norm_eq_of_add_equiv_zero hfgne
exact
if hf : f ≈ 0 then by
have : LimZero (f - 0) := hf
have : f + g ≈ g := show LimZero (f + g - g) by simpa only [sub_zero, add_sub_cancel_right]
have h1 : (f + g).norm = g.norm := norm_equiv this
have h2 : f.norm = 0 := (norm_zero_iff _).2 hf
rw [h1, h2, max_eq_right (norm_nonneg _)]
else
if hg : g ≈ 0 then by
have : LimZero (g - 0) := hg
have : f + g ≈ f := show LimZero (f + g - f) by simpa only [add_sub_cancel_left, sub_zero]
have h1 : (f + g).norm = f.norm := norm_equiv this
have h2 : g.norm = 0 := (norm_zero_iff _).2 hg
rw [h1, h2, max_eq_left (norm_nonneg _)]
else by
unfold norm at hfgne ⊢;
split_ifs at hfgne
⊢
-- Porting note: originally `padic_index_simp [hfg, hf, hg] at hfgne ⊢`
rw [lift_index_left hf, lift_index_right hg] at hfgne
· rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
exact padicNorm.add_eq_max_of_ne hfgne
