Theorem: neg_log_one_sub_le_linear (Ray/Dynamics/Multibrot/Log1p.lean)

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⟩
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

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
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

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
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

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
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

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
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

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)
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

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
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

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)
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

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
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

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
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

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
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

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 _]
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

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 * (1 - x)⁻¹ / 2) * x ≤ c * x
Tactic:
apply mul_le_mul_of_nonneg_right _ x0
State after:
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 ≤ c

State before:
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 ≤ c
Tactic:
nth_rw 1 [←inv_inv x]
State after:
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 ≤ c

State before:
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 ≤ c
Tactic:
rw [←mul_inv, mul_sub, mul_one, inv_mul_cancel xz]
State after:
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)⁻¹ / 2 ≤ c

State before:
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)⁻¹ / 2 ≤ c
Tactic:
rw [add_comm, ←le_sub_iff_add_le, div_le_iff (by norm_num)]
State after:
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⁻¹ - 1)⁻¹ ≤ (c - 1) * 2

State before:
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⁻¹ - 1)⁻¹ ≤ (c - 1) * 2
Tactic:
apply inv_le_of_inv_le c1p
State after:
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
⊢ ((c - 1) * 2)⁻¹ ≤ x⁻¹ - 1

State before:
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
⊢ ((c - 1) * 2)⁻¹ ≤ x⁻¹ - 1
Tactic:
rw [le_sub_iff_add_le, le_inv (add_pos (inv_pos.mpr c1p) (by norm_num)) x0']
State after:
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 ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹

State before:
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 ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
exact xc
State after:
no goals

State before:
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
Tactic:
simp only [xz, sub_zero, Real.log_one, neg_zero, mul_zero, le_refl]
State after:
no goals

State before:
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
Tactic:
simp only [xe, sub_self, Real.log_zero, neg_zero, mul_one]
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
⊢ 0 ≤ c

State before:
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
⊢ 0 ≤ c
Tactic:
linarith
State after:
no goals

State before:
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
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
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
⊢ 0 < 1 - x
Tactic:
linarith
State after:
no goals

State before:
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
⊢ ‖-↑x‖ < 1
Tactic:
simp only [norm_neg, Complex.norm_eq_abs, Complex.abs_ofReal, abs_of_nonneg x0]
State after:
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
⊢ x < 1

State before:
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
⊢ x < 1
Tactic:
exact x1
State after:
no goals

State before:
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 ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
Tactic:
linarith
State after:
no goals

State before:
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
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
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
⊢ 0 < 1
Tactic:
norm_num
State after:
no goals