Theorem: log1p_small' (Ray/Misc/Bounds.lean)

State before:
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
by_cases r0 : r ≤ 0
State after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : ¬r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

State before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : ¬r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simp only [not_le] at r0
State after:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

State before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
have fc : ContinuousAt (fun z ↦ log (1 + z)) z := by
  apply ContinuousAt.clog; apply ContinuousAt.add; exact continuousAt_const; exact continuousAt_id
  refine mem_slitPlane_of_near_one ?_
  simp only [add_sub_cancel_left, lt_of_le_of_lt zr r1]
State after:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

State before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
apply weak_to_strong_small r0 (by bound) zr fc
State after:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
⊢ ∀ (z : ℂ), Complex.abs z < r → Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

State before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
⊢ ∀ (z : ℂ), Complex.abs z < r → Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
intro w wr
State after:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
w : ℂ
wr : Complex.abs w < r
⊢ Complex.abs (1 + w).log ≤ 1 / (1 - r) * Complex.abs w

State before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
w : ℂ
wr : Complex.abs w < r
⊢ Complex.abs (1 + w).log ≤ 1 / (1 - r) * Complex.abs w
Tactic:
exact @weak_log1p_small w r (by bound) wr
State after:
no goals

State before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
have z0 := le_antisymm (le_trans zr r0) (Complex.abs.nonneg _)
State after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
z0 : Complex.abs z = 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

State before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
z0 : Complex.abs z = 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simp only [map_eq_zero] at z0
State after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
z0 : z = 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

State before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
z0 : z = 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simp only [z0, add_zero, Complex.log_one, map_zero, r0, sub_zero, ne_eq, one_ne_zero,
  not_false_eq_true, div_self, mul_zero, le_refl]
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun z => (1 + z).log) z
Tactic:
apply ContinuousAt.clog
State after:
case h₁
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun t => 1 + t) z

case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane

State before:
case h₁
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun t => 1 + t) z

case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane
Tactic:
apply ContinuousAt.add
State after:
case h₁.hf
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => 1) z

case h₁.hg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => x) z

case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane

State before:
case h₁.hf
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => 1) z

case h₁.hg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => x) z

case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane
Tactic:
exact continuousAt_const
State after:
case h₁.hg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => x) z

case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane

State before:
case h₁.hg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => x) z

case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane
Tactic:
exact continuousAt_id
State after:
case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane

State before:
case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane
Tactic:
refine mem_slitPlane_of_near_one ?_
State after:
case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ Complex.abs (1 + z - 1) < 1

State before:
case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ Complex.abs (1 + z - 1) < 1
Tactic:
simp only [add_sub_cancel_left, lt_of_le_of_lt zr r1]
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
⊢ 1 / (1 - r) > 0
Tactic:
bound
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
w : ℂ
wr : Complex.abs w < r
⊢ r < 1
Tactic:
bound
State after:
no goals