awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
neg : AEStronglyMeasurable (β := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (μ.restrict (Ι a b))
neg₁ : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) μ a b
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b

Tactic:
refine (IntervalIntegrable.intervalIntegrable_norm_iff ?_).mp ?_

Premises used: IntervalIntegrable.intervalIntegrable_norm_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ AEStronglyMeasurable (β := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (μ.restrict (Ι a b))

Tactic:
(measurable_of_continuousOn_compl_singleton (0 : ℝ) ?_).aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, measurable_of_continuousOn_compl_singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
neg : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) {0}ᶜ
⊢ AEStronglyMeasurable (β := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (μ.restrict (Ι a b))

Tactic:
refine (measurable_of_continuousOn_compl_singleton (0 : ℝ) ?_).aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, measurable_of_continuousOn_compl_singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) {0}ᶜ

Tactic:
continuousOn_of_forall_continuousAt fun x hx =>
      Complex.continuousAt_ofReal_cpow_const x r (Or.inr hx)

Premises used: continuousOn_of_forall_continuousAt, Or.inr, Complex.continuousAt_ofReal_cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) {0}ᶜ

Tactic:
exact continuousOn_of_forall_continuousAt fun x hx =>
      Complex.continuousAt_ofReal_cpow_const x r (Or.inr hx)

Premises used: continuousOn_of_forall_continuousAt, Or.inr, Complex.continuousAt_ofReal_cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
neg : ∀ (c : ℝ), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) μ a b

Tactic:
suffices ∀ c : ℝ, IntervalIntegrable (fun x : ℝ => ‖(x : ℂ) ^ r‖) μ 0 c from
    (this a).symm.trans (this b)
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
neg : ∀ (hc : 0 ≤ c), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
neg₁ : ∀ (hc : c < 0), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c

Tactic:
rcases le_or_gt 0 c with (hc | hc)

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) μ 0 c

Tactic:
have : IntervalIntegrable (fun _ => 1 : ℝ → ℝ) μ 0 c := intervalIntegrable_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) μ 0 c
neg :
  ∀ (this : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 1) (Ioc 0 c) μ),
    IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioc 0 c) μ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc] at this ⊢

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 1) (Ioc 0 c) μ
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioc 0 c) μ

Tactic:
IntegrableOn.congr_fun this (fun x hx => ?_) measurableSet_Ioc

Premises used: measurableSet_Ioc, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 1) (Ioc 0 c) μ
neg : ∀ (x : ℝ) (hx : x ∈ Ioc 0 c), 1 = ‖(↑x : ℂ) ^ r‖
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioc 0 c) μ

Tactic:
refine IntegrableOn.congr_fun this (fun x hx => ?_) measurableSet_Ioc

Premises used: measurableSet_Ioc, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 1) (Ioc 0 c) μ
x : ℝ
hx : x ∈ Ioc 0 c
neg : 1 = x ^ r.re
neg₁ : 1 = HPow.hPow (β := ℝ) x 0
neg₂ neg₃ : Eq (α := ℝ) 1 1
⊢ 1 = ‖(↑x : ℂ) ^ r‖

Tactic:
rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1, ← h', rpow_zero]

Premises used: Real.rpow_zero, And.left, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
neg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ c 0
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c

Tactic:
apply IntervalIntegrable.symm

Premises used: IntervalIntegrable.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
neg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioc c 0) μ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ c 0

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc.le]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
neg :
  IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) {0} μ ∧
    IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioo c 0) μ
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioc c 0) μ

Tactic:
rw [← Ioo_union_right hc, integrableOn_union, and_comm]

Premises used: MeasureTheory.integrableOn_union, and_comm, Set.Ioo_union_right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
neg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) {0} μ
neg₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioo c 0) μ
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) {0} μ ∧
    IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioo c 0) μ

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ ‖‖(↑0 : ℂ) ^ r‖‖ₑ ≠ ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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‖) {0} μ

Tactic:
exact integrableOn_singleton (by simp) <|
        isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact isCompact_singleton

Premises used: MeasureTheory.integrableOn_singleton, isCompact_singleton, MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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)‖
rw₆ rw₇ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖
⊢ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ 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]

Premises used: Iff.mpr, neg_pos, Complex.ofReal_cpow_of_nonpos, Complex.ofReal_neg, Real.rpow_zero, LT.lt.le, norm_mul, And.right, Complex.norm_cpow_eq_rpow_re_of_pos, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ ∀ 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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) μ

Tactic:
IntegrableOn.congr_fun ?_ this measurableSet_Ioo

Premises used: measurableSet_Ioo, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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‖
neg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖) (Ioo c 0) μ
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioo c 0) μ

Tactic:
refine IntegrableOn.congr_fun ?_ this measurableSet_Ioo

Premises used: measurableSet_Ioo, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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‖
neg :
  ‖‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖‖ₑ = 0 ∨
    LT.lt (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ioo c 0) : ENNReal) (⊤ : ENNReal)
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖) (Ioo c 0) μ

Tactic:
rw [integrableOn_const_iff]

Premises used: MeasureTheory.integrableOn_const_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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‖
neg : LT.lt (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ioo c 0) : ENNReal) (⊤ : ENNReal)
⊢ ‖‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖‖ₑ = 0 ∨
    LT.lt (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ioo c 0) : ENNReal) (⊤ : ENNReal)

Tactic:
right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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)

Tactic:
(measure_mono Set.Ioo_subset_Icc_self).trans_lt ?_

Premises used: Set.Ioo_subset_Icc_self, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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‖
neg : LT.lt (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Icc c 0) : ENNReal) (⊤ : ENNReal)
⊢ LT.lt (α := ENNReal) ((μ : (a : Set ℝ) → ENNReal) (Ioo c 0) : ENNReal) (⊤ : ENNReal)

Tactic:
refine (measure_mono Set.Ioo_subset_Icc_self).trans_lt ?_

Premises used: Set.Ioo_subset_Icc_self, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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) (Icc c 0) : ENNReal) (⊤ : ENNReal)

Tactic:
isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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) (Icc c 0) : ENNReal) (⊤ : ENNReal)

Tactic:
exact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume a b

Tactic:
IntervalIntegrable.trans (this a).symm (this b)

Premises used: IntervalIntegrable.symm, IntervalIntegrable.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume a b

Tactic:
exact IntervalIntegrable.trans (this a).symm (this b)

Premises used: IntervalIntegrable.symm, IntervalIntegrable.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
suffices : ∀ (c : ℝ), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume a b

Tactic:
suffices ∀ c : ℝ, IntervalIntegrable (fun x => (x : ℂ) ^ r) volume 0 c by
    exact IntervalIntegrable.trans (this a).symm (this b)
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
rw : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) volume 0 c
rw₁ :
  AEStronglyMeasurable (β := ℂ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (Measure.restrict volume (Ι 0 c))
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c

Tactic:
rw [← IntervalIntegrable.intervalIntegrable_norm_iff]

Premises used: IntervalIntegrable.intervalIntegrable_norm_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
rw : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) (Ι 0 c) volume
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) volume 0 c

Tactic:
rw [intervalIntegrable_iff]

Premises used: intervalIntegrable_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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)
f : ℝ → ℝ
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) (Ι 0 c) volume

Tactic:
apply IntegrableOn.congr_fun

Premises used: MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
h₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r.re) volume 0 c
rw : ℝ → ℝ
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r.re) (Ι 0 c) volume

Tactic:
rw [← intervalIntegrable_iff]

Premises used: intervalIntegrable_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r.re) volume 0 c

Tactic:
intervalIntegral.intervalIntegrable_rpow' h

Premises used: intervalIntegral.intervalIntegrable_rpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ι 0 c
⊢ x ∈ Ioc 0 c

Tactic:
rw [uIoc_of_le hc] at hx

Premises used: Set.uIoc_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
hst hst₁ : x ^ r.re = x ^ r.re
⊢ x ^ r.re = ‖(↑x : ℂ) ^ r‖

Tactic:
rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1]

Premises used: And.left, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ MeasurableSet (Ι 0 c)

Tactic:
measurableSet_uIoc

Premises used: measurableSet_uIoc
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ MeasurableSet (Ι 0 c)

Tactic:
exact measurableSet_uIoc

Premises used: measurableSet_uIoc
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (Measure.restrict volume (Ι 0 c))

Tactic:
ContinuousOn.aestronglyMeasurable ?_ measurableSet_uIoc

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_uIoc
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
refine : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (Ι 0 c)
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (Measure.restrict volume (Ι 0 c))

Tactic:
refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_uIoc

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_uIoc
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (Ι 0 c)

Tactic:
continuousOn_of_forall_continuousAt fun x hx => ?_

Premises used: continuousOn_of_forall_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
refine : ∀ (x : ℝ) (hx : x ∈ Ι 0 c), ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) x
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (Ι 0 c)

Tactic:
refine continuousOn_of_forall_continuousAt fun x hx => ?_

Premises used: continuousOn_of_forall_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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

Tactic:
(continuousAt_cpow_const (Or.inl ?_)).comp Complex.continuous_ofReal.continuousAt

Premises used: Continuous.continuousAt, continuousAt_cpow_const, Complex.continuous_ofReal, ContinuousAt.comp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
refine : 0 < (↑x : ℂ).re
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) x

Tactic:
refine (continuousAt_cpow_const (Or.inl ?_)).comp Complex.continuous_ofReal.continuousAt

Premises used: Continuous.continuousAt, continuousAt_cpow_const, Complex.continuous_ofReal, ContinuousAt.comp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
rw : 0 < x
⊢ 0 < (↑x : ℂ).re

Tactic:
rw [Complex.ofReal_re]

Premises used: Complex.ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ 0 < x

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ 0 < x

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ ∀ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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
inr : ∀ (hc : c ≤ 0), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) volume 0 c

Tactic:
rcases le_total 0 c with (hc | hc)

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
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

Tactic:
this c hc
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
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

Tactic:
exact this c hc