Theorem: monotone_maxLog (Ray/Hartogs/MaxLog.lean)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Monotone fun x => maxLog b x
Tactic:
simp_rw [maxLog]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Monotone fun x => (max b.exp x).log

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Monotone fun x => (max b.exp x).log
Tactic:
intro x y xy
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ (fun x => (max b.exp x).log) x ≤ (fun x => (max b.exp x).log) y

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ (fun x => (max b.exp x).log) x ≤ (fun x => (max b.exp x).log) y
Tactic:
simp only [ge_iff_le]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ (max b.exp x).log ≤ (max b.exp y).log

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ (max b.exp x).log ≤ (max b.exp y).log
Tactic:
rw [Real.log_le_log_iff max_exp_pos max_exp_pos]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ max b.exp x ≤ max b.exp y

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ max b.exp x ≤ max b.exp y
Tactic:
apply max_le_max (le_refl _) xy
State after:
no goals