awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
rw : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(-(↑x : ℂ)) ^ r * Complex.exp ((↑π : ℂ) * Complex.I * r)‖
rw₁ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(-(↑x : ℂ)) ^ r‖ * ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
rw₂ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑(-x) : ℂ) ^ r‖ * ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
rw₃ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = (-x) ^ r.re * ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
rw₄ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = HPow.hPow (β := ℝ) (-x) 0 * ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
⊢ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
have rw₅ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = 1 * ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
Tactic: rw [Complex.ofReal_cpow_of_nonpos hx.2.le, norm_mul, ← Complex.ofReal_neg,
          Complex.norm_cpow_eq_rpow_re_of_pos (neg_pos.mpr hx.2), ← h',
          rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
rw : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(-(↑x : ℂ)) ^ r * Complex.exp ((↑π : ℂ) * Complex.I * r)‖
rw₁ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(-(↑x : ℂ)) ^ r‖ * ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
rw₂ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑(-x) : ℂ) ^ r‖ * ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
rw₃ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = (-x) ^ r.re * ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
rw₄ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = HPow.hPow (β := ℝ) (-x) 0 * ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
rw₅ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = 1 * ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
⊢ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
have rw₆ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
Tactic: rw [Complex.ofReal_cpow_of_nonpos hx.2.le, norm_mul, ← Complex.ofReal_neg,
          Complex.norm_cpow_eq_rpow_re_of_pos (neg_pos.mpr hx.2), ← h',
          rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioo c 0) μ
have this : ∀ x ∈ Ioo c 0, ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
Tactic: 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_cpow_eq_rpow_re_of_pos (neg_pos.mpr hx.2), ← h',
          rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Ioo c 0, ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioo c 0) μ
have neg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖) (Ioo c 0) μ
Tactic: refine IntegrableOn.congr_fun ?_ this measurableSet_Ioo
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Ioo c 0, ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖) (Ioo c 0) μ
have neg : ‖‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖‖ₑ = 0 ∨
  LT.lt (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ioo c 0) : ENNReal) (⊤ : ENNReal)
Tactic: rw [integrableOn_const_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Ioo c 0, ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
⊢ ‖‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖‖ₑ = 0 ∨
    LT.lt (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ioo c 0) : ENNReal) (⊤ : ENNReal)
have neg : LT.lt (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ioo c 0) : ENNReal) (⊤ : ENNReal)
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Ioo c 0, ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
⊢ LT.lt (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ioo c 0) : ENNReal) (⊤ : ENNReal)
have neg : LT.lt (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Icc c 0) : ENNReal) (⊤ : ENNReal)
Tactic: refine (measure_mono Set.Ioo_subset_Icc_self).trans_lt ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume a b
have suffices : ∀ (c : ℝ), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
Tactic: suffices ∀ c : ℝ, IntervalIntegrable (fun x => (x : ℂ) ^ r) volume 0 c by
    exact IntervalIntegrable.trans (this a).symm (this b)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
have rw : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) volume 0 c
Tactic: rw [← IntervalIntegrable.intervalIntegrable_norm_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
rw : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) volume 0 c
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
have rw₁ : AEStronglyMeasurable (β := ℂ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (Measure.restrict volume (Ι 0 c))
Tactic: rw [← IntervalIntegrable.intervalIntegrable_norm_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) volume 0 c
have rw : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) (Ι 0 c) volume
Tactic: rw [intervalIntegrable_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) (Ι 0 c) volume
have h₁ : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r.re) (Ι 0 c) volume
Tactic: apply IntegrableOn.congr_fun
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
h₁ : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r.re) (Ι 0 c) volume
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) (Ι 0 c) volume
have hst : EqOn (β := ℝ) (fun (x : ℝ) ↦ x ^ r.re) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) (Ι 0 c)
Tactic: apply IntegrableOn.congr_fun
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
h₁ : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r.re) (Ι 0 c) volume
hst : EqOn (β := ℝ) (fun (x : ℝ) ↦ x ^ r.re) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) (Ι 0 c)
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) (Ι 0 c) volume
have hs : MeasurableSet (Ι 0 c)
Tactic: apply IntegrableOn.congr_fun
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
h₁ : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r.re) (Ι 0 c) volume
hst : EqOn (β := ℝ) (fun (x : ℝ) ↦ x ^ r.re) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) (Ι 0 c)
hs : MeasurableSet (Ι 0 c)
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) (Ι 0 c) volume
have f : ℝ → ℝ
Tactic: apply IntegrableOn.congr_fun
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r.re) (Ι 0 c) volume
have h₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r.re) volume 0 c
Tactic: rw [← intervalIntegrable_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
h₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r.re) volume 0 c
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r.re) (Ι 0 c) volume
have rw : ℝ → ℝ
Tactic: rw [← intervalIntegrable_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ x ^ r.re) x) ((fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) x)
have hx₁ : x ∈ Ioc 0 c
Tactic: rw [uIoc_of_le hc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ x ^ r.re = ‖(↑x : ℂ) ^ r‖
have hst : x ^ r.re = x ^ r.re
Tactic: rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (Measure.restrict volume (Ι 0 c))
have refine : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (Ι 0 c)
Tactic: refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_uIoc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (Ι 0 c)
have refine : ∀ (x : ℝ) (hx : x ∈ Ι 0 c), ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) x
Tactic: refine continuousOn_of_forall_continuousAt fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) x
have hx₁ : x ∈ Ioc 0 c
Tactic: rw [uIoc_of_le hc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) x
have refine : 0 < (↑x : ℂ).re
Tactic: refine (continuousAt_cpow_const (Or.inl ?_)).comp Complex.continuous_ofReal.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ 0 < (↑x : ℂ).re
have rw : 0 < x
Tactic: rw [Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ ∀ (c : ℝ), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
have this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
Tactic: 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_cpow_eq_rpow_re_of_pos hx.1]
      · exact measurableSet_uIoc
    · refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_uIoc
      refine continuousOn_of_forall_continuousAt 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
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
have inl : ∀ (hc : 0 ≤ c), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
Tactic: rcases le_total 0 c with (hc | hc)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
inl : ∀ (hc : 0 ≤ c), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
have inr : ∀ (hc : c ≤ 0), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
Tactic: rcases le_total 0 c with (hc | hc)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
have inr : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ r) volume 0 (-c)
Tactic: rw [IntervalIntegrable.iff_comp_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ 0 ≤ -c
have linarith : -c < 0 → c - 0 + (-c - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ r) volume 0 (-c)
have m : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r) volume 0 (-c)
Tactic: have m := (this (-c) (by linarith)).const_mul (Complex.exp (π * Complex.I * r))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ι 0 (-c)) volume
⊢ 0 ≤ -c
have linarith : -c < 0 → c - 0 + (-c - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
⊢ 0 ≤ -c
have linarith : -c < 0 → c - 0 + (-c - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
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)
have inr : ∀
  (m :
    IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
      (Ioc 0 (-c)) volume),
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ r) (Ioc 0 (-c)) volume
Tactic: rw [intervalIntegrable_iff, uIoc_of_le (by linarith : 0 ≤ -c)] at m ⊢
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
⊢ IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ (↑(-x) : ℂ) ^ r) (Ioc 0 (-c)) volume
have inr : ∀ (x : ℝ) (hx : x ∈ Ioc 0 (-c)), Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r = (↑(-x) : ℂ) ^ r
Tactic: refine m.congr_fun (fun x hx => ?_) measurableSet_Ioc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
x : ℝ
hx : x ∈ Ioc 0 (-c)
⊢ -x ≤ 0
have linarith : 0 < -x → 0 - -x + (0 - x) = 0
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
x : ℝ
hx : x ∈ Ioc 0 (-c)
⊢ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r = (↑(-x) : ℂ) ^ r
have this₁ : -x ≤ 0
Tactic: have : -x ≤ 0 := by linarith [hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this_1 : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m :
  IntegrableOn (ε := ℂ) (mα := measurableSpace) (fun (x : ℝ) ↦ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r)
    (Ioc 0 (-c)) volume
x : ℝ
hx : x ∈ Ioc 0 (-c)
this : -x ≤ 0
⊢ Complex.exp ((↑π : ℂ) * Complex.I * r) * (↑x : ℂ) ^ r = (↑(-x) : ℂ) ^ r
have inr : (↑x : ℂ) ^ r * Complex.exp ((↑π : ℂ) * Complex.I * r) = (-(↑(-x) : ℂ)) ^ r * Complex.exp ((↑π : ℂ) * Complex.I * r)
Tactic: rw [Complex.ofReal_cpow_of_nonpos this, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume ↔ -1 < s.re
have refine_1 : ∀ (h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume),
  -1 < s.re
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
refine_1 :
  ∀ (h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume),
    -1 < s.re
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume ↔ -1 < s.re
have refine_2 : ∀ (h : -1 < s.re),
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : -1 < s.re
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume
have refine_2 : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) volume 0 t
Tactic: rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (a : ℝ) ↦ a ^ s.re) (Ioo 0 t) volume
have apply : EqOn (β := ℝ) (fun (a : ℝ) ↦ ‖(↑a : ℂ) ^ s‖) (fun (a : ℝ) ↦ a ^ s.re) (Ioo 0 t)
Tactic: apply (integrableOn_congr_fun _ measurableSet_Ioo).1 h.norm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume
⊢ -1 < s.re
have B : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (a : ℝ) ↦ a ^ s.re) (Ioo 0 t) volume
Tactic: have B : IntegrableOn (fun a ↦ a ^ s.re) (Ioo 0 t) := by
    apply (integrableOn_congr_fun _ measurableSet_Ioo).1 h.norm
    intro a ha
    simp [Complex.norm_cpow_eq_rpow_re_of_pos ha.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 t) volume
B : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (a : ℝ) ↦ a ^ s.re) (Ioo 0 t) volume
⊢ -1 < s.re
have refine_1 : ∀ (B : -1 < s.re), -1 < s.re
Tactic: rwa [integrableOn_Ioo_rpow_iff ht] at B
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
⊢ IntervalIntegrable log volume a b
have apply : ∀ (x : ℝ), 0 < x → IntervalIntegrable log volume 0 x
Tactic: apply intervalIntegrable_of_even (log_neg_eq_log · |>.symm)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 0 x
have hab : IntervalIntegrable log volume 0 1
Tactic: apply IntervalIntegrable.trans (b := 1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
hab : IntervalIntegrable log volume 0 1
⊢ IntervalIntegrable log volume 0 x
have hbc : IntervalIntegrable log volume 1 x
Tactic: apply IntervalIntegrable.trans (b := 1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 0 1
have hab : IntervalIntegrable (- -log) volume 0 1
Tactic: rw [← neg_neg log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable (- -log) volume 0 1
have hab : IntervalIntegrable (-log) volume 0 1
Tactic: apply IntervalIntegrable.neg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable (-log) volume 0 1
have hab : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ -(x * log x - x)) [[0, 1]]
Tactic: apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
hab : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ -(x * log x - x)) [[0, 1]]
⊢ IntervalIntegrable (-log) volume 0 1
have hab₁ : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) (Ioo (min 0 1) (max 0 1)) x → HasDerivAt (fun (x : ℝ) ↦ -(x * log x - x)) ((-log) x) x
Tactic: apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b x : ℝ
hx : 0 < x
hab : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ -(x * log x - x)) [[0, 1]]
hab₁ :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo (min 0 1) (max 0 1)) x → HasDerivAt (fun (x : ℝ) ↦ -(x * log x - x)) ((-log) x) x
⊢ IntervalIntegrable (-log) volume 0 1
have hab₂ : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo (min 0 1) (max 0 1)) x → 0 ≤ (-log) x
Tactic: apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))