English
For any complex CauSeq f, f is equivalent to the constant CauSeq with value limAux f, i.e., f ≈ CauSeq.const (||·||) (limAux f).
Русский
Для любой комплексной CauSeq f справедливо равенство f ≈ CauSeq.const (||·||) (limAux f).
LaTeX
$$$f \\approx CauSeq.const(\\\\|\\\\cdot\\\\|) (\\\\limAux f)$$$
Lean4
theorem equiv_limAux (f : CauSeq ℂ (‖·‖)) : f ≈ CauSeq.const (‖·‖) (limAux f) := fun ε ε0 ↦
(exists_forall_ge_and (CauSeq.equiv_lim ⟨_, isCauSeq_re f⟩ _ (half_pos ε0))
(CauSeq.equiv_lim ⟨_, isCauSeq_im f⟩ _ (half_pos ε0))).imp
fun _ H j ij ↦ by
obtain ⟨H₁, H₂⟩ := H _ ij
apply lt_of_le_of_lt (norm_le_abs_re_add_abs_im _)
dsimp [limAux] at *
have := add_lt_add H₁ H₂
rwa [add_halves] at this
