Theorem: Complex.abs_log_one_add_le (Ray/Dynamics/Multibrot/Log1p.lean)

State before:
z : ℂ
z1 : abs z < 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have m1 : ∀ t : ℝ, t ≤ 1 → t * abs z < 1 :=
  fun _ m ↦ Right.mul_lt_one_of_le_of_lt_of_nonneg m z1 (Complex.abs.nonneg _)
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have dr : ∀ t : ℝ, t ∈ uIcc 0 1 →
    HasDerivAt (fun t : ℝ ↦ -Real.log (1 - t * abs z)) (- (-abs z / (1 - t * abs z))) t := by
  intro t m
  simp only [ge_iff_le, zero_le_one, uIcc_of_le, mem_Icc] at m
  exact (((hasDerivAt_mul_const _).const_sub _).log ((sub_pos.mpr (m1 _ m.2)).ne')).neg
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
⊢ abs (1 + z).log ≤ -(1 - abs z).log

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have ic : IntervalIntegrable (fun t ↦ z / (1 + t*z)) MeasureTheory.volume 0 1 := by
  apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one
  apply continuousOn_const.div (Continuous.continuousOn (by continuity))
  intro t ⟨t0,t1⟩
  rw [←Complex.abs.ne_zero_iff]
  apply ne_of_gt
  calc abs (1 + t*z)
    _ ≥ Complex.abs 1 - abs (t*z) := Complex.abs.le_add _ _
    _ = 1 - |t| * abs z := by simp only [map_one, map_mul, Complex.abs_ofReal]
    _ > 0 := by refine sub_pos.mpr (m1 _ (abs_le.mpr ⟨by linarith, t1⟩))
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
simp only [neg_div, neg_neg] at dr
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
⊢ abs (1 + z).log ≤ -(1 - abs z).log

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have ir : IntervalIntegrable (fun t ↦ abs z / (1 - t * abs z)) MeasureTheory.volume 0 1 := by
  apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one
  apply continuousOn_const.div (Continuous.continuousOn (by continuity))
  intro t ⟨_,t1⟩; exact ne_of_gt (sub_pos.mpr (m1 _ t1))
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have fc := intervalIntegral.integral_eq_sub_of_hasDerivAt dc ic
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + ↑1 * z).log - (1 + ↑0 * z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + ↑1 * z).log - (1 + ↑0 * z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
have fr := intervalIntegral.integral_eq_sub_of_hasDerivAt dr ir
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + ↑1 * z).log - (1 + ↑0 * z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - 1 * abs z).log - -(1 - 0 * abs z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + ↑1 * z).log - (1 + ↑0 * z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - 1 * abs z).log - -(1 - 0 * abs z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
simp only [Complex.ofReal_one, one_mul, Complex.ofReal_zero, zero_mul, add_zero, Complex.log_one,
  sub_zero, Real.log_one, neg_zero] at fc fr
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - abs z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - abs z).log
⊢ abs (1 + z).log ≤ -(1 - abs z).log
Tactic:
rw [←fc, ←fr, ←Complex.norm_eq_abs]
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - abs z).log
⊢ ‖∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
fc : ∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z) = (1 + z).log
fr : ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z) = -(1 - abs z).log
⊢ ‖∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)
Tactic:
clear dc dr fc fr
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ‖∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ‖∫ (y : ℝ) in 0 ..1, z / (1 + ↑y * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)
Tactic:
apply le_trans (intervalIntegral.norm_integral_le_integral_norm zero_le_one) ?_
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ∫ (x : ℝ) in 0 ..1, ‖z / (1 + ↑x * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ∫ (x : ℝ) in 0 ..1, ‖z / (1 + ↑x * z)‖ ≤ ∫ (y : ℝ) in 0 ..1, abs z / (1 - y * abs z)
Tactic:
apply intervalIntegral.integral_mono_on zero_le_one ic.norm ir
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ∀ x ∈ Icc 0 1, ‖z / (1 + ↑x * z)‖ ≤ abs z / (1 - x * abs z)

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
⊢ ∀ x ∈ Icc 0 1, ‖z / (1 + ↑x * z)‖ ≤ abs z / (1 - x * abs z)
Tactic:
intro t ⟨t0,t1⟩
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ ‖z / (1 + ↑t * z)‖ ≤ abs z / (1 - t * abs z)

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ ‖z / (1 + ↑t * z)‖ ≤ abs z / (1 - t * abs z)
Tactic:
simp only [norm_div, Complex.norm_eq_abs]
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ abs z / abs (1 + ↑t * z) ≤ abs z / (1 - t * abs z)

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ abs z / abs (1 + ↑t * z) ≤ abs z / (1 - t * abs z)
Tactic:
apply div_le_div_of_nonneg_left (Complex.abs.nonneg _) (sub_pos.mpr (m1 _ t1)) ?_
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ 1 - t * abs z ≤ abs (1 + ↑t * z)

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ 1 - t * abs z ≤ abs (1 + ↑t * z)
Tactic:
calc abs (1 + t * z)
  _ ≥ Complex.abs 1 - abs (t * z) := Complex.abs.le_add _ _
  _ = 1 - t * abs z := by
    simp only [map_one, map_mul, Complex.abs_ofReal, _root_.abs_of_nonneg t0]
State after:
no goals

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
⊢ ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
Tactic:
intro t m
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : t ∈ uIcc 0 1
⊢ HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : t ∈ uIcc 0 1
⊢ HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
Tactic:
apply HasDerivAt.clog_real
State after:
case h₁
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : t ∈ uIcc 0 1
⊢ HasDerivAt (fun t => 1 + ↑t * z) z t

case h₂
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : t ∈ uIcc 0 1
⊢ 1 + ↑t * z ∈ slitPlane

State before:
case h₁
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : t ∈ uIcc 0 1
⊢ HasDerivAt (fun t => 1 + ↑t * z) z t
Tactic:
exact ((hasDerivAt_mul_const _).const_add _).comp_ofReal
State after:
no goals

State before:
case h₂
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : t ∈ uIcc 0 1
⊢ 1 + ↑t * z ∈ slitPlane
Tactic:
apply Complex.mem_slitPlane_of_norm_lt_one
State after:
case h₂.hz
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : t ∈ uIcc 0 1
⊢ ‖↑t * z‖ < 1

State before:
case h₂.hz
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : t ∈ uIcc 0 1
⊢ ‖↑t * z‖ < 1
Tactic:
simp only [norm_mul, Complex.norm_eq_abs, Complex.abs_ofReal]
State after:
case h₂.hz
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : t ∈ uIcc 0 1
⊢ |t| * abs z < 1

State before:
case h₂.hz
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : t ∈ uIcc 0 1
⊢ |t| * abs z < 1
Tactic:
simp only [ge_iff_le, zero_le_one, uIcc_of_le, mem_Icc] at m
State after:
case h₂.hz
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : 0 ≤ t ∧ t ≤ 1
⊢ |t| * abs z < 1

State before:
case h₂.hz
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : 0 ≤ t ∧ t ≤ 1
⊢ |t| * abs z < 1
Tactic:
apply m1
State after:
case h₂.hz.a
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : 0 ≤ t ∧ t ≤ 1
⊢ |t| ≤ 1

State before:
case h₂.hz.a
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : 0 ≤ t ∧ t ≤ 1
⊢ |t| ≤ 1
Tactic:
simp only [abs_le]
State after:
case h₂.hz.a
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : 0 ≤ t ∧ t ≤ 1
⊢ -1 ≤ t ∧ t ≤ 1

State before:
case h₂.hz.a
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : 0 ≤ t ∧ t ≤ 1
⊢ -1 ≤ t ∧ t ≤ 1
Tactic:
exact ⟨by linarith, m.2⟩
State after:
no goals

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : 0 ≤ t ∧ t ≤ 1
⊢ -1 ≤ t
Tactic:
linarith
State after:
no goals

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
⊢ ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
Tactic:
intro t m
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
t : ℝ
m : t ∈ uIcc 0 1
⊢ HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
t : ℝ
m : t ∈ uIcc 0 1
⊢ HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
Tactic:
simp only [ge_iff_le, zero_le_one, uIcc_of_le, mem_Icc] at m
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
t : ℝ
m : 0 ≤ t ∧ t ≤ 1
⊢ HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
t : ℝ
m : 0 ≤ t ∧ t ≤ 1
⊢ HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
Tactic:
exact (((hasDerivAt_mul_const _).const_sub _).log ((sub_pos.mpr (m1 _ m.2)).ne')).neg
State after:
no goals

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
⊢ IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
Tactic:
apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
⊢ ContinuousOn (fun t => z / (1 + ↑t * z)) (Icc 0 1)

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
⊢ ContinuousOn (fun t => z / (1 + ↑t * z)) (Icc 0 1)
Tactic:
apply continuousOn_const.div (Continuous.continuousOn (by continuity))
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
⊢ ∀ x ∈ Icc 0 1, 1 + ↑x * z ≠ 0

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
⊢ ∀ x ∈ Icc 0 1, 1 + ↑x * z ≠ 0
Tactic:
intro t ⟨t0,t1⟩
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ 1 + ↑t * z ≠ 0

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ 1 + ↑t * z ≠ 0
Tactic:
rw [←Complex.abs.ne_zero_iff]
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ abs (1 + ↑t * z) ≠ 0

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ abs (1 + ↑t * z) ≠ 0
Tactic:
apply ne_of_gt
State after:
case h
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ 0 < abs (1 + ↑t * z)

State before:
case h
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ 0 < abs (1 + ↑t * z)
Tactic:
calc abs (1 + t*z)
  _ ≥ Complex.abs 1 - abs (t*z) := Complex.abs.le_add _ _
  _ = 1 - |t| * abs z := by simp only [map_one, map_mul, Complex.abs_ofReal]
  _ > 0 := by refine sub_pos.mpr (m1 _ (abs_le.mpr ⟨by linarith, t1⟩))
State after:
no goals

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
⊢ Continuous fun t => 1 + ↑t * z
Tactic:
continuity
State after:
no goals

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ abs 1 - abs (↑t * z) = 1 - |t| * abs z
Tactic:
simp only [map_one, map_mul, Complex.abs_ofReal]
State after:
no goals

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ 1 - |t| * abs z > 0
Tactic:
refine sub_pos.mpr (m1 _ (abs_le.mpr ⟨by linarith, t1⟩))
State after:
no goals

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (-(-abs z / (1 - t * abs z))) t
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ -1 ≤ t
Tactic:
linarith
State after:
no goals

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
⊢ IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
Tactic:
apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
⊢ ContinuousOn (fun t => abs z / (1 - t * abs z)) (Icc 0 1)

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
⊢ ContinuousOn (fun t => abs z / (1 - t * abs z)) (Icc 0 1)
Tactic:
apply continuousOn_const.div (Continuous.continuousOn (by continuity))
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
⊢ ∀ x ∈ Icc 0 1, 1 - x * abs z ≠ 0

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
⊢ ∀ x ∈ Icc 0 1, 1 - x * abs z ≠ 0
Tactic:
intro t ⟨_,t1⟩
State after:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
t : ℝ
left✝ : 0 ≤ t
t1 : t ≤ 1
⊢ 1 - t * abs z ≠ 0

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
t : ℝ
left✝ : 0 ≤ t
t1 : t ≤ 1
⊢ 1 - t * abs z ≠ 0
Tactic:
exact ne_of_gt (sub_pos.mpr (m1 _ t1))
State after:
no goals

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
dc : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => (1 + ↑t * z).log) (z / (1 + ↑t * z)) t
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
dr : ∀ t ∈ uIcc 0 1, HasDerivAt (fun t => -(1 - t * abs z).log) (abs z / (1 - t * abs z)) t
⊢ Continuous fun t => 1 - t * abs z
Tactic:
continuity
State after:
no goals

State before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
ic : IntervalIntegrable (fun t => z / (1 + ↑t * z)) MeasureTheory.volume 0 1
ir : IntervalIntegrable (fun t => abs z / (1 - t * abs z)) MeasureTheory.volume 0 1
t : ℝ
t0 : 0 ≤ t
t1 : t ≤ 1
⊢ abs 1 - abs (↑t * z) = 1 - t * abs z
Tactic:
simp only [map_one, map_mul, Complex.abs_ofReal, _root_.abs_of_nonneg t0]
State after:
no goals