Theorem: LipschitzOnWith.log (Ray/Hartogs/MaxLog.lean)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ LipschitzOnWith (-b).exp.toNNReal Real.log (Ici b.exp)
Tactic:
rw [lipschitzOnWith_iff_dist_le_mul]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ ∀ x ∈ Ici b.exp, ∀ y ∈ Ici b.exp, dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ ∀ x ∈ Ici b.exp, ∀ y ∈ Ici b.exp, dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y
Tactic:
have half : ∀ x y : ℝ, b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y| := by
  intro x y yb xy
  have yp : y > 0 := lt_of_lt_of_le (Real.exp_pos _) yb
  have xp : x > 0 := lt_of_lt_of_le yp xy
  have yi : y⁻¹ ≤ (-b).exp := by rw [Real.exp_neg]; bound
  rw [abs_of_nonneg (sub_nonneg.mpr xy)]
  rw [abs_of_nonneg (sub_nonneg.mpr ((Real.log_le_log_iff yp xp).mpr xy))]
  rw [← Real.log_div xp.ne' yp.ne']
  rw [Real.log_le_iff_le_exp (div_pos xp yp)]
  trans (y⁻¹ * (x - y)).exp; swap; bound
  have e : y⁻¹ * (x - y) = x / y - 1 := by field_simp [yp.ne']
  rw [e]
  have e1 := Real.add_one_le_exp (x / y - 1)
  simp at e1; exact e1
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
⊢ ∀ x ∈ Ici b.exp, ∀ y ∈ Ici b.exp, dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
⊢ ∀ x ∈ Ici b.exp, ∀ y ∈ Ici b.exp, dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y
Tactic:
intro x xs y ys
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x : ℝ
xs : x ∈ Ici b.exp
y : ℝ
ys : y ∈ Ici b.exp
⊢ dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x : ℝ
xs : x ∈ Ici b.exp
y : ℝ
ys : y ∈ Ici b.exp
⊢ dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y
Tactic:
simp at xs ys ⊢
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ dist x.log y.log ≤ max (-b).exp 0 * dist x y

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ dist x.log y.log ≤ max (-b).exp 0 * dist x y
Tactic:
rw [max_eq_left (Real.exp_pos _).le]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ dist x.log y.log ≤ (-b).exp * dist x y

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ dist x.log y.log ≤ (-b).exp * dist x y
Tactic:
simp_rw [Real.dist_eq]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
by_cases xy : x ≥ y
State after:
case pos
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x ≥ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|

case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : ¬x ≥ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|

State before:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : ¬x ≥ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
simp at xy
State after:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|

State before:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
rw [← neg_sub y x, abs_neg]
State after:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |x.log - y.log| ≤ (-b).exp * |y - x|

State before:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |x.log - y.log| ≤ (-b).exp * |y - x|
Tactic:
rw [← neg_sub y.log x.log, abs_neg]
State after:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |y.log - x.log| ≤ (-b).exp * |y - x|

State before:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |y.log - x.log| ≤ (-b).exp * |y - x|
Tactic:
exact half y x xs xy.le
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
intro x y yb xy
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
have yp : y > 0 := lt_of_lt_of_le (Real.exp_pos _) yb
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
have xp : x > 0 := lt_of_lt_of_le yp xy
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
have yi : y⁻¹ ≤ (-b).exp := by rw [Real.exp_neg]; bound
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
rw [abs_of_nonneg (sub_nonneg.mpr xy)]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ |x.log - y.log| ≤ (-b).exp * (x - y)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ |x.log - y.log| ≤ (-b).exp * (x - y)
Tactic:
rw [abs_of_nonneg (sub_nonneg.mpr ((Real.log_le_log_iff yp xp).mpr xy))]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x.log - y.log ≤ (-b).exp * (x - y)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x.log - y.log ≤ (-b).exp * (x - y)
Tactic:
rw [← Real.log_div xp.ne' yp.ne']
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (x / y).log ≤ (-b).exp * (x - y)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (x / y).log ≤ (-b).exp * (x - y)
Tactic:
rw [Real.log_le_iff_le_exp (div_pos xp yp)]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ ((-b).exp * (x - y)).exp

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ ((-b).exp * (x - y)).exp
Tactic:
trans (y⁻¹ * (x - y)).exp
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp

E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (y⁻¹ * (x - y)).exp ≤ ((-b).exp * (x - y)).exp

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp

E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (y⁻¹ * (x - y)).exp ≤ ((-b).exp * (x - y)).exp
Tactic:
swap
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (y⁻¹ * (x - y)).exp ≤ ((-b).exp * (x - y)).exp

E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (y⁻¹ * (x - y)).exp ≤ ((-b).exp * (x - y)).exp

E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp
Tactic:
bound
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp
Tactic:
have e : y⁻¹ * (x - y) = x / y - 1 := by field_simp [yp.ne']
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
⊢ x / y ≤ (y⁻¹ * (x - y)).exp

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
⊢ x / y ≤ (y⁻¹ * (x - y)).exp
Tactic:
rw [e]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
⊢ x / y ≤ (x / y - 1).exp

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
⊢ x / y ≤ (x / y - 1).exp
Tactic:
have e1 := Real.add_one_le_exp (x / y - 1)
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
e1 : x / y - 1 + 1 ≤ (x / y - 1).exp
⊢ x / y ≤ (x / y - 1).exp

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
e1 : x / y - 1 + 1 ≤ (x / y - 1).exp
⊢ x / y ≤ (x / y - 1).exp
Tactic:
simp at e1
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
e1 : x / y ≤ (x / y - 1).exp
⊢ x / y ≤ (x / y - 1).exp

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
e1 : x / y ≤ (x / y - 1).exp
⊢ x / y ≤ (x / y - 1).exp
Tactic:
exact e1
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
⊢ y⁻¹ ≤ (-b).exp
Tactic:
rw [Real.exp_neg]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
⊢ y⁻¹ ≤ b.exp⁻¹

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
⊢ y⁻¹ ≤ b.exp⁻¹
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ y⁻¹ * (x - y) = x / y - 1
Tactic:
field_simp [yp.ne']
State after:
no goals

State before:
case pos
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x ≥ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
exact half x y ys xy
State after:
no goals