internlm/Lean-Github huggingface dataset:
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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]
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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]
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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⟩
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof state before:
z : ℂ
z1 : abs z < 1
m1 : ∀ t ≤ 1, t * abs z < 1
t : ℝ
m : 0 ≤ t ∧ t ≤ 1
⊢ -1 ≤ t
Tactic:
linarith
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof 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)
Theorem: Complex.abs_log_one_add_le
Proof 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))
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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⟩
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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]
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof 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)
Theorem: Complex.abs_log_one_add_le
Proof 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⟩))
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof 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]
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof 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⟩))
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof 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)
Theorem: Complex.abs_log_one_add_le
Proof 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))
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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⟩
Proof 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
Theorem: Complex.abs_log_one_add_le
Proof 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))
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof 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
Proof state after:
no goals
Theorem: Complex.abs_log_one_add_le
Proof 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]
Proof state after:
no goals
Theorem: Real.abs_log_one_add_le
Proof state before:
x : ℝ
x1 : |x| < 1
⊢ |(1 + x).log| ≤ -(1 - |x|).log
Tactic:
have h := Complex.abs_log_one_add_le (z := x) ?_
Proof state after:
case refine_2
x : ℝ
x1 : |x| < 1
h : Complex.abs (1 + ↑x).log ≤ -(1 - Complex.abs ↑x).log
⊢ |(1 + x).log| ≤ -(1 - |x|).log

case refine_1
x : ℝ
x1 : |x| < 1
⊢ Complex.abs ↑x < 1
Theorem: Real.abs_log_one_add_le
Proof state before:
case refine_2
x : ℝ
x1 : |x| < 1
h : Complex.abs (1 + ↑x).log ≤ -(1 - Complex.abs ↑x).log
⊢ |(1 + x).log| ≤ -(1 - |x|).log
Tactic:
rw [←Complex.ofReal_one, ←Complex.ofReal_add, ←Complex.ofReal_log, Complex.abs_ofReal,
  Complex.abs_ofReal] at h
Proof state after:
case refine_2
x : ℝ
x1 : |x| < 1
h : |(1 + x).log| ≤ -(1 - |x|).log
⊢ |(1 + x).log| ≤ -(1 - |x|).log

case refine_2
x : ℝ
x1 : |x| < 1
h : Complex.abs (↑(1 + x)).log ≤ -(1 - Complex.abs ↑x).log
⊢ 0 ≤ 1 + x
Theorem: Real.abs_log_one_add_le
Proof state before:
case refine_2
x : ℝ
x1 : |x| < 1
h : |(1 + x).log| ≤ -(1 - |x|).log
⊢ |(1 + x).log| ≤ -(1 - |x|).log
Tactic:
exact h
Proof state after:
no goals
Theorem: Real.abs_log_one_add_le
Proof state before:
case refine_2
x : ℝ
x1 : |x| < 1
h : Complex.abs (↑(1 + x)).log ≤ -(1 - Complex.abs ↑x).log
⊢ 0 ≤ 1 + x
Tactic:
simp only [abs_lt] at x1
Proof state after:
case refine_2
x : ℝ
h : Complex.abs (↑(1 + x)).log ≤ -(1 - Complex.abs ↑x).log
x1 : -1 < x ∧ x < 1
⊢ 0 ≤ 1 + x
Theorem: Real.abs_log_one_add_le
Proof state before:
case refine_2
x : ℝ
h : Complex.abs (↑(1 + x)).log ≤ -(1 - Complex.abs ↑x).log
x1 : -1 < x ∧ x < 1
⊢ 0 ≤ 1 + x
Tactic:
linarith
Proof state after:
no goals
Theorem: Real.abs_log_one_add_le
Proof state before:
case refine_1
x : ℝ
x1 : |x| < 1
⊢ Complex.abs ↑x < 1
Tactic:
simpa only [Complex.abs_ofReal]
Proof state after:
no goals
Theorem: Real.neg_log_one_sub_mono
Proof state before:
x y : ℝ
xy : x ≤ y
y1 : y < 1
⊢ 0 < 1 - y
Tactic:
linarith
Proof state after:
no goals
Theorem: Real.neg_log_one_sub_mono
Proof state before:
x y : ℝ
xy : x ≤ y
y1 : y < 1
⊢ 1 - y ≤ 1 - x
Tactic:
linarith
Proof state after:
no goals
Theorem: neg_log_one_sub_le_two
Proof state before:
x : ℝ
x2 : x ≤ 1 / 2
⊢ -(1 - x).log ≤ 2
Tactic:
apply le_trans (Real.neg_log_one_sub_mono x2 (by linarith)) ?_
Proof state after:
x : ℝ
x2 : x ≤ 1 / 2
⊢ -(1 - 1 / 2).log ≤ 2
Theorem: neg_log_one_sub_le_two
Proof state before:
x : ℝ
x2 : x ≤ 1 / 2
⊢ -(1 - 1 / 2).log ≤ 2
Tactic:
rw [neg_le, Real.le_log_iff_exp_le]
Proof state after:
x : ℝ
x2 : x ≤ 1 / 2
⊢ (-2).exp ≤ 1 - 1 / 2

x : ℝ
x2 : x ≤ 1 / 2
⊢ 0 < 1 - 1 / 2
Theorem: neg_log_one_sub_le_two
Proof state before:
x : ℝ
x2 : x ≤ 1 / 2
⊢ 1 / 2 < 1
Tactic:
linarith
Proof state after:
no goals
Theorem: neg_log_one_sub_le_two
Proof state before:
x : ℝ
x2 : x ≤ 1 / 2
⊢ (-2).exp ≤ 1 - 1 / 2
Tactic:
exact (exp_neg_ofNat_lt).le
Proof state after:
no goals
Theorem: neg_log_one_sub_le_two
Proof state before:
x : ℝ
x2 : x ≤ 1 / 2
⊢ 0 < 1 - 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
⊢ -(1 - x).log ≤ c * x
Tactic:
rcases le_min_iff.mp xc with ⟨x1,xc⟩
Proof state after:
case intro
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
⊢ -(1 - x).log ≤ c * x
Theorem: neg_log_one_sub_le_linear
Proof state before:
case intro
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
⊢ -(1 - x).log ≤ c * x
Tactic:
by_cases xz : x = 0
Proof state after:
case pos
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : x = 0
⊢ -(1 - x).log ≤ c * x

case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
⊢ -(1 - x).log ≤ c * x
Theorem: neg_log_one_sub_le_linear
Proof state before:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
⊢ -(1 - x).log ≤ c * x
Tactic:
by_cases xe : x = 1
Proof state after:
case pos
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : x = 1
⊢ -(1 - x).log ≤ c * x

case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
⊢ -(1 - x).log ≤ c * x
Theorem: neg_log_one_sub_le_linear
Proof state before:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
⊢ -(1 - x).log ≤ c * x
Tactic:
replace x1 := Ne.lt_of_le xe x1
Proof state after:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
⊢ -(1 - x).log ≤ c * x
Theorem: neg_log_one_sub_le_linear
Proof state before:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
⊢ -(1 - x).log ≤ c * x
Tactic:
have x0' : 0 < x := (Ne.symm xz).lt_of_le x0
Proof state after:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
⊢ -(1 - x).log ≤ c * x
Theorem: neg_log_one_sub_le_linear
Proof state before:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
⊢ -(1 - x).log ≤ c * x
Tactic:
have c1p : 0 < (c - 1) * 2 := mul_pos (sub_pos.mpr c1) (by norm_num)
Proof state after:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
⊢ -(1 - x).log ≤ c * x
Theorem: neg_log_one_sub_le_linear
Proof state before:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
⊢ -(1 - x).log ≤ c * x
Tactic:
have x1p : 0 < 1 - x := by linarith
Proof state after:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
⊢ -(1 - x).log ≤ c * x
Theorem: neg_log_one_sub_le_linear
Proof state before:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
⊢ -(1 - x).log ≤ c * x
Tactic:
have h := Complex.norm_log_one_add_sub_self_le (z := -x)
  (by simp only [norm_neg, Complex.norm_eq_abs, Complex.abs_ofReal, abs_of_nonneg x0]; exact x1)
Proof state after:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : ‖(1 + -↑x).log - -↑x‖ ≤ ‖-↑x‖ ^ 2 * (1 - ‖-↑x‖)⁻¹ / 2
⊢ -(1 - x).log ≤ c * x
Theorem: neg_log_one_sub_le_linear
Proof state before:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : ‖(1 + -↑x).log - -↑x‖ ≤ ‖-↑x‖ ^ 2 * (1 - ‖-↑x‖)⁻¹ / 2
⊢ -(1 - x).log ≤ c * x
Tactic:
simp only [Complex.norm_eq_abs, Complex.abs_ofReal, ←Complex.ofReal_one, ←Complex.ofReal_add,
  ←Complex.ofReal_log x1p.le, ←Complex.ofReal_sub, abs_le, abs_of_nonneg x0, ←Complex.ofReal_neg,
  ←sub_eq_add_neg, abs_neg] at h
Proof state after:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(x ^ 2 * (1 - x)⁻¹ / 2) ≤ (1 - x).log - -x ∧ (1 - x).log - -x ≤ x ^ 2 * (1 - x)⁻¹ / 2
⊢ -(1 - x).log ≤ c * x
Theorem: neg_log_one_sub_le_linear
Proof state before:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(x ^ 2 * (1 - x)⁻¹ / 2) ≤ (1 - x).log - -x ∧ (1 - x).log - -x ≤ x ^ 2 * (1 - x)⁻¹ / 2
⊢ -(1 - x).log ≤ c * x
Tactic:
replace h : -Real.log (1 - x) ≤ x + x^2 * (1 - x)⁻¹ / 2 := by linarith
Proof state after:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ -(1 - x).log ≤ c * x
Theorem: neg_log_one_sub_le_linear
Proof state before:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ -(1 - x).log ≤ c * x
Tactic:
apply le_trans h
Proof state after:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ x + x ^ 2 * (1 - x)⁻¹ / 2 ≤ c * x
Theorem: neg_log_one_sub_le_linear
Proof state before:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ x + x ^ 2 * (1 - x)⁻¹ / 2 ≤ c * x
Tactic:
rw [pow_two, mul_assoc, mul_div_assoc, ←mul_one_add, mul_comm x _]
Proof state after:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ (1 + x * (1 - x)⁻¹ / 2) * x ≤ c * x