case pos
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re ∨ ¬0 ∈ [[a, b]]
h2 : ¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b

case neg
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re ∨ ¬0 ∈ [[a, b]]
h2 : ¬¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re ∨ ¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
by_cases h2 : (0 : ℝ) ∉ [[a, b]]
case neg
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
case neg
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re ∨ ¬0 ∈ [[a, b]]
h2 : ¬¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
rw [eq_false h2, or_false_iff] at h
case neg.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 < r.re
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b

case neg.inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
case neg
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
rcases lt_or_eq_of_le h with (h' | h')
case neg.inr.refine'_1
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ AEStronglyMeasurable (fun x => ↑x ^ r) (Measure.restrict μ (Ι a b))

case neg.inr.refine'_2
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ IntervalIntegrable (fun t => ‖↑t ^ r‖) μ a b
case neg.inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
refine' (IntervalIntegrable.intervalIntegrable_norm_iff _).mp _
case neg.inr.refine'_2
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
this : ∀ (c : ℝ), IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
⊢ IntervalIntegrable (fun t => ‖↑t ^ r‖) μ a b

case this
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
case neg.inr.refine'_2
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ IntervalIntegrable (fun t => ‖↑t ^ r‖) μ a b
suffices : ∀ c : ℝ, IntervalIntegrable (fun x : ℝ => ‖(x:ℂ) ^ r‖) μ 0 c
case this
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
case neg.inr.refine'_2
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
this : ∀ (c : ℝ), IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
⊢ IntervalIntegrable (fun t => ‖↑t ^ r‖) μ a b

case this
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
exact (this a).symm.trans (this b)
case this
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
case this
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
intro c
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c

case this.inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
case this
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
rcases le_or_lt 0 c with (hc | hc)
case pos
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re ∨ ¬0 ∈ [[a, b]]
h2 : ¬0 ∈ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ ContinuousAt (fun x => ↑x ^ r) x
case pos
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re ∨ ¬0 ∈ [[a, b]]
h2 : ¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
refine' (ContinuousAt.continuousOn fun x hx => _).intervalIntegrable
no goals
case pos
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re ∨ ¬0 ∈ [[a, b]]
h2 : ¬0 ∈ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ ContinuousAt (fun x => ↑x ^ r) x
exact Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_mem_of_not_mem hx h2)
no goals
case neg.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 < r.re
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
exact (Complex.continuous_ofReal_cpow_const h').intervalIntegrable _ _
case neg.inr.refine'_1
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ ContinuousOn (fun x => ↑x ^ r) ({0}ᶜ)
case neg.inr.refine'_1
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ AEStronglyMeasurable (fun x => ↑x ^ r) (Measure.restrict μ (Ι a b))
refine' (measurable_of_continuousOn_compl_singleton (0 : ℝ) _).aestronglyMeasurable
no goals
case neg.inr.refine'_1
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ ContinuousOn (fun x => ↑x ^ r) ({0}ᶜ)
exact ContinuousAt.continuousOn fun x hx =>
  Complex.continuousAt_ofReal_cpow_const x r (Or.inr hx)
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntervalIntegrable (fun x => 1) μ 0 c
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
have : IntervalIntegrable (fun _ => 1 : ℝ → ℝ) μ 0 c := intervalIntegrable_const
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntegrableOn (fun x => 1) (Set.Ioc 0 c)
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioc 0 c)
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntervalIntegrable (fun x => 1) μ 0 c
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
rw [intervalIntegrable_iff_integrable_Ioc_of_le hc] at this ⊢
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntegrableOn (fun x => 1) (Set.Ioc 0 c)
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 1 = ‖↑x ^ r‖
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntegrableOn (fun x => 1) (Set.Ioc 0 c)
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioc 0 c)
refine' IntegrableOn.congr_fun this (fun x hx => _) measurableSet_Ioc
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntegrableOn (fun x => 1) (Set.Ioc 0 c)
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 1 = ‖↑x ^ r‖
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntegrableOn (fun x => 1) (Set.Ioc 0 c)
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 1 = ‖↑x ^ r‖
dsimp only
no goals
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntegrableOn (fun x => 1) (Set.Ioc 0 c)
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 1 = ‖↑x ^ r‖
rw [Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos hx.1, ← h', rpow_zero]
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ c 0
case this.inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
apply IntervalIntegrable.symm
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioc c 0)
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntervalIntegrable (fun x => ‖↑x ^ r‖) μ c 0
rw [intervalIntegrable_iff_integrable_Ioc_of_le hc.le]
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioc c 0)
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioc c 0)
have : Ioc c 0 = Ioo c 0 ∪ {(0 : ℝ)} := by
  rw [← Ioo_union_Icc_eq_Ioc hc (le_refl 0), ← Icc_def]
  simp_rw [← le_antisymm_iff, setOf_eq_eq_singleton']
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) {0} ∧ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioo c 0)
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioc c 0)
rw [this, integrableOn_union, and_comm]
case this.inr.h.left
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) {0}

case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioo c 0)
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) {0} ∧ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioo c 0)
constructor
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ Set.Ioo c 0 ∪ {x | 0 ≤ x ∧ x ≤ 0} = Set.Ioo c 0 ∪ {0}
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
rw [← Ioo_union_Icc_eq_Ioc hc (le_refl 0), ← Icc_def]
no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ Set.Ioo c 0 ∪ {x | 0 ≤ x ∧ x ≤ 0} = Set.Ioo c 0 ∪ {0}
simp_rw [← le_antisymm_iff, setOf_eq_eq_singleton']
case this.inr.h.left
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
⊢ ↑↑μ {0} < ⊤
case this.inr.h.left
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) {0}
refine' integrableOn_singleton_iff.mpr (Or.inr _)
no goals
case this.inr.h.left
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
⊢ ↑↑μ {0} < ⊤
exact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact
  isCompact_singleton
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this✝ : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
this : ∀ (x : ℝ), x ∈ Set.Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioo c 0)
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioo c 0)
have : ∀ x : ℝ, x ∈ Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖(x : ℂ) ^ r‖ := by
  intro x hx
  rw [Complex.ofReal_cpow_of_nonpos hx.2.le, norm_mul, ← Complex.ofReal_neg,
    Complex.norm_eq_abs (_ ^ _), Complex.abs_cpow_eq_rpow_re_of_pos (neg_pos.mpr hx.2), ← h',
    rpow_zero, one_mul]
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this✝ : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
this : ∀ (x : ℝ), x ∈ Set.Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ IntegrableOn (fun x => ‖Complex.exp (↑π * Complex.I * r)‖) (Set.Ioo c 0)
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this✝ : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
this : ∀ (x : ℝ), x ∈ Set.Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ IntegrableOn (fun x => ‖↑x ^ r‖) (Set.Ioo c 0)
refine' IntegrableOn.congr_fun _ this measurableSet_Ioo
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this✝ : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
this : ∀ (x : ℝ), x ∈ Set.Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = 0 ∨ ↑↑μ (Set.Ioo c 0) < ⊤
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this✝ : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
this : ∀ (x : ℝ), x ∈ Set.Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ IntegrableOn (fun x => ‖Complex.exp (↑π * Complex.I * r)‖) (Set.Ioo c 0)
rw [integrableOn_const]
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this✝ : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
this : ∀ (x : ℝ), x ∈ Set.Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ ↑↑μ (Set.Icc c 0) < ⊤
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this✝ : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
this : ∀ (x : ℝ), x ∈ Set.Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = 0 ∨ ↑↑μ (Set.Ioo c 0) < ⊤
refine' Or.inr ((measure_mono Set.Ioo_subset_Icc_self).trans_lt _)
no goals
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this✝ : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
this : ∀ (x : ℝ), x ∈ Set.Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ ↑↑μ (Set.Icc c 0) < ⊤
exact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact isCompact_Icc
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
x : ℝ
hx : x ∈ Set.Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
⊢ ∀ (x : ℝ), x ∈ Set.Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
intro x hx
no goals
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : MeasureTheory.Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : Set.Ioc c 0 = Set.Ioo c 0 ∪ {0}
x : ℝ
hx : x ∈ Set.Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
rw [Complex.ofReal_cpow_of_nonpos hx.2.le, norm_mul, ← Complex.ofReal_neg,
  Complex.norm_eq_abs (_ ^ _), Complex.abs_cpow_eq_rpow_re_of_pos (neg_pos.mpr hx.2), ← h',
  rpow_zero, one_mul]