a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : -1 < r.re
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : -1 < r.re
⊢ 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.re
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.re
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.re
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.re
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.re
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.re
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.re
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.re
⊢ ∀ (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.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun t => ‖↑t ^ r‖) volume 0 c

a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ AEStronglyMeasurable (fun x => ↑x ^ r) (Measure.restrict volume (Ι 0 c))
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
rw [← IntervalIntegrable.intervalIntegrable_norm_iff]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun t => ‖↑t ^ r‖) (Ι 0 c)
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun t => ‖↑t ^ r‖) volume 0 c
rw [intervalIntegrable_iff]
case h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn ?f (Ι 0 c)

case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ EqOn ?f (fun t => ‖↑t ^ r‖) (Ι 0 c)

case hs
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ MeasurableSet (Ι 0 c)

case f
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ ℝ → ℝ
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun t => ‖↑t ^ r‖) (Ι 0 c)
apply IntegrableOn.congr_fun
case h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable ?m.1667833 volume 0 c

a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ ℝ → ℝ
case h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn ?f (Ι 0 c)
rw [← intervalIntegrable_iff]
no goals
case h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable ?m.1667833 volume 0 c

a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ ℝ → ℝ
exact intervalIntegral.intervalIntegrable_rpow' h
case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ (fun x => x ^ r.re) x = (fun t => ‖↑t ^ r‖) x
case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ EqOn (fun x => x ^ r.re) (fun t => ‖↑t ^ r‖) (Ι 0 c)
intro x hx
case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ (fun x => x ^ r.re) x = (fun t => ‖↑t ^ r‖) x
case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ (fun x => x ^ r.re) x = (fun t => ‖↑t ^ r‖) x
rw [uIoc_of_le hc] at hx
case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ x ^ r.re = ‖↑x ^ r‖
case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ (fun x => x ^ r.re) x = (fun t => ‖↑t ^ r‖) x
dsimp only
no goals
case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ x ^ r.re = ‖↑x ^ r‖
rw [Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos hx.1]
no goals
case hs
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ MeasurableSet (Ι 0 c)
exact measurableSet_uIoc
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ ContinuousOn (fun x => ↑x ^ r) (Ι 0 c)
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ AEStronglyMeasurable (fun x => ↑x ^ r) (Measure.restrict volume (Ι 0 c))
refine' ContinuousOn.aestronglyMeasurable _ measurableSet_uIoc
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ ContinuousAt (fun x => ↑x ^ r) x
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ ContinuousOn (fun x => ↑x ^ r) (Ι 0 c)
refine' ContinuousAt.continuousOn fun x hx => _
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ ContinuousAt (fun x => ↑x ^ r) x
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ ContinuousAt (fun x => ↑x ^ r) x
rw [uIoc_of_le hc] at hx
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 0 < (↑x).re
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ ContinuousAt (fun x => ↑x ^ r) x
refine' (continuousAt_cpow_const (Or.inl _)).comp Complex.continuous_ofReal.continuousAt
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 0 < x
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 0 < (↑x).re
rw [Complex.ofReal_re]
no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 0 < x
exact hx.1
no goals
case inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
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.re
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.re
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.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntervalIntegrable (fun x => Complex.exp (↑π * Complex.I * r) * ↑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.re
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)).const_mul (Complex.exp (π * Complex.I * r))
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
⊢ IntegrableOn (fun x => ↑(-x) ^ r) (Set.Ioc 0 (-c))
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntervalIntegrable (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) volume 0 (-c)
⊢ IntervalIntegrable (fun x => ↑(-x) ^ r) volume 0 (-c)
rw [intervalIntegrable_iff, uIoc_of_le (by linarith : 0 ≤ -c)] at m ⊢
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
⊢ Complex.exp (↑π * Complex.I * r) * ↑x ^ r = ↑(-x) ^ r
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
⊢ IntegrableOn (fun x => ↑(-x) ^ r) (Set.Ioc 0 (-c))
refine' m.congr_fun (fun x hx => _) measurableSet_Ioc
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
⊢ Complex.exp (↑π * Complex.I * r) * ↑x ^ r = ↑(-x) ^ r
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
⊢ Complex.exp (↑π * Complex.I * r) * ↑x ^ r = ↑(-x) ^ r
dsimp only
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this✝ : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
this : -x ≤ 0
⊢ Complex.exp (↑π * Complex.I * r) * ↑x ^ r = ↑(-x) ^ r
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
⊢ Complex.exp (↑π * Complex.I * r) * ↑x ^ r = ↑(-x) ^ r
have : -x ≤ 0 := by linarith [hx.1]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this✝ : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
this : -x ≤ 0
⊢ ↑x ^ r * Complex.exp (↑π * Complex.I * r) = (-↑(-x)) ^ r * Complex.exp (↑π * Complex.I * r)
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this✝ : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
this : -x ≤ 0
⊢ Complex.exp (↑π * Complex.I * r) * ↑x ^ r = ↑(-x) ^ r
rw [Complex.ofReal_cpow_of_nonpos this, mul_comm]
no goals
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this✝ : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
this : -x ≤ 0
⊢ ↑x ^ r * Complex.exp (↑π * Complex.I * r) = (-↑(-x)) ^ r * Complex.exp (↑π * Complex.I * r)
simp
no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
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.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
⊢ 0 ≤ -c
linarith
no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x => Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Set.Ioc 0 (-c))
x : ℝ
hx : x ∈ Set.Ioc 0 (-c)
⊢ -x ≤ 0
linarith [hx.1]