s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
hx₀ : 0 ≤ log x
⊢ ‖log x ^ r‖ ≤ 1 * ‖log x ^ r'‖
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
⊢ ‖log x ^ r‖ ≤ 1 * ‖log x ^ r'‖
have hx₀ : 0 ≤ log x := zero_le_one.trans hx
no goals
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 1 ≤ log x
hx₀ : 0 ≤ log x
⊢ ‖log x ^ r‖ ≤ 1 * ‖log x ^ r'‖
simp [norm_eq_abs, abs_rpow_of_nonneg, abs_rpow_of_nonneg hx₀,
  rpow_le_rpow_of_exponent_le (hx.trans (le_abs_self _))]
no goals
s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 0 ≤ x
⊢ (fun x => (x ^ (s / r')) ^ r') x = (fun x => x ^ s) x
simp only [← rpow_mul hx, div_mul_cancel _ hr.ne']