English
For |z| < 1, log(1 + i z) - log(1 - i z) = log((1 + i z)/(1 - i z)).
Русский
Для |z| < 1 выполняется log(1 + i z) − log(1 − i z) = log((1 + i z)/(1 − i z)).
LaTeX
$$$$\\log(1 + i z) - \\log(1 - i z) = \\log\\left(\\frac{1 + i z}{1 - i z}\\right) \\quad\\text{при } |z| < 1.$$$
Lean4
/-- We can combine the logs in `log (1 + z * I) + -log (1 - z * I)` into one.
This is only used in `hasSum_arctan`. -/
theorem hasSum_arctan_aux {z : ℂ} (hz : ‖z‖ < 1) :
log (1 + z * I) + -log (1 - z * I) = log ((1 + z * I) / (1 - z * I)) :=
by
have z₁ := mem_slitPlane_iff_arg.mp (mem_slitPlane_of_norm_lt_one (z := z * I) (by simpa))
have z₂ := mem_slitPlane_iff_arg.mp (mem_slitPlane_of_norm_lt_one (z := -(z * I)) (by simpa))
rw [← sub_eq_add_neg] at z₂
rw [← log_inv _ z₂.1, ← (log_mul_eq_add_log_iff z₁.2 (inv_eq_zero.ne.mpr z₂.2)).mpr, div_eq_mul_inv]
-- `log_mul_eq_add_log_iff` requires a bound on `arg (1 + z * I) + arg (1 - z * I)⁻¹`.
-- `arg_one_add_mem_Ioo` provides sufficiently tight bounds on both terms
have b₁ := arg_one_add_mem_Ioo (z := z * I) (by simpa)
have b₂ : arg (1 - z * I)⁻¹ ∈ Set.Ioo (-(π / 2)) (π / 2) :=
by
simp_rw [arg_inv, z₂.1, ite_false, Set.neg_mem_Ioo_iff, neg_neg, sub_eq_add_neg]
exact arg_one_add_mem_Ioo (by simpa)
have c₁ := add_lt_add b₁.1 b₂.1
have c₂ := add_lt_add b₁.2 b₂.2
rw [show -(π / 2) + -(π / 2) = -π by ring] at c₁
rw [show π / 2 + π / 2 = π by ring] at c₂
exact ⟨c₁, c₂.le⟩
