E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
⊢ IntegrableOn (fun x => (abs p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
⊢ IntegrableOn (fun x => (abs p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
let S := Ioi (0 : ℝ)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
⊢ IntegrableOn (fun x => (abs p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
⊢ IntegrableOn (fun x => (abs p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
have a1 : ∀ x : ℝ, x ∈ S → HasDerivWithinAt (fun t : ℝ => t ^ p) (p * x ^ (p - 1)) S x :=
  fun x hx => (hasDerivAt_rpow_const (Or.inl (mem_Ioi.mp hx).ne')).hasDerivWithinAt
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f ((fun t => t ^ p) '' Ioi 0) ↔ IntegrableOn (fun x => abs (p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0)
⊢ IntegrableOn (fun x => (abs p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
⊢ IntegrableOn (fun x => (abs p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
have := integrableOn_image_iff_integrableOn_abs_deriv_smul measurableSet_Ioi a1 a2 f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f S ↔ IntegrableOn (fun x => abs (p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0)
⊢ IntegrableOn (fun x => (abs p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f ((fun t => t ^ p) '' Ioi 0) ↔ IntegrableOn (fun x => abs (p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0)
⊢ IntegrableOn (fun x => (abs p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
rw [a3] at this
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f S ↔ IntegrableOn (fun x => abs (p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0)
⊢ IntegrableOn (fun x => (abs p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔
    IntegrableOn (fun x => abs (p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f S ↔ IntegrableOn (fun x => abs (p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0)
⊢ IntegrableOn (fun x => (abs p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
rw [this]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f S ↔ IntegrableOn (fun x => abs (p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
⊢ (abs p * x ^ (p - 1)) • f (x ^ p) = abs (p * x ^ (p - 1)) • f (x ^ p)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f S ↔ IntegrableOn (fun x => abs (p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0)
⊢ IntegrableOn (fun x => (abs p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔
    IntegrableOn (fun x => abs (p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0)
refine' integrableOn_congr_fun (fun x hx => _) measurableSet_Ioi
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f S ↔ IntegrableOn (fun x => abs (p * x ^ (p - 1)) • f (x ^ p)) (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
⊢ (abs p * x ^ (p - 1)) • f (x ^ p) = abs (p * x ^ (p - 1)) • f (x ^ p)
simp_rw [abs_mul, abs_of_nonneg (rpow_nonneg_of_nonneg (le_of_lt hx) _)]
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
⊢ InjOn (fun x => x ^ p) S

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p > 0
⊢ InjOn (fun x => x ^ p) S
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
⊢ InjOn (fun x => x ^ p) S
rcases lt_or_gt_of_ne hp with (h | h)
no goals
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p > 0
⊢ InjOn (fun x => x ^ p) S
exact StrictMonoOn.injOn fun x hx y _hy hxy => rpow_lt_rpow (mem_Ioi.mp hx).le hxy h
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
⊢ StrictAntiOn (fun x => x ^ p) S
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
⊢ InjOn (fun x => x ^ p) S
apply StrictAntiOn.injOn
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ (fun x => x ^ p) y < (fun x => x ^ p) x
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
⊢ StrictAntiOn (fun x => x ^ p) S
intro x hx y hy hxy
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ x ^ (-p) < y ^ (-p)
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ (fun x => x ^ p) y < (fun x => x ^ p) x
rw [← inv_lt_inv (rpow_pos_of_pos hx p) (rpow_pos_of_pos hy p), ← rpow_neg (le_of_lt hx), ←
  rpow_neg (le_of_lt hy)]
no goals
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ x ^ (-p) < y ^ (-p)
exact rpow_lt_rpow (le_of_lt hx) hxy (neg_pos.mpr h)
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ x ∈ (fun t => t ^ p) '' S ↔ x ∈ S
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
⊢ (fun t => t ^ p) '' S = S
ext1 x
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ (∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x) ↔ x ∈ S
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ x ∈ (fun t => t ^ p) '' S ↔ x ∈ S
rw [mem_image]
case h.mp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ (∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x) → x ∈ S

case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ x ∈ S → ∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ (∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x) ↔ x ∈ S
constructor
case h.mp.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
y : ℝ
hy : y ∈ S
⊢ y ^ p ∈ S
case h.mp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ (∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x) → x ∈ S
rintro ⟨y, hy, rfl⟩
no goals
case h.mp.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
y : ℝ
hy : y ∈ S
⊢ y ^ p ∈ S
exact rpow_pos_of_pos hy p
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ ∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ x ∈ S → ∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x
intro hx
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ (x ^ (1 / p)) ^ p = x
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ ∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x
refine' ⟨x ^ (1 / p), rpow_pos_of_pos hx _, _⟩
no goals
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ (x ^ (1 / p)) ^ p = x
rw [← rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one]