[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d r : ℝ
h : -1 < r
⊢ IntervalIntegrable (fun x => x ^ r) volume a b
[PROOFSTEP]
suffices ∀ c : ℝ, IntervalIntegrable (fun x => x ^ r) volume 0 c by
  exact IntervalIntegrable.trans (this a).symm (this b)
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
exact IntervalIntegrable.trans (this a).symm (this b)
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d r : ℝ
h : -1 < r
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => x ^ r) volume 0 c
[PROOFSTEP]
have : ∀ c : ℝ, 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c :=
  by
  intro c hc
  rw [intervalIntegrable_iff, uIoc_of_le hc]
  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
  apply integrableOn_deriv_of_nonneg _ hderiv
  · intro x hx; apply rpow_nonneg_of_nonneg hx.1.le
  · refine' (continuousOn_id.rpow_const _).div_const _; intro x _; right; linarith
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d r : ℝ
h : -1 < r
⊢ ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c
[PROOFSTEP]
intro c hc
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => x ^ r) volume 0 c
[PROOFSTEP]
rw [intervalIntegrable_iff, uIoc_of_le hc]
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun x => x ^ r) (Set.Ioc 0 c)
[PROOFSTEP]
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
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
intro x hx
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
convert (Real.hasDerivAt_rpow_const (p := r + 1) (Or.inl hx.1.ne')).div_const (r + 1) using 1
[GOAL]
case h.e'_7
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
field_simp [(by linarith : r + 1 ≠ 0)]
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioo 0 c
⊢ r + 1 ≠ 0
[PROOFSTEP]
linarith
[GOAL]
case h.e'_7
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
ring
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
apply integrableOn_deriv_of_nonneg _ hderiv
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
intro x hx
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
apply rpow_nonneg_of_nonneg hx.1.le
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
refine' (continuousOn_id.rpow_const _).div_const _
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
intro x _
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
right
[GOAL]
case h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
linarith
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
intro c
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
rcases le_total 0 c with (hc | hc)
[GOAL]
case inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
exact this c hc
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
rw [IntervalIntegrable.iff_comp_neg, neg_zero]
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
have m := (this (-c) (by linarith)).smul (cos (r * π))
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
linarith
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
rw [intervalIntegrable_iff] at m ⊢
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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))
[PROOFSTEP]
refine' m.congr_fun _ measurableSet_Ioc
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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))
[PROOFSTEP]
intro x hx
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
rw [uIoc_of_le (by linarith : 0 ≤ -c)] at hx
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
linarith
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
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)]
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
linarith [hx.1]
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re ∨ ¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
[PROOFSTEP]
by_cases h2 : (0 : ℝ) ∉ [[a, b]]
[GOAL]
case pos
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re ∨ ¬0 ∈ [[a, b]]
h2 : ¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
[PROOFSTEP]
refine' (ContinuousAt.continuousOn fun x hx => _).intervalIntegrable
[GOAL]
case pos
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
exact Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_mem_of_not_mem hx h2)
[GOAL]
case neg
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re ∨ ¬0 ∈ [[a, b]]
h2 : ¬¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
[PROOFSTEP]
rw [eq_false h2, or_false_iff] at h
[GOAL]
case neg
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ r) μ a b
[PROOFSTEP]
rcases lt_or_eq_of_le h with (h' | h')
[GOAL]
case neg.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
exact
  (Complex.continuous_ofReal_cpow_const h').intervalIntegrable _
    _
      -- Now the hard case: re r = 0 and 0 is in the interval.
[GOAL]
case neg.inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
refine' (IntervalIntegrable.intervalIntegrable_norm_iff _).mp _
[GOAL]
case neg.inr.refine'_1
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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))
[PROOFSTEP]
refine' (measurable_of_continuousOn_compl_singleton (0 : ℝ) _).aestronglyMeasurable
[GOAL]
case neg.inr.refine'_1
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : 0 ≤ r.re
h2 : ¬¬0 ∈ [[a, b]]
h' : 0 = r.re
⊢ ContinuousOn (fun x => ↑x ^ r) {0}ᶜ
[PROOFSTEP]
exact
  ContinuousAt.continuousOn fun x hx =>
    Complex.continuousAt_ofReal_cpow_const x r
      (Or.inr hx)
        -- reduce to case of integral over `[0, c]`
[GOAL]
case neg.inr.refine'_2
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
suffices : ∀ c : ℝ, IntervalIntegrable (fun x : ℝ => ‖(x : ℂ) ^ r‖) μ 0 c
[GOAL]
case neg.inr.refine'_2
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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 : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
exact (this a).symm.trans (this b)
[GOAL]
case this
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
intro c
[GOAL]
case this
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
rcases le_or_lt 0 c with (hc | hc)
[GOAL]
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
have : IntervalIntegrable (fun _ => 1 : ℝ → ℝ) μ 0 c := intervalIntegrable_const
[GOAL]
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
rw [intervalIntegrable_iff_integrable_Ioc_of_le hc] at this ⊢
[GOAL]
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
refine' IntegrableOn.congr_fun this (fun x hx => _) measurableSet_Ioc
[GOAL]
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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‖
[PROOFSTEP]
dsimp only
[GOAL]
case this.inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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‖
[PROOFSTEP]
rw [Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos hx.1, ← h', rpow_zero]
[GOAL]
case this.inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
apply IntervalIntegrable.symm
[GOAL]
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
rw [intervalIntegrable_iff_integrable_Ioc_of_le hc.le]
[GOAL]
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
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']
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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}
[PROOFSTEP]
rw [← Ioo_union_Icc_eq_Ioc hc (le_refl 0), ← Icc_def]
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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}
[PROOFSTEP]
simp_rw [← le_antisymm_iff, setOf_eq_eq_singleton']
[GOAL]
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
rw [this, integrableOn_union, and_comm]
[GOAL]
case this.inr.h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
constructor
[GOAL]
case this.inr.h.left
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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}
[PROOFSTEP]
refine' integrableOn_singleton_iff.mpr (Or.inr _)
[GOAL]
case this.inr.h.left
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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} < ⊤
[PROOFSTEP]
exact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact isCompact_singleton
[GOAL]
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
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]
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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‖
[PROOFSTEP]
intro x hx
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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‖
[PROOFSTEP]
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]
[GOAL]
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
refine' IntegrableOn.congr_fun _ this measurableSet_Ioo
[GOAL]
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
rw [integrableOn_const]
[GOAL]
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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) < ⊤
[PROOFSTEP]
refine' Or.inr ((measure_mono Set.Ioo_subset_Icc_self).trans_lt _)
[GOAL]
case this.inr.h.right
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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) < ⊤
[PROOFSTEP]
exact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact isCompact_Icc
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : -1 < r.re
⊢ IntervalIntegrable (fun x => ↑x ^ r) volume a b
[PROOFSTEP]
suffices ∀ c : ℝ, IntervalIntegrable (fun x => (x : ℂ) ^ r) volume 0 c by
  exact IntervalIntegrable.trans (this a).symm (this b)
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
exact IntervalIntegrable.trans (this a).symm (this b)
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : -1 < r.re
⊢ ∀ (c : ℝ), IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
[PROOFSTEP]
have : ∀ c : ℝ, 0 ≤ c → IntervalIntegrable (fun x => (x : ℂ) ^ r) volume 0 c :=
  by
  intro c hc
  rw [← IntervalIntegrable.intervalIntegrable_norm_iff]
  · rw [intervalIntegrable_iff]
    apply IntegrableOn.congr_fun
    · rw [← intervalIntegrable_iff]; exact intervalIntegral.intervalIntegrable_rpow' h
    · intro x hx
      rw [uIoc_of_le hc] at hx
      dsimp only
      rw [Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos hx.1]
    · exact measurableSet_uIoc
  · refine' ContinuousOn.aestronglyMeasurable _ measurableSet_uIoc
    refine' ContinuousAt.continuousOn fun x hx => _
    rw [uIoc_of_le hc] at hx
    refine' (continuousAt_cpow_const (Or.inl _)).comp Complex.continuous_ofReal.continuousAt
    rw [Complex.ofReal_re]
    exact hx.1
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
r : ℂ
h : -1 < r.re
⊢ ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
[PROOFSTEP]
intro c hc
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
[PROOFSTEP]
rw [← IntervalIntegrable.intervalIntegrable_norm_iff]
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun t => ‖↑t ^ r‖) volume 0 c
[PROOFSTEP]
rw [intervalIntegrable_iff]
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun t => ‖↑t ^ r‖) (Ι 0 c)
[PROOFSTEP]
apply IntegrableOn.congr_fun
[GOAL]
case h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn ?f (Ι 0 c)
[PROOFSTEP]
rw [← intervalIntegrable_iff]
[GOAL]
case h
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable ?m.22126 volume 0 c
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ ℝ → ℝ
[PROOFSTEP]
exact intervalIntegral.intervalIntegrable_rpow' h
[GOAL]
case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
intro x hx
[GOAL]
case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
rw [uIoc_of_le hc] at hx
[GOAL]
case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
dsimp only
[GOAL]
case hst
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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‖
[PROOFSTEP]
rw [Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos hx.1]
[GOAL]
case hs
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ MeasurableSet (Ι 0 c)
[PROOFSTEP]
exact measurableSet_uIoc
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ AEStronglyMeasurable (fun x => ↑x ^ r) (Measure.restrict volume (Ι 0 c))
[PROOFSTEP]
refine' ContinuousOn.aestronglyMeasurable _ measurableSet_uIoc
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ ContinuousOn (fun x => ↑x ^ r) (Ι 0 c)
[PROOFSTEP]
refine' ContinuousAt.continuousOn fun x hx => _
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
rw [uIoc_of_le hc] at hx
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
refine' (continuousAt_cpow_const (Or.inl _)).comp Complex.continuous_ofReal.continuousAt
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 0 < (↑x).re
[PROOFSTEP]
rw [Complex.ofReal_re]
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c✝ d : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Set.Ioc 0 c
⊢ 0 < x
[PROOFSTEP]
exact hx.1
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
intro c
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
rcases le_total 0 c with (hc | hc)
[GOAL]
case inl
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
exact this c hc
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
rw [IntervalIntegrable.iff_comp_neg, neg_zero]
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
have m := (this (-c) (by linarith)).const_mul (Complex.exp (π * Complex.I * r))
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
linarith
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
rw [intervalIntegrable_iff, uIoc_of_le (by linarith : 0 ≤ -c)] at m ⊢
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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) (Ι 0 (-c))
⊢ 0 ≤ -c
[PROOFSTEP]
linarith
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
linarith
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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))
[PROOFSTEP]
refine' m.congr_fun (fun x hx => _) measurableSet_Ioc
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
dsimp only
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
have : -x ≤ 0 := by linarith [hx.1]
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
linarith [hx.1]
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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
[PROOFSTEP]
rw [Complex.ofReal_cpow_of_nonpos this, mul_comm]
[GOAL]
case inr
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : 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)
[PROOFSTEP]
simp
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
h : ∀ (x : ℝ), x ∈ [[a, b]] → f x ≠ 0
hf : ContinuousOn f [[a, b]]
⊢ IntervalIntegrable (fun x => (f x)⁻¹) μ a b
[PROOFSTEP]
simpa only [one_div] using intervalIntegrable_one_div h hf
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
⊢ IntervalIntegrable (fun x => ↑1 / (1 + x ^ 2)) μ a b
[PROOFSTEP]
refine' (continuous_const.div _ fun x => _).intervalIntegrable a b
[GOAL]
case refine'_1
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
⊢ Continuous fun x => 1 + x ^ 2
[PROOFSTEP]
continuity
[GOAL]
case refine'_2
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d x : ℝ
⊢ 1 + x ^ 2 ≠ 0
[PROOFSTEP]
nlinarith
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
⊢ IntervalIntegrable (fun x => (1 + x ^ 2)⁻¹) μ a b
[PROOFSTEP]
field_simp
[GOAL]
a b : ℝ
n : ℕ
f : ℝ → ℝ
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
c d : ℝ
⊢ IntervalIntegrable (fun x => 1 / (1 + x ^ 2)) μ a b
[PROOFSTEP]
exact_mod_cast intervalIntegrable_one_div_one_add_sq
[GOAL]
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = (↑b ^ (r + 1) - ↑a ^ (r + 1)) / (r + 1)
[PROOFSTEP]
rw [sub_div]
[GOAL]
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
[PROOFSTEP]
have hr : r + 1 ≠ 0 := by
  cases' h with h h
  · apply_fun Complex.re
    rw [Complex.add_re, Complex.one_re, Complex.zero_re, Ne.def, add_eq_zero_iff_eq_neg]
    exact h.ne'
  · rw [Ne.def, ← add_eq_zero_iff_eq_neg] at h ; exact h.1
[GOAL]
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ r + 1 ≠ 0
[PROOFSTEP]
cases' h with h h
[GOAL]
case inl
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re
⊢ r + 1 ≠ 0
[PROOFSTEP]
apply_fun Complex.re
[GOAL]
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re
⊢ (r + 1).re ≠ 0.re
[PROOFSTEP]
rw [Complex.add_re, Complex.one_re, Complex.zero_re, Ne.def, add_eq_zero_iff_eq_neg]
[GOAL]
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re
⊢ ¬r.re = -1
[PROOFSTEP]
exact h.ne'
[GOAL]
case inr
a b : ℝ
n : ℕ
r : ℂ
h : r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ r + 1 ≠ 0
[PROOFSTEP]
rw [Ne.def, ← add_eq_zero_iff_eq_neg] at h
[GOAL]
case inr
a b : ℝ
n : ℕ
r : ℂ
h : ¬r + 1 = 0 ∧ ¬0 ∈ [[a, b]]
⊢ r + 1 ≠ 0
[PROOFSTEP]
exact h.1
[GOAL]
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
[PROOFSTEP]
by_cases hab : (0 : ℝ) ∉ [[a, b]]
[GOAL]
case pos
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∈ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
[PROOFSTEP]
apply integral_eq_sub_of_hasDerivAt (fun x hx => ?_) (intervalIntegrable_cpow (r := r) <| Or.inr hab)
[GOAL]
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∈ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ HasDerivAt (fun {b} => ↑b ^ (r + 1) / (r + 1)) (↑x ^ r) x
[PROOFSTEP]
refine' hasDerivAt_ofReal_cpow (ne_of_mem_of_not_mem hx hab) _
[GOAL]
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∈ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ r ≠ -1
[PROOFSTEP]
contrapose! hr
[GOAL]
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hab : ¬0 ∈ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
hr : r = -1
⊢ r + 1 = 0
[PROOFSTEP]
rwa [add_eq_zero_iff_eq_neg]
[GOAL]
case neg
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
[PROOFSTEP]
replace h : -1 < r.re
[GOAL]
case h
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
⊢ -1 < r.re
[PROOFSTEP]
tauto
[GOAL]
case neg
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
[PROOFSTEP]
suffices ∀ c : ℝ, (∫ x : ℝ in (0)..c, (x : ℂ) ^ r) = (c : ℂ) ^ (r + 1) / (r + 1) - (0 : ℂ) ^ (r + 1) / (r + 1)
  by
  rw [← integral_add_adjacent_intervals (@intervalIntegrable_cpow' a 0 r h) (@intervalIntegrable_cpow' 0 b r h),
    integral_symm, this a, this b, Complex.zero_cpow hr]
  ring
[GOAL]
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
this : ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
[PROOFSTEP]
rw [← integral_add_adjacent_intervals (@intervalIntegrable_cpow' a 0 r h) (@intervalIntegrable_cpow' 0 b r h),
  integral_symm, this a, this b, Complex.zero_cpow hr]
[GOAL]
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
this : ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
⊢ -(↑a ^ (r + 1) / (r + 1) - 0 / (r + 1)) + (↑b ^ (r + 1) / (r + 1) - 0 / (r + 1)) =
    ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
[PROOFSTEP]
ring
[GOAL]
case neg
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
⊢ ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
[PROOFSTEP]
intro c
[GOAL]
case neg
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∫ (x : ℝ) in 0 ..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
[PROOFSTEP]
apply integral_eq_sub_of_hasDeriv_right
[GOAL]
case neg.hcont
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ContinuousOn (fun c => ↑c ^ (r + 1) / (r + 1)) [[0, c]]
[PROOFSTEP]
refine' ((Complex.continuous_ofReal_cpow_const _).div_const _).continuousOn
[GOAL]
case neg.hcont
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ 0 < (r + 1).re
[PROOFSTEP]
rwa [Complex.add_re, Complex.one_re, ← neg_lt_iff_pos_add]
[GOAL]
case neg.hderiv
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∀ (x : ℝ), x ∈ Set.Ioo (min 0 c) (max 0 c) → HasDerivWithinAt (fun c => ↑c ^ (r + 1) / (r + 1)) (↑x ^ r) (Set.Ioi x) x
[PROOFSTEP]
refine' fun x hx => (hasDerivAt_ofReal_cpow _ _).hasDerivWithinAt
[GOAL]
case neg.hderiv.refine'_1
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
⊢ x ≠ 0
[PROOFSTEP]
rcases le_total c 0 with (hc | hc)
[GOAL]
case neg.hderiv.refine'_1.inl
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : c ≤ 0
⊢ x ≠ 0
[PROOFSTEP]
rw [max_eq_left hc] at hx
[GOAL]
case neg.hderiv.refine'_1.inl
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) 0
hc : c ≤ 0
⊢ x ≠ 0
[PROOFSTEP]
exact hx.2.ne
[GOAL]
case neg.hderiv.refine'_1.inr
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0
[PROOFSTEP]
rw [min_eq_left hc] at hx
[GOAL]
case neg.hderiv.refine'_1.inr
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo 0 (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0
[PROOFSTEP]
exact hx.1.ne'
[GOAL]
case neg.hderiv.refine'_2
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
⊢ r ≠ -1
[PROOFSTEP]
contrapose! hr
[GOAL]
case neg.hderiv.refine'_2
a b : ℝ
n : ℕ
r : ℂ
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hr : r = -1
⊢ r + 1 = 0
[PROOFSTEP]
rw [hr]
[GOAL]
case neg.hderiv.refine'_2
a b : ℝ
n : ℕ
r : ℂ
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hr : r = -1
⊢ -1 + 1 = 0
[PROOFSTEP]
ring
[GOAL]
case neg.hint
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ IntervalIntegrable (fun y => ↑y ^ r) MeasureTheory.volume 0 c
[PROOFSTEP]
exact intervalIntegrable_cpow' h
[GOAL]
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
[PROOFSTEP]
have h' : -1 < (r : ℂ).re ∨ (r : ℂ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]] :=
  by
  cases h
  · left; rwa [Complex.ofReal_re]
  · right; rwa [← Complex.ofReal_one, ← Complex.ofReal_neg, Ne.def, Complex.ofReal_inj]
[GOAL]
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
[PROOFSTEP]
cases h
[GOAL]
case inl
a b : ℝ
n : ℕ
r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
[PROOFSTEP]
left
[GOAL]
case inl.h
a b : ℝ
n : ℕ
r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re
[PROOFSTEP]
rwa [Complex.ofReal_re]
[GOAL]
case inr
a b : ℝ
n : ℕ
r : ℝ
h✝ : r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
[PROOFSTEP]
right
[GOAL]
case inr.h
a b : ℝ
n : ℕ
r : ℝ
h✝ : r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
[PROOFSTEP]
rwa [← Complex.ofReal_one, ← Complex.ofReal_neg, Ne.def, Complex.ofReal_inj]
[GOAL]
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
[PROOFSTEP]
have : (∫ x in a..b, (x : ℂ) ^ (r : ℂ)) = ((b : ℂ) ^ (r + 1 : ℂ) - (a : ℂ) ^ (r + 1 : ℂ)) / (r + 1) := integral_cpow h'
[GOAL]
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : ∫ (x : ℝ) in a..b, ↑x ^ ↑r = (↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)
⊢ ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
[PROOFSTEP]
apply_fun Complex.re at this
[GOAL]
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ∫ (x : ℝ) in a..b, x ^ r = (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re
[PROOFSTEP]
simp_rw [intervalIntegral_eq_integral_uIoc, Complex.real_smul, Complex.ofReal_mul_re]
[GOAL]
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r = (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r).re
[PROOFSTEP]
have : Complex.re = IsROrC.re := by rfl
[GOAL]
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ Complex.re = ↑IsROrC.re
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r = (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r).re
[PROOFSTEP]
rw [this, ← integral_re]
[GOAL]
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r =
    (if a ≤ b then 1 else -1) * ∫ (a : ℝ) in Ι a b, ↑IsROrC.re (↑a ^ ↑r)
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ MeasureTheory.Integrable fun x => ↑x ^ ↑r
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ MeasureTheory.Integrable fun x => ↑x ^ ↑r
[PROOFSTEP]
refine' intervalIntegrable_iff.mp _
[GOAL]
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b
[PROOFSTEP]
cases' h' with h' h'
[GOAL]
case h.e'_2.inl
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
h' : -1 < (↑r).re
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b
[PROOFSTEP]
exact intervalIntegrable_cpow' h'
[GOAL]
case h.e'_2.inr
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
h' : ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b
[PROOFSTEP]
exact intervalIntegrable_cpow (Or.inr h'.2)
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
[PROOFSTEP]
rw [(by push_cast ; rfl : (r : ℂ) + 1 = ((r + 1 : ℝ) : ℂ))]
[GOAL]
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ↑r + 1 = ↑(r + 1)
[PROOFSTEP]
push_cast
[GOAL]
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ↑r + 1 = ↑r + 1
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = ((↑b ^ ↑(r + 1) - ↑a ^ ↑(r + 1)) / ↑(r + 1)).re
[PROOFSTEP]
simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.ofReal_mul_re, Complex.sub_re]
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = (r + 1)⁻¹ * ((↑b ^ ↑(r + 1)).re - (↑a ^ ↑(r + 1)).re)
[PROOFSTEP]
rfl
[GOAL]
a b : ℝ
n✝ : ℕ
n : ℤ
h : 0 ≤ n ∨ n ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
[PROOFSTEP]
replace h : -1 < (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]]
[GOAL]
case h
a b : ℝ
n✝ : ℕ
n : ℤ
h : 0 ≤ n ∨ n ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ -1 < ↑n ∨ ↑n ≠ -1 ∧ ¬0 ∈ [[a, b]]
[PROOFSTEP]
exact_mod_cast h
[GOAL]
a b : ℝ
n✝ : ℕ
n : ℤ
h : -1 < ↑n ∨ ↑n ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
[PROOFSTEP]
exact_mod_cast integral_rpow h
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
[PROOFSTEP]
simpa only [← Int.ofNat_succ, zpow_ofNat] using integral_zpow (Or.inl (Int.coe_nat_nonneg n))
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)
[PROOFSTEP]
cases' le_or_lt a b with hab hab
[GOAL]
case inl
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)
[PROOFSTEP]
calc
  ∫ x in Ι a b, |x - a| ^ n = ∫ x in a..b, |x - a| ^ n := by rw [uIoc_of_le hab, ← integral_of_le hab]
  _ = ∫ x in (0)..(b - a), x ^ n :=
    by
    simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
    refine' integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| _) rfl
    rw [uIcc_of_le (sub_nonneg.2 hab)] at hx
    exact hx.1
  _ = |b - a| ^ (n + 1) / (n + 1) := by simp [abs_of_nonneg (sub_nonneg.2 hab)]
[GOAL]
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = ∫ (x : ℝ) in a..b, |x - a| ^ n
[PROOFSTEP]
rw [uIoc_of_le hab, ← integral_of_le hab]
[GOAL]
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, |x - a| ^ n = ∫ (x : ℝ) in 0 ..b - a, x ^ n
[PROOFSTEP]
simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
[GOAL]
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in 0 ..b - a, |x| ^ n = ∫ (x : ℝ) in 0 ..b - a, x ^ n
[PROOFSTEP]
refine' integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| _) rfl
[GOAL]
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ [[0, b - a]]
⊢ 0 ≤ x
[PROOFSTEP]
rw [uIcc_of_le (sub_nonneg.2 hab)] at hx
[GOAL]
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ Set.Icc 0 (b - a)
⊢ 0 ≤ x
[PROOFSTEP]
exact hx.1
[GOAL]
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in 0 ..b - a, x ^ n = |b - a| ^ (n + 1) / (↑n + 1)
[PROOFSTEP]
simp [abs_of_nonneg (sub_nonneg.2 hab)]
[GOAL]
case inr
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)
[PROOFSTEP]
calc
  ∫ x in Ι a b, |x - a| ^ n = ∫ x in b..a, |x - a| ^ n := by rw [uIoc_of_lt hab, ← integral_of_le hab.le]
  _ = ∫ x in b - a..0, (-x) ^ n :=
    by
    simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
    refine' integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| _) rfl
    rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx
    exact hx.2
  _ = |b - a| ^ (n + 1) / (n + 1) := by simp [integral_comp_neg fun x => x ^ n, abs_of_neg (sub_neg.2 hab)]
[GOAL]
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = ∫ (x : ℝ) in b..a, |x - a| ^ n
[PROOFSTEP]
rw [uIoc_of_lt hab, ← integral_of_le hab.le]
[GOAL]
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in b..a, |x - a| ^ n = ∫ (x : ℝ) in b - a..0, (-x) ^ n
[PROOFSTEP]
simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
[GOAL]
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in b - a..0, |x| ^ n = ∫ (x : ℝ) in b - a..0, (-x) ^ n
[PROOFSTEP]
refine' integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| _) rfl
[GOAL]
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ [[b - a, 0]]
⊢ x ≤ 0
[PROOFSTEP]
rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx
[GOAL]
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ Set.Icc (b - a) 0
⊢ x ≤ 0
[PROOFSTEP]
exact hx.2
[GOAL]
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in b - a..0, (-x) ^ n = |b - a| ^ (n + 1) / (↑n + 1)
[PROOFSTEP]
simp [integral_comp_neg fun x => x ^ n, abs_of_neg (sub_neg.2 hab)]
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
[PROOFSTEP]
have := @integral_pow a b 1
[GOAL]
a b : ℝ
n : ℕ
this : ∫ (x : ℝ) in a..b, x ^ 1 = (b ^ (1 + 1) - a ^ (1 + 1)) / (↑1 + 1)
⊢ ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
[PROOFSTEP]
norm_num at this
[GOAL]
a b : ℝ
n : ℕ
this : ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
⊢ ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
[PROOFSTEP]
exact this
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, 1 = b - a
[PROOFSTEP]
simp only [mul_one, smul_eq_mul, integral_const]
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..a + 1, b = b
[PROOFSTEP]
simp
[GOAL]
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = Real.log (b / a)
[PROOFSTEP]
have h' := fun x (hx : x ∈ [[a, b]]) => ne_of_mem_of_not_mem hx h
[GOAL]
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
h' : ∀ (x : ℝ), x ∈ [[a, b]] → x ≠ 0
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = Real.log (b / a)
[PROOFSTEP]
rw [integral_deriv_eq_sub' _ deriv_log' (fun x hx => differentiableAt_log (h' x hx))
    (continuousOn_inv₀.mono <| subset_compl_singleton_iff.mpr h),
  log_div (h' b right_mem_uIcc) (h' a left_mem_uIcc)]
[GOAL]
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
[PROOFSTEP]
simp only [one_div, integral_inv h]
[GOAL]
a b : ℝ
n : ℕ
ha : 0 < a
hb : 0 < b
⊢ ∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
[PROOFSTEP]
simp only [one_div, integral_inv_of_pos ha hb]
[GOAL]
a b : ℝ
n : ℕ
ha : a < 0
hb : b < 0
⊢ ∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
[PROOFSTEP]
simp only [one_div, integral_inv_of_neg ha hb]
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, exp x = exp b - exp a
[PROOFSTEP]
rw [integral_deriv_eq_sub']
[GOAL]
case hderiv
a b : ℝ
n : ℕ
⊢ deriv exp = fun x => exp x
[PROOFSTEP]
norm_num
[GOAL]
case hdiff
a b : ℝ
n : ℕ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ exp x
[PROOFSTEP]
exact fun _ _ => differentiableAt_exp
[GOAL]
case hcont
a b : ℝ
n : ℕ
⊢ ContinuousOn (fun x => exp x) [[a, b]]
[PROOFSTEP]
exact continuousOn_exp
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, Complex.exp (c * ↑x) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
[PROOFSTEP]
have D : ∀ x : ℝ, HasDerivAt (fun y : ℝ => Complex.exp (c * y) / c) (Complex.exp (c * x)) x :=
  by
  intro x
  conv => congr
  rw [← mul_div_cancel (Complex.exp (c * x)) hc]
  apply ((Complex.hasDerivAt_exp _).comp x _).div_const c
  simpa only [mul_one] using ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
⊢ ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
[PROOFSTEP]
intro x
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
[PROOFSTEP]
conv => congr
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
| HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
[PROOFSTEP]
congr
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
| HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
[PROOFSTEP]
congr
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
| HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
[PROOFSTEP]
congr
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
[PROOFSTEP]
rw [← mul_div_cancel (Complex.exp (c * x)) hc]
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x) * c / c) x
[PROOFSTEP]
apply ((Complex.hasDerivAt_exp _).comp x _).div_const c
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun x => c * ↑x) c x
[PROOFSTEP]
simpa only [mul_one] using ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ ∫ (x : ℝ) in a..b, Complex.exp (c * ↑x) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
[PROOFSTEP]
rw [integral_deriv_eq_sub' _ (funext fun x => (D x).deriv) fun x _ => (D x).differentiableAt]
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ Complex.exp (c * ↑b) / c - Complex.exp (c * ↑a) / c = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
[PROOFSTEP]
ring
[GOAL]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ ContinuousOn (fun x => Complex.exp (c * ↑x)) [[a, b]]
[PROOFSTEP]
apply Continuous.continuousOn
[GOAL]
case h
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ Continuous fun x => Complex.exp (c * ↑x)
[PROOFSTEP]
continuity
[GOAL]
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
[PROOFSTEP]
have h' := fun x (hx : x ∈ [[a, b]]) => ne_of_mem_of_not_mem hx h
[GOAL]
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
h' : ∀ (x : ℝ), x ∈ [[a, b]] → x ≠ 0
⊢ ∫ (x : ℝ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
[PROOFSTEP]
have heq := fun x hx => mul_inv_cancel (h' x hx)
[GOAL]
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
h' : ∀ (x : ℝ), x ∈ [[a, b]] → x ≠ 0
heq : ∀ (x : ℝ), x ∈ [[a, b]] → x * x⁻¹ = 1
⊢ ∫ (x : ℝ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
[PROOFSTEP]
convert
  integral_mul_deriv_eq_deriv_mul (fun x hx => hasDerivAt_log (h' x hx)) (fun x _ => hasDerivAt_id x)
    (continuousOn_inv₀.mono <| subset_compl_singleton_iff.mpr h).intervalIntegrable
    continuousOn_const.intervalIntegrable using
  1
[GOAL]
case h.e'_2
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
h' : ∀ (x : ℝ), x ∈ [[a, b]] → x ≠ 0
heq : ∀ (x : ℝ), x ∈ [[a, b]] → x * x⁻¹ = 1
⊢ ∫ (x : ℝ) in a..b, Real.log x = ∫ (x : ℝ) in a..b, Real.log x * 1
[PROOFSTEP]
simp [integral_congr heq, mul_comm, ← sub_add]
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
h' : ∀ (x : ℝ), x ∈ [[a, b]] → x ≠ 0
heq : ∀ (x : ℝ), x ∈ [[a, b]] → x * x⁻¹ = 1
⊢ b * Real.log b - a * Real.log a - b + a = Real.log b * id b - Real.log a * id a - ∫ (x : ℝ) in a..b, x⁻¹ * id x
[PROOFSTEP]
simp [integral_congr heq, mul_comm, ← sub_add]
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x = cos a - cos b
[PROOFSTEP]
rw [integral_deriv_eq_sub' fun x => -cos x]
[GOAL]
a b : ℝ
n : ℕ
⊢ -cos b - -cos a = cos a - cos b
[PROOFSTEP]
ring
[GOAL]
case hderiv
a b : ℝ
n : ℕ
⊢ (deriv fun x => -cos x) = fun x => sin x
[PROOFSTEP]
norm_num
[GOAL]
case hdiff
a b : ℝ
n : ℕ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ (fun x => -cos x) x
[PROOFSTEP]
simp only [differentiableAt_neg_iff, differentiableAt_cos, implies_true]
[GOAL]
case hcont
a b : ℝ
n : ℕ
⊢ ContinuousOn (fun x => sin x) [[a, b]]
[PROOFSTEP]
exact continuousOn_sin
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, cos x = sin b - sin a
[PROOFSTEP]
rw [integral_deriv_eq_sub']
[GOAL]
case hderiv
a b : ℝ
n : ℕ
⊢ deriv sin = fun x => cos x
[PROOFSTEP]
norm_num
[GOAL]
case hdiff
a b : ℝ
n : ℕ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ sin x
[PROOFSTEP]
simp only [differentiableAt_sin, implies_true]
[GOAL]
case hcont
a b : ℝ
n : ℕ
⊢ ContinuousOn (fun x => cos x) [[a, b]]
[PROOFSTEP]
exact continuousOn_cos
[GOAL]
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, Complex.cos (z * ↑x) = Complex.sin (z * ↑b) / z - Complex.sin (z * ↑a) / z
[PROOFSTEP]
apply integral_eq_sub_of_hasDerivAt
[GOAL]
case hderiv
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
case hint
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ IntervalIntegrable (fun y => Complex.cos (z * ↑y)) MeasureTheory.volume a b
[PROOFSTEP]
swap
[GOAL]
case hint
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ IntervalIntegrable (fun y => Complex.cos (z * ↑y)) MeasureTheory.volume a b
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case hint.hu
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ Continuous fun y => Complex.cos (z * ↑y)
[PROOFSTEP]
exact Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)
[GOAL]
case hderiv
a✝ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
[PROOFSTEP]
intro x _
[GOAL]
case hderiv
a✝¹ b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a b x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
[PROOFSTEP]
have a := Complex.hasDerivAt_sin (↑x * z)
[GOAL]
case hderiv
a✝² b✝ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b x : ℝ
a✝ : x ∈ [[a✝¹, b]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
[PROOFSTEP]
have b : HasDerivAt (fun y => y * z : ℂ → ℂ) z ↑x := hasDerivAt_mul_const _
[GOAL]
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
[PROOFSTEP]
have c : HasDerivAt (fun y : ℂ => Complex.sin (y * z)) _ ↑x := HasDerivAt.comp (𝕜 := ℂ) x a b
[GOAL]
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
[PROOFSTEP]
have d := HasDerivAt.comp_ofReal (c.div_const z)
[GOAL]
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (↑y * z) / z) (Complex.cos (↑x * z) * z / z) x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
[PROOFSTEP]
simp only [mul_comm] at d
[GOAL]
case hderiv
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
[PROOFSTEP]
convert d using 1
[GOAL]
case h.e'_7
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
⊢ Complex.cos (z * ↑x) = z * Complex.cos (z * ↑x) / z
[PROOFSTEP]
conv_rhs => arg 1; rw [mul_comm]
[GOAL]
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
| z * Complex.cos (z * ↑x) / z
[PROOFSTEP]
arg 1; rw [mul_comm]
[GOAL]
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
| z * Complex.cos (z * ↑x) / z
[PROOFSTEP]
arg 1; rw [mul_comm]
[GOAL]
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
| z * Complex.cos (z * ↑x) / z
[PROOFSTEP]
arg 1
[GOAL]
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
| z * Complex.cos (z * ↑x)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case h.e'_7
a✝² b✝¹ : ℝ
n : ℕ
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
c : HasDerivAt (fun y => Complex.sin (y * z)) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y => Complex.sin (z * ↑y) / z) (z * Complex.cos (z * ↑x) / z) x
⊢ Complex.cos (z * ↑x) = Complex.cos (z * ↑x) * z / z
[PROOFSTEP]
rw [mul_div_cancel _ hz]
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, cos x ^ 2 - sin x ^ 2 = sin b * cos b - sin a * cos a
[PROOFSTEP]
simpa only [sq, sub_eq_add_neg, neg_mul_eq_mul_neg] using
  integral_deriv_mul_eq_sub (fun x _ => hasDerivAt_sin x) (fun x _ => hasDerivAt_cos x)
    continuousOn_cos.intervalIntegrable continuousOn_sin.neg.intervalIntegrable
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, (1 + x ^ 2)⁻¹ = arctan b - arctan a
[PROOFSTEP]
simp only [← one_div]
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2) = arctan b - arctan a
[PROOFSTEP]
refine' integral_deriv_eq_sub' _ _ _ (continuous_const.div _ fun x => _).continuousOn
[GOAL]
case refine'_1
a b : ℝ
n : ℕ
⊢ deriv arctan = fun x => 1 / (1 + x ^ 2)
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2
a b : ℝ
n : ℕ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ arctan x
[PROOFSTEP]
exact fun _ _ => differentiableAt_arctan _
[GOAL]
case refine'_3
a b : ℝ
n : ℕ
⊢ Continuous fun x => 1 + x ^ 2
[PROOFSTEP]
continuity
[GOAL]
case refine'_4
a b : ℝ
n : ℕ
x : ℝ
⊢ 1 + x ^ 2 ≠ 0
[PROOFSTEP]
nlinarith
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2) = arctan b - arctan a
[PROOFSTEP]
simp only [one_div, integral_inv_one_add_sq]
[GOAL]
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
⊢ ∫ (x : ℝ) in a..b, ↑x * (1 + ↑x ^ 2) ^ t =
    (1 + ↑b ^ 2) ^ (t + 1) / (↑2 * (t + 1)) - (1 + ↑a ^ 2) ^ (t + 1) / (2 * (t + 1))
[PROOFSTEP]
have : t + 1 ≠ 0 := by contrapose! ht; rwa [add_eq_zero_iff_eq_neg] at ht
[GOAL]
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
⊢ t + 1 ≠ 0
[PROOFSTEP]
contrapose! ht
[GOAL]
a b : ℝ
n : ℕ
t : ℂ
ht : t + 1 = 0
⊢ t = -1
[PROOFSTEP]
rwa [add_eq_zero_iff_eq_neg] at ht
[GOAL]
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∫ (x : ℝ) in a..b, ↑x * (1 + ↑x ^ 2) ^ t =
    (1 + ↑b ^ 2) ^ (t + 1) / (↑2 * (t + 1)) - (1 + ↑a ^ 2) ^ (t + 1) / (2 * (t + 1))
[PROOFSTEP]
apply integral_eq_sub_of_hasDerivAt
[GOAL]
case hderiv
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (↑2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x
[PROOFSTEP]
intro x _
[GOAL]
case hderiv
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (↑2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x
[PROOFSTEP]
have f : HasDerivAt (fun y : ℂ => 1 + y ^ 2) (2 * x) x :=
  by
  convert (hasDerivAt_pow 2 (x : ℂ)).const_add 1
  · norm_cast
  · simp
[GOAL]
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
[PROOFSTEP]
convert (hasDerivAt_pow 2 (x : ℂ)).const_add 1
[GOAL]
case h.e'_6.h.h.e'_5
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
x✝ : ℂ
⊢ ↑1 = 1
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_7.h.e'_6
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ ↑x = ↑x ^ (2 - 1)
[PROOFSTEP]
simp
[GOAL]
case hderiv
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
⊢ HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (↑2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x
[PROOFSTEP]
have g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z :=
  by
  intro z hz
  convert (HasDerivAt.cpow_const (c := t + 1) (hasDerivAt_id _) (Or.inl hz)).div_const (2 * (t + 1)) using 1
  field_simp
  ring
[GOAL]
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
⊢ ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
[PROOFSTEP]
intro z hz
[GOAL]
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
[PROOFSTEP]
convert (HasDerivAt.cpow_const (c := t + 1) (hasDerivAt_id _) (Or.inl hz)).div_const (2 * (t + 1)) using 1
[GOAL]
case h.e'_7
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ z ^ t / 2 = (t + 1) * id z ^ (t + 1 - 1) * 1 / (2 * (t + 1))
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_7
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
hz : 0 < z.re
⊢ z ^ t * (2 * (t + 1)) = (t + 1) * z ^ t * 2
[PROOFSTEP]
ring
[GOAL]
case hderiv
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ HasDerivAt (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (↑2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x
[PROOFSTEP]
convert (HasDerivAt.comp (↑x) (g _) f).comp_ofReal using 1
[GOAL]
case h.e'_6
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ (fun {b} => (1 + ↑b ^ 2) ^ (t + 1) / (↑2 * (t + 1))) = fun y =>
    ((fun z => z ^ (t + 1) / (2 * (t + 1))) ∘ fun y => ↑1 + y ^ 2) ↑y
[PROOFSTEP]
simp
[GOAL]
case h.e'_7
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ ↑x * (1 + ↑x ^ 2) ^ t = (↑1 + ↑x ^ 2) ^ t / 2 * (2 * ↑x)
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_7
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ ↑x * (1 + ↑x ^ 2) ^ t * 2 = (1 + ↑x ^ 2) ^ t * (2 * ↑x)
[PROOFSTEP]
ring
[GOAL]
case hderiv
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y => ↑1 + y ^ 2) (2 * ↑x) ↑x
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ 0 < (↑1 + ↑x ^ 2).re
[PROOFSTEP]
exact_mod_cast add_pos_of_pos_of_nonneg zero_lt_one (sq_nonneg x)
[GOAL]
case hint
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ IntervalIntegrable (fun y => ↑y * (1 + ↑y ^ 2) ^ t) MeasureTheory.volume a b
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case hint.hu
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y => ↑y * (1 + ↑y ^ 2) ^ t
[PROOFSTEP]
refine' continuous_ofReal.mul _
[GOAL]
case hint.hu
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y => (1 + ↑y ^ 2) ^ t
[PROOFSTEP]
apply Continuous.cpow
[GOAL]
case hint.hu.hf
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun x => 1 + ↑x ^ 2
[PROOFSTEP]
exact continuous_const.add (continuous_ofReal.pow 2)
[GOAL]
case hint.hu.hg
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun x => t
[PROOFSTEP]
exact continuous_const
[GOAL]
case hint.hu.h0
a b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∀ (a : ℝ), 0 < (1 + ↑a ^ 2).re ∨ (1 + ↑a ^ 2).im ≠ 0
[PROOFSTEP]
intro a
[GOAL]
case hint.hu.h0
a✝ b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ 0 < (1 + ↑a ^ 2).re ∨ (1 + ↑a ^ 2).im ≠ 0
[PROOFSTEP]
rw [add_re, one_re, ← ofReal_pow, ofReal_re]
[GOAL]
case hint.hu.h0
a✝ b : ℝ
n : ℕ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ 0 < 1 + a ^ 2 ∨ (1 + ↑(a ^ 2)).im ≠ 0
[PROOFSTEP]
exact Or.inl (add_pos_of_pos_of_nonneg zero_lt_one (sq_nonneg a))
[GOAL]
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
⊢ ∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t = (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))
[PROOFSTEP]
have : ∀ x s : ℝ, (((↑1 + x ^ 2) ^ s : ℝ) : ℂ) = (1 + (x : ℂ) ^ 2) ^ (s : ℂ) :=
  by
  intro x s
  norm_cast
  rw [ofReal_cpow, ofReal_add, ofReal_pow, ofReal_one]
  exact add_nonneg zero_le_one (sq_nonneg x)
[GOAL]
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
⊢ ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
[PROOFSTEP]
intro x s
[GOAL]
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
[PROOFSTEP]
norm_cast
[GOAL]
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ ↑((1 + x ^ 2) ^ s) = ↑(1 + x ^ 2) ^ ↑s
[PROOFSTEP]
rw [ofReal_cpow, ofReal_add, ofReal_pow, ofReal_one]
[GOAL]
case hx
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ 0 ≤ 1 + x ^ 2
[PROOFSTEP]
exact add_nonneg zero_le_one (sq_nonneg x)
[GOAL]
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t = (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))
[PROOFSTEP]
rw [← ofReal_inj]
[GOAL]
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑(∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t) =
    ↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1)))
[PROOFSTEP]
convert integral_mul_cpow_one_add_sq (_ : (t : ℂ) ≠ -1)
[GOAL]
case h.e'_2
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑(∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t) = ∫ (x : ℝ) in ?convert_1..?convert_2, ↑x * (1 + ↑x ^ 2) ^ ↑t
[PROOFSTEP]
rw [← intervalIntegral.integral_ofReal]
[GOAL]
case h.e'_2
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ∫ (x : ℝ) in a..b, ↑(x * (1 + x ^ 2) ^ t) = ∫ (x : ℝ) in ?convert_1..?convert_2, ↑x * (1 + ↑x ^ 2) ^ ↑t
case convert_1
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ℝ
case convert_2 a b : ℝ n : ℕ t : ℝ ht : t ≠ -1 this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s ⊢ ℝ
[PROOFSTEP]
congr with x : 1
[GOAL]
case h.e'_2.e_f.h
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
x : ℝ
⊢ ↑(x * (1 + x ^ 2) ^ t) = ↑x * (1 + ↑x ^ 2) ^ ↑t
[PROOFSTEP]
rw [ofReal_mul, this x t]
[GOAL]
case h.e'_2.e_f.h
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
x : ℝ
⊢ ↑x * (↑1 + ↑x ^ 2) ^ ↑t = ↑x * (1 + ↑x ^ 2) ^ ↑t
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (↑2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
[PROOFSTEP]
simp_rw [ofReal_sub, ofReal_div, this a (t + 1), this b (t + 1)]
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ (↑1 + ↑b ^ 2) ^ ↑(t + 1) / ↑(2 * (t + 1)) - (↑1 + ↑a ^ 2) ^ ↑(t + 1) / ↑(2 * (t + 1)) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (↑2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
[PROOFSTEP]
rfl
[GOAL]
case convert_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ↑t ≠ -1
[PROOFSTEP]
rw [← ofReal_one, ← ofReal_neg, Ne.def, ofReal_inj]
[GOAL]
case convert_3
a b : ℝ
n : ℕ
t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (↑1 + ↑x ^ 2) ^ ↑s
⊢ ¬t = -1
[PROOFSTEP]
exact ht
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
[PROOFSTEP]
have continuous_sin_pow : ∀ (k : ℕ), (Continuous fun x => sin x ^ k) := fun k => continuous_sin.pow k
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
[PROOFSTEP]
let C := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
[PROOFSTEP]
have h : ∀ α β γ : ℝ, β * α * γ * α = β * (α * α * γ) := fun α β γ => by ring
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
α β γ : ℝ
⊢ β * α * γ * α = β * (α * α * γ)
[PROOFSTEP]
ring
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
[PROOFSTEP]
have hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) ((n + 1 : ℕ) * cos x * sin x ^ n) x := fun x _ => by
  simpa only [mul_right_comm] using (hasDerivAt_sin x).pow (n + 1)
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
[PROOFSTEP]
simpa only [mul_right_comm] using (hasDerivAt_sin x).pow (n + 1)
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
[PROOFSTEP]
have hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x := fun x _ => by simpa only [neg_neg] using (hasDerivAt_cos x).neg
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt (-cos) (sin x) x
[PROOFSTEP]
simpa only [neg_neg] using (hasDerivAt_cos x).neg
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
[PROOFSTEP]
have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_
[GOAL]
case refine_3
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
case refine_1
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ IntervalIntegrable (fun x => ↑(n + 1) * cos x * sin x ^ n) MeasureTheory.volume a b
case refine_2
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ IntervalIntegrable (fun x => sin x) MeasureTheory.volume a b
[PROOFSTEP]
calc
  (∫ x in a..b, sin x ^ (n + 2)) = ∫ x in a..b, sin x ^ (n + 1) * sin x := by simp only [_root_.pow_succ']
  _ = C + (↑n + 1) * ∫ x in a..b, cos x ^ 2 * sin x ^ n := by simp [H, h, sq]; ring
  _ = C + (↑n + 1) * ∫ x in a..b, sin x ^ n - sin x ^ (n + 2) := by simp [cos_sq', sub_mul, ← pow_add, add_comm]
  _ = (C + (↑n + 1) * ∫ x in a..b, sin x ^ n) - (↑n + 1) * ∫ x in a..b, sin x ^ (n + 2) :=
    by
    rw [integral_sub, mul_sub, add_sub_assoc] <;> apply Continuous.intervalIntegrable
    · exact continuous_sin_pow n
    · exact continuous_sin_pow (n + 2)
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) = ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x
[PROOFSTEP]
simp only [_root_.pow_succ']
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x = C + (↑n + ↑1) * ∫ (x : ℝ) in a..b, cos x ^ 2 * sin x ^ n
[PROOFSTEP]
simp [H, h, sq]
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ -(sin b ^ (n + 1) * cos b) + sin a ^ (n + 1) * cos a = sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
[PROOFSTEP]
ring
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ C + (↑n + ↑1) * ∫ (x : ℝ) in a..b, cos x ^ 2 * sin x ^ n =
    C + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2)
[PROOFSTEP]
simp [cos_sq', sub_mul, ← pow_add, add_comm]
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ C + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2) =
    (C + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
[PROOFSTEP]
rw [integral_sub, mul_sub, add_sub_assoc]
[GOAL]
case hf
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ IntervalIntegrable (fun x => sin x ^ n) MeasureTheory.volume a b
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case hg
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ IntervalIntegrable (fun x => sin x ^ (n + 2)) MeasureTheory.volume a b
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case hf.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ Continuous fun x => sin x ^ n
[PROOFSTEP]
exact continuous_sin_pow n
[GOAL]
case hg.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ Continuous fun x => sin x ^ (n + 2)
[PROOFSTEP]
exact continuous_sin_pow (n + 2)
[GOAL]
case refine_1
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ IntervalIntegrable (fun x => ↑(n + 1) * cos x * sin x ^ n) MeasureTheory.volume a b
case refine_2
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ IntervalIntegrable (fun x => sin x) MeasureTheory.volume a b
[PROOFSTEP]
all_goals apply Continuous.intervalIntegrable
[GOAL]
case refine_1
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ IntervalIntegrable (fun x => ↑(n + 1) * cos x * sin x ^ n) MeasureTheory.volume a b
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case refine_2
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ IntervalIntegrable (fun x => sin x) MeasureTheory.volume a b
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case refine_1.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ Continuous fun x => ↑(n + 1) * cos x * sin x ^ n
[PROOFSTEP]
have : Continuous fun x ↦ ↑(n + 1) * cos x := by continuity
[GOAL]
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ Continuous fun x => ↑(n + 1) * cos x
[PROOFSTEP]
continuity
[GOAL]
case refine_1.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
this : Continuous fun x => ↑(n + 1) * cos x
⊢ Continuous fun x => ↑(n + 1) * cos x * sin x ^ n
[PROOFSTEP]
exact this.mul (continuous_sin_pow n)
[GOAL]
case refine_2.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ Continuous fun x => sin x
[PROOFSTEP]
exact continuous_sin
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, sin x ^ n
[PROOFSTEP]
have : n + 2 ≠ 0 := by linarith
[GOAL]
a b : ℝ
n : ℕ
⊢ n + 2 ≠ 0
[PROOFSTEP]
linarith
[GOAL]
a b : ℝ
n : ℕ
this : n + 2 ≠ 0
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, sin x ^ n
[PROOFSTEP]
have : (n : ℝ) + 2 ≠ 0 := by norm_cast
[GOAL]
a b : ℝ
n : ℕ
this : n + 2 ≠ 0
⊢ ↑n + 2 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, sin x ^ n
[PROOFSTEP]
field_simp
[GOAL]
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) =
    sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n
[PROOFSTEP]
convert eq_sub_iff_add_eq.mp (integral_sin_pow_aux n) using 1
[GOAL]
case h.e'_2
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) =
    (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
[PROOFSTEP]
ring
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 = (sin a * cos a - sin b * cos b + b - a) / 2
[PROOFSTEP]
field_simp [integral_sin_pow, add_sub_assoc]
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * n + 1) = 2 * ∏ i in Finset.range n, (2 * ↑i + 2) / (2 * ↑i + 3)
[PROOFSTEP]
induction' n with k ih
[GOAL]
case zero
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * zero + 1) = 2 * ∏ i in Finset.range zero, (2 * ↑i + 2) / (2 * ↑i + 3)
[PROOFSTEP]
norm_num
[GOAL]
case succ
a b : ℝ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i in Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * succ k + 1) = 2 * ∏ i in Finset.range (succ k), (2 * ↑i + 2) / (2 * ↑i + 3)
[PROOFSTEP]
rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]
[GOAL]
case succ
a b : ℝ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i in Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ (sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / (↑(2 * k + 1) + 2) +
      (↑(2 * k + 1) + 1) / (↑(2 * k + 1) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) =
    (2 * ↑k + 2) / (2 * ↑k + 3) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)
[PROOFSTEP]
norm_cast
[GOAL]
case succ
a b : ℝ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) = 2 * ∏ i in Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ (sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / ↑(2 * k + 1 + 2) +
      ↑(2 * k + 1 + 1) / ↑(2 * k + 1 + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) =
    ↑(2 * k + 2) / ↑(2 * k + 3) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)
[PROOFSTEP]
simp [-cast_add, field_simps]
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * n) = π * ∏ i in Finset.range n, (2 * ↑i + 1) / (2 * ↑i + 2)
[PROOFSTEP]
induction' n with k ih
[GOAL]
case zero
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * zero) = π * ∏ i in Finset.range zero, (2 * ↑i + 1) / (2 * ↑i + 2)
[PROOFSTEP]
simp
[GOAL]
case succ
a b : ℝ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i in Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * succ k) = π * ∏ i in Finset.range (succ k), (2 * ↑i + 1) / (2 * ↑i + 2)
[PROOFSTEP]
rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]
[GOAL]
case succ
a b : ℝ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i in Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
[PROOFSTEP]
norm_cast
[GOAL]
case succ
a b : ℝ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i in Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / ↑(2 * k + 2) +
      ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
[PROOFSTEP]
simp [-cast_add, field_simps]
[GOAL]
a b : ℝ
n : ℕ
⊢ 0 < ∫ (x : ℝ) in 0 ..π, sin x ^ n
[PROOFSTEP]
rcases even_or_odd' n with ⟨k, rfl | rfl⟩
[GOAL]
case intro.inl
a b : ℝ
k : ℕ
⊢ 0 < ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
[PROOFSTEP]
simp only [integral_sin_pow_even, integral_sin_pow_odd]
[GOAL]
case intro.inr
a b : ℝ
k : ℕ
⊢ 0 < ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)
[PROOFSTEP]
simp only [integral_sin_pow_even, integral_sin_pow_odd]
[GOAL]
case intro.inl
a b : ℝ
k : ℕ
⊢ 0 < π * ∏ i in Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
[PROOFSTEP]
refine' mul_pos (by norm_num <;> exact pi_pos) (prod_pos fun n _ => div_pos _ _)
[GOAL]
a b : ℝ
k : ℕ
⊢ 0 < π
[PROOFSTEP]
norm_num
[GOAL]
a b : ℝ
k : ℕ
⊢ 0 < π
[PROOFSTEP]
exact pi_pos
[GOAL]
case intro.inr
a b : ℝ
k : ℕ
⊢ 0 < 2 * ∏ i in Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
[PROOFSTEP]
refine' mul_pos (by norm_num <;> exact pi_pos) (prod_pos fun n _ => div_pos _ _)
[GOAL]
a b : ℝ
k : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case intro.inl.refine'_1
a b : ℝ
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 1
[PROOFSTEP]
norm_cast
[GOAL]
case intro.inl.refine'_2
a b : ℝ
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 2
[PROOFSTEP]
norm_cast
[GOAL]
case intro.inr.refine'_1
a b : ℝ
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 2
[PROOFSTEP]
norm_cast
[GOAL]
case intro.inr.refine'_2
a b : ℝ
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 3
[PROOFSTEP]
norm_cast
[GOAL]
case intro.inl.refine'_1
a b : ℝ
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 1
[PROOFSTEP]
linarith
[GOAL]
case intro.inl.refine'_2
a b : ℝ
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 2
[PROOFSTEP]
linarith
[GOAL]
case intro.inr.refine'_1
a b : ℝ
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 2
[PROOFSTEP]
linarith
[GOAL]
case intro.inr.refine'_2
a b : ℝ
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 3
[PROOFSTEP]
linarith
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ n
[PROOFSTEP]
let H x h := pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (n.le_add_right 1)
[GOAL]
a b : ℝ
n : ℕ
H : ∀ (x : ℝ), x ∈ Set.Icc 0 π → sin x ^ (n + 1) ≤ sin x ^ n :=
  fun x h => pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ n
[PROOFSTEP]
refine' integral_mono_on pi_pos.le _ _ H
[GOAL]
case refine'_1
a b : ℝ
n : ℕ
H : ∀ (x : ℝ), x ∈ Set.Icc 0 π → sin x ^ (n + 1) ≤ sin x ^ n :=
  fun x h => pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)
⊢ IntervalIntegrable (fun x => sin x ^ (n + 1)) MeasureTheory.volume 0 π
[PROOFSTEP]
exact (continuous_sin.pow _).intervalIntegrable 0 π
[GOAL]
case refine'_2
a b : ℝ
n : ℕ
H : ∀ (x : ℝ), x ∈ Set.Icc 0 π → sin x ^ (n + 1) ≤ sin x ^ n :=
  fun x h => pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)
⊢ IntervalIntegrable (fun x => sin x ^ n) MeasureTheory.volume 0 π
[PROOFSTEP]
exact (continuous_sin.pow _).intervalIntegrable 0 π
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
[PROOFSTEP]
have continuous_cos_pow : ∀ (k : ℕ), (Continuous fun x => cos x ^ k) := fun k => continuous_cos.pow k
[GOAL]
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
[PROOFSTEP]
let C := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
[GOAL]
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
[PROOFSTEP]
have h : ∀ α β γ : ℝ, β * α * γ * α = β * (α * α * γ) := fun α β γ => by ring
[GOAL]
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
α β γ : ℝ
⊢ β * α * γ * α = β * (α * α * γ)
[PROOFSTEP]
ring
[GOAL]
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
[PROOFSTEP]
have hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => cos y ^ (n + 1)) (-(n + 1 : ℕ) * sin x * cos x ^ n) x := fun x _ => by
  simpa only [mul_right_comm, neg_mul, mul_neg] using (hasDerivAt_cos x).pow (n + 1)
[GOAL]
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
[PROOFSTEP]
simpa only [mul_right_comm, neg_mul, mul_neg] using (hasDerivAt_cos x).pow (n + 1)
[GOAL]
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
[PROOFSTEP]
have hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x := fun x _ => hasDerivAt_sin x
[GOAL]
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
[PROOFSTEP]
have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_
[GOAL]
case refine_3
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
case refine_1
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
⊢ IntervalIntegrable (fun x => -↑(n + 1) * sin x * cos x ^ n) MeasureTheory.volume a b
case refine_2
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
⊢ IntervalIntegrable (fun x => cos x) MeasureTheory.volume a b
[PROOFSTEP]
calc
  (∫ x in a..b, cos x ^ (n + 2)) = ∫ x in a..b, cos x ^ (n + 1) * cos x := by simp only [_root_.pow_succ']
  _ = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n := by simp [H, h, sq, -neg_add_rev]
  _ = C + (n + 1) * ∫ x in a..b, cos x ^ n - cos x ^ (n + 2) := by simp [sin_sq, sub_mul, ← pow_add, add_comm]
  _ = (C + (n + 1) * ∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos x ^ (n + 2) :=
    by
    rw [integral_sub, mul_sub, add_sub_assoc] <;> apply Continuous.intervalIntegrable
    · exact continuous_cos_pow n
    · exact continuous_cos_pow (n + 2)
[GOAL]
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) = ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x
[PROOFSTEP]
simp only [_root_.pow_succ']
[GOAL]
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x = C + (↑n + ↑1) * ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x ^ n
[PROOFSTEP]
simp [H, h, sq, -neg_add_rev]
[GOAL]
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ C + (↑n + ↑1) * ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x ^ n =
    C + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n - cos x ^ (n + 2)
[PROOFSTEP]
simp [sin_sq, sub_mul, ← pow_add, add_comm]
[GOAL]
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ C + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n - cos x ^ (n + 2) =
    (C + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
[PROOFSTEP]
rw [integral_sub, mul_sub, add_sub_assoc]
[GOAL]
case hf
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ IntervalIntegrable (fun x => cos x ^ n) MeasureTheory.volume a b
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case hg
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ IntervalIntegrable (fun x => cos x ^ (n + 2)) MeasureTheory.volume a b
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case hf.hu
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ Continuous fun x => cos x ^ n
[PROOFSTEP]
exact continuous_cos_pow n
[GOAL]
case hg.hu
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ Continuous fun x => cos x ^ (n + 2)
[PROOFSTEP]
exact continuous_cos_pow (n + 2)
[GOAL]
case refine_1
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
⊢ IntervalIntegrable (fun x => -↑(n + 1) * sin x * cos x ^ n) MeasureTheory.volume a b
case refine_2
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
⊢ IntervalIntegrable (fun x => cos x) MeasureTheory.volume a b
[PROOFSTEP]
all_goals apply Continuous.intervalIntegrable; continuity
[GOAL]
case refine_1
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
⊢ IntervalIntegrable (fun x => -↑(n + 1) * sin x * cos x ^ n) MeasureTheory.volume a b
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case refine_1.hu
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
⊢ Continuous fun x => -↑(n + 1) * sin x * cos x ^ n
[PROOFSTEP]
continuity
[GOAL]
case refine_2
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
⊢ IntervalIntegrable (fun x => cos x) MeasureTheory.volume a b
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case refine_2.hu
a b : ℝ
n : ℕ
continuous_cos_pow : ∀ (k : ℕ), Continuous fun x => cos x ^ k
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt sin (cos x) x
⊢ Continuous fun x => cos x
[PROOFSTEP]
continuity
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, cos x ^ n
[PROOFSTEP]
have : n + 2 ≠ 0 := by linarith
[GOAL]
a b : ℝ
n : ℕ
⊢ n + 2 ≠ 0
[PROOFSTEP]
linarith
[GOAL]
a b : ℝ
n : ℕ
this : n + 2 ≠ 0
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, cos x ^ n
[PROOFSTEP]
have : (n : ℝ) + 2 ≠ 0 := by norm_cast
[GOAL]
a b : ℝ
n : ℕ
this : n + 2 ≠ 0
⊢ ↑n + 2 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, cos x ^ n
[PROOFSTEP]
field_simp
[GOAL]
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) * (↑n + 2) =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n
[PROOFSTEP]
convert eq_sub_iff_add_eq.mp (integral_cos_pow_aux n) using 1
[GOAL]
case h.e'_2
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) * (↑n + 2) =
    (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
[PROOFSTEP]
ring
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, cos x ^ 2 = (cos b * sin b - cos a * sin a + b - a) / 2
[PROOFSTEP]
field_simp [integral_cos_pow, add_sub_assoc]
[GOAL]
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n
⊢ ∫ (x : ℝ) in a..b, sin x ^ m * cos x ^ (2 * n + 1) = ∫ (x : ℝ) in a..b, sin x ^ m * (1 - sin x ^ 2) ^ n * cos x
[PROOFSTEP]
simp only [_root_.pow_zero, _root_.pow_succ', mul_assoc, pow_mul, one_mul]
[GOAL]
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n
⊢ ∫ (x : ℝ) in a..b, sin x ^ m * ((cos x * cos x) ^ n * cos x) =
    ∫ (x : ℝ) in a..b, sin x ^ m * ((1 - sin x * sin x) ^ n * cos x)
[PROOFSTEP]
congr! 5
[GOAL]
case h.e'_4.h.h.e'_6.h.e'_5.h.e'_5
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n
x✝ : ℝ
⊢ cos x✝ * cos x✝ = 1 - sin x✝ * sin x✝
[PROOFSTEP]
rw [← sq, ← sq, cos_sq']
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x * cos x = (sin b ^ 2 - sin a ^ 2) / 2
[PROOFSTEP]
simpa using integral_sin_pow_mul_cos_pow_odd 1 0
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3
[PROOFSTEP]
have := @integral_sin_pow_mul_cos_pow_odd a b 2 0
[GOAL]
a b : ℝ
n : ℕ
this : ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x ^ (2 * 0 + 1) = ∫ (u : ℝ) in sin a..sin b, u ^ 2 * (1 - u ^ 2) ^ 0
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3
[PROOFSTEP]
norm_num at this
[GOAL]
a b : ℝ
n : ℕ
this : ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x = (sin b ^ 3 - sin a ^ 3) / 3
[PROOFSTEP]
exact this
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3
[PROOFSTEP]
have := @integral_sin_pow_mul_cos_pow_odd a b 0 1
[GOAL]
a b : ℝ
n : ℕ
this : ∫ (x : ℝ) in a..b, sin x ^ 0 * cos x ^ (2 * 1 + 1) = ∫ (u : ℝ) in sin a..sin b, u ^ 0 * (1 - u ^ 2) ^ 1
⊢ ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3
[PROOFSTEP]
norm_num at this
[GOAL]
a b : ℝ
n : ℕ
this : ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3
[PROOFSTEP]
exact this
[GOAL]
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ ∫ (x : ℝ) in a..b, sin x ^ (2 * m + 1) * cos x ^ n = -∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n
[PROOFSTEP]
rw [integral_symm]
[GOAL]
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ -∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n = ∫ (x : ℝ) in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n
[PROOFSTEP]
simp only [_root_.pow_succ', pow_mul, _root_.pow_zero, one_mul, mul_neg, neg_mul, integral_neg, neg_inj]
[GOAL]
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ ∫ (x : ℝ) in b..a, (sin x * sin x) ^ m * sin x * cos x ^ n =
    ∫ (x : ℝ) in b..a, (1 - cos x * cos x) ^ m * sin x * cos x ^ n
[PROOFSTEP]
congr! 5
[GOAL]
case h.e'_4.h.h.e'_5.h.e'_5.h.e'_5
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ sin x✝ * sin x✝ = 1 - cos x✝ * cos x✝
[PROOFSTEP]
rw [← sq, ← sq, sin_sq]
[GOAL]
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ ∫ (x : ℝ) in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n =
    ∫ (x : ℝ) in b..a, cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x
[PROOFSTEP]
congr
[GOAL]
case e_f
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ (fun x => (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n) = fun x => cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x
[PROOFSTEP]
ext
[GOAL]
case e_f.h
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ (1 - cos x✝ ^ 2) ^ m * -sin x✝ * cos x✝ ^ n = cos x✝ ^ n * (1 - cos x✝ ^ 2) ^ m * -sin x✝
[PROOFSTEP]
ring
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x * cos x = (cos a ^ 2 - cos b ^ 2) / 2
[PROOFSTEP]
simpa using integral_sin_pow_odd_mul_cos_pow 0 1
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3
[PROOFSTEP]
have := @integral_sin_pow_odd_mul_cos_pow a b 0 2
[GOAL]
a b : ℝ
n : ℕ
this : ∫ (x : ℝ) in a..b, sin x ^ (2 * 0 + 1) * cos x ^ 2 = ∫ (u : ℝ) in cos b..cos a, u ^ 2 * (1 - u ^ 2) ^ 0
⊢ ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3
[PROOFSTEP]
norm_num at this
[GOAL]
a b : ℝ
n : ℕ
this : ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3
[PROOFSTEP]
exact this
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3
[PROOFSTEP]
have := @integral_sin_pow_odd_mul_cos_pow a b 1 0
[GOAL]
a b : ℝ
n : ℕ
this : ∫ (x : ℝ) in a..b, sin x ^ (2 * 1 + 1) * cos x ^ 0 = ∫ (u : ℝ) in cos b..cos a, u ^ 0 * (1 - u ^ 2) ^ 1
⊢ ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3
[PROOFSTEP]
norm_num at this
[GOAL]
a b : ℝ
n : ℕ
this : ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3
[PROOFSTEP]
exact this
[GOAL]
a b : ℝ
n✝ m n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ (2 * m) * cos x ^ (2 * n) =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n
[PROOFSTEP]
field_simp [pow_mul, sin_sq, cos_sq, ← sub_sub, (by ring : (2 : ℝ) - 1 = 1)]
[GOAL]
a b : ℝ
n✝ m n : ℕ
⊢ 2 - 1 = 1
[PROOFSTEP]
ring
[GOAL]
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x ^ 2 = (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32
[PROOFSTEP]
convert integral_sin_pow_even_mul_cos_pow_even 1 1 using 1
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ 1 * ((1 + cos (2 * x)) / 2) ^ 1
[PROOFSTEP]
have h1 : ∀ c : ℝ, (↑1 - c) / ↑2 * ((↑1 + c) / ↑2) = (↑1 - c ^ 2) / 4 := fun c => by ring
[GOAL]
a b : ℝ
n : ℕ
c : ℝ
⊢ (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
[PROOFSTEP]
ring
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ 1 * ((1 + cos (2 * x)) / 2) ^ 1
[PROOFSTEP]
have h2 : Continuous fun x => cos (2 * x) ^ 2 := by continuity
[GOAL]
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
⊢ Continuous fun x => cos (2 * x) ^ 2
[PROOFSTEP]
continuity
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ 1 * ((1 + cos (2 * x)) / 2) ^ 1
[PROOFSTEP]
have h3 : ∀ x, cos x * sin x = sin (2 * x) / 2 := by intro; rw [sin_two_mul]; ring
[GOAL]
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
⊢ ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
[PROOFSTEP]
intro
[GOAL]
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
x✝ : ℝ
⊢ cos x✝ * sin x✝ = sin (2 * x✝) / 2
[PROOFSTEP]
rw [sin_two_mul]
[GOAL]
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
x✝ : ℝ
⊢ cos x✝ * sin x✝ = 2 * sin x✝ * cos x✝ / 2
[PROOFSTEP]
ring
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ 1 * ((1 + cos (2 * x)) / 2) ^ 1
[PROOFSTEP]
have h4 : ∀ d : ℝ, 2 * (2 * d) = 4 * d := fun d => by
  ring
    -- Porting note: was
      -- `simp [h1, h2.interval_integrable, integral_comp_mul_left fun x => cos x ^ 2, h3, h4]`
      -- `ring`
[GOAL]
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
d : ℝ
⊢ 2 * (2 * d) = 4 * d
[PROOFSTEP]
ring
  -- Porting note: was
    -- `simp [h1, h2.interval_integrable, integral_comp_mul_left fun x => cos x ^ 2, h3, h4]`
    -- `ring`
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ 1 * ((1 + cos (2 * x)) / 2) ^ 1
[PROOFSTEP]
simp only [pow_one, h1]
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 = ∫ (x : ℝ) in a..b, (1 - cos (2 * x) ^ 2) / 4
[PROOFSTEP]
rw [integral_div, integral_sub, integral_one]
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 = (b - a - ∫ (x : ℝ) in a..b, cos (2 * x) ^ 2) / 4
[PROOFSTEP]
simp [integral_comp_mul_left (fun x => cos x ^ 2), h3, h4]
[GOAL]
case h.e'_3
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    (b - a - 2⁻¹ * ((sin (4 * b) / 2 - sin (4 * a) / 2 + 2 * b - 2 * a) / 2)) / 4
[PROOFSTEP]
ring
[GOAL]
case h.e'_3.hf
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
⊢ IntervalIntegrable (fun x => 1) MeasureTheory.volume a b
[PROOFSTEP]
exact intervalIntegrable_const
[GOAL]
case h.e'_3.hg
a b : ℝ
n : ℕ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x => cos (2 * x) ^ 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
⊢ IntervalIntegrable (fun x => cos (2 * x) ^ 2) MeasureTheory.volume a b
[PROOFSTEP]
exact h2.intervalIntegrable a b