a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d r : ℝ
h : -1 < r
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => x ^ r) volume 0 c
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d r : ℝ
h : -1 < r
⊢ IntervalIntegrable (fun x => x ^ r) volume a b
suffices ∀ c : ℝ, IntervalIntegrable (fun x => x ^ r) volume 0 c by
  exact IntervalIntegrable.trans (this a).symm (this b)
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => x ^ r) volume 0 c
intro c
case inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c

case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c
rcases le_total 0 c with (hc | hc)
no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), IntervalIntegrable (fun x => x ^ r) volume 0 c
⊢ IntervalIntegrable (fun x => x ^ r) volume a b
exact IntervalIntegrable.trans (this a).symm (this b)
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d r : ℝ
h : -1 < r
⊢ ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
intro c hc
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun x => x ^ r) (Set.Ioc 0 c)
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c
rw [intervalIntegrable_iff, uIoc_of_le hc]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ IntegrableOn (fun x => x ^ r) (Set.Ioc 0 c)
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun x => x ^ r) (Set.Ioc 0 c)
have hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun x : ℝ => x ^ (r + 1) / (r + 1)) (x ^ r) x := by
  intro x hx
  convert (Real.hasDerivAt_rpow_const (p := r + 1) (Or.inl hx.1.ne')).div_const (r + 1) using 1
  field_simp [(by linarith : r + 1 ≠ 0)]; ring
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ∀ (x : ℝ), x ∈ Set.Ioo 0 c → 0 ≤ x ^ r

a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ContinuousOn (fun x => x ^ (r + 1) / (r + 1)) (Set.Icc 0 c)
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ IntegrableOn (fun x => x ^ r) (Set.Ioc 0 c)
apply integrableOn_deriv_of_nonneg _ hderiv
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
intro x hx
case h.e'_7
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ x ^ r = (r + 1) * x ^ (r + 1 - 1) / (r + 1)
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
convert (Real.hasDerivAt_rpow_const (p := r + 1) (Or.inl hx.1.ne')).div_const (r + 1) using 1
case h.e'_7
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ x ^ r * (r + 1) = (r + 1) * x ^ r
case h.e'_7
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ x ^ r = (r + 1) * x ^ (r + 1 - 1) / (r + 1)
field_simp [(by linarith : r + 1 ≠ 0)]
no goals
case h.e'_7
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ x ^ r * (r + 1) = (r + 1) * x ^ r
ring
no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ r + 1 ≠ 0
linarith
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ 0 ≤ x ^ r
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ∀ (x : ℝ), x ∈ Set.Ioo 0 c → 0 ≤ x ^ r
intro x hx
no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ 0 ≤ x ^ r
apply rpow_nonneg_of_nonneg hx.1.le
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ∀ (x : ℝ), x ∈ Set.Icc 0 c → id x ≠ 0 ∨ 0 ≤ r + 1
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ContinuousOn (fun x => x ^ (r + 1) / (r + 1)) (Set.Icc 0 c)
refine' (continuousOn_id.rpow_const _).div_const _
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
a✝ : x ∈ Set.Icc 0 c
⊢ id x ≠ 0 ∨ 0 ≤ r + 1
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ∀ (x : ℝ), x ∈ Set.Icc 0 c → id x ≠ 0 ∨ 0 ≤ r + 1
intro x _
case h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
a✝ : x ∈ Set.Icc 0 c
⊢ 0 ≤ r + 1
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
a✝ : x ∈ Set.Icc 0 c
⊢ id x ≠ 0 ∨ 0 ≤ r + 1
right
no goals
case h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ (x : ℝ), x ∈ Set.Ioo 0 c → HasDerivAt (fun x => x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
a✝ : x ∈ Set.Icc 0 c
⊢ 0 ≤ r + 1
linarith
no goals
case inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c
exact this c hc
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x => (-x) ^ r) volume 0 (-c)
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c
rw [IntervalIntegrable.iff_comp_neg, neg_zero]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntervalIntegrable (cos (r * π) • fun x => x ^ r) volume 0 (-c)
⊢ IntervalIntegrable (fun x => (-x) ^ r) volume 0 (-c)
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x => (-x) ^ r) volume 0 (-c)
have m := (this (-c) (by linarith)).smul (cos (r * π))
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c))
⊢ IntegrableOn (fun x => (-x) ^ r) (Ι 0 (-c))
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntervalIntegrable (cos (r * π) • fun x => x ^ r) volume 0 (-c)
⊢ IntervalIntegrable (fun x => (-x) ^ r) volume 0 (-c)
rw [intervalIntegrable_iff] at m ⊢
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c))
⊢ EqOn (cos (r * π) • fun x => x ^ r) (fun x => (-x) ^ r) (Ι 0 (-c))
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c))
⊢ IntegrableOn (fun x => (-x) ^ r) (Ι 0 (-c))
refine' m.congr_fun _ measurableSet_Ioc
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c))
x : ℝ
hx : x ∈ Ι 0 (-c)
⊢ (cos (r * π) • fun x => x ^ r) x = (fun x => (-x) ^ r) x
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c))
⊢ EqOn (cos (r * π) • fun x => x ^ r) (fun x => (-x) ^ r) (Ι 0 (-c))
intro x hx
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
⊢ (cos (r * π) • fun x => x ^ r) x = (fun x => (-x) ^ r) x
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c))
x : ℝ
hx : x ∈ Ι 0 (-c)
⊢ (cos (r * π) • fun x => x ^ r) x = (fun x => (-x) ^ r) x
rw [uIoc_of_le (by linarith : 0 ≤ -c)] at hx
no goals
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
⊢ (cos (r * π) • fun x => x ^ r) x = (fun x => (-x) ^ r) x
simp only [Pi.smul_apply, Algebra.id.smul_eq_mul, log_neg_eq_log, mul_comm,
  rpow_def_of_pos hx.1, rpow_def_of_neg (by linarith [hx.1] : -x < 0)]
no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ 0 ≤ -c
linarith
no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c))
x : ℝ
hx : x ∈ Ι 0 (-c)
⊢ 0 ≤ -c
linarith
no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x => x ^ r) (Ι 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
⊢ -x < 0
linarith [hx.1]