English
If f + g ≈ 0, then f.norm = g.norm.
Русский
Если f + g эквивалентна нулю, то f.norm = g.norm.
LaTeX
$$f + g \approx 0 \Rightarrow f.norm = g.norm$$
Lean4
theorem norm_eq {f g : PadicSeq p} (h : ∀ k, padicNorm p (f k) = padicNorm p (g k)) : f.norm = g.norm := by
classical
exact
if hf : f ≈ 0 then by
have hg : g ≈ 0 := equiv_zero_of_val_eq_of_equiv_zero h hf
simp only [hf, hg, norm, dif_pos]
else by
have hg : ¬g ≈ 0 := fun hg ↦ hf <| equiv_zero_of_val_eq_of_equiv_zero (by simp only [h, forall_const]) hg
simp only [hg, hf, norm, dif_neg, not_false_iff]
let i := max (stationaryPoint hf) (stationaryPoint hg)
have hpf : padicNorm p (f (stationaryPoint hf)) = padicNorm p (f i) :=
by
apply stationaryPoint_spec
· apply le_max_left
· exact le_rfl
have hpg : padicNorm p (g (stationaryPoint hg)) = padicNorm p (g i) :=
by
apply stationaryPoint_spec
· apply le_max_right
· exact le_rfl
rw [hpf, hpg, h]
