awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntervalIntegrable (HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) fun (x : ℝ) ↦ x ^ r) volume 0 (-c)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (-x) ^ r) volume 0 (-c)
have inr : ∀
  (m :
    IntegrableOn (mα := measurableSpace) (HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) fun (x : ℝ) ↦ x ^ r) (Ι 0 (-c))
      volume),
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (-x) ^ r) (Ι 0 (-c)) volume
Tactic: rw [intervalIntegrable_iff] at m ⊢
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (mα := measurableSpace) (HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) fun (x : ℝ) ↦ x ^ r) (Ι 0 (-c)) volume
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (-x) ^ r) (Ι 0 (-c)) volume
have inr : EqOn (HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) fun (x : ℝ) ↦ x ^ r) (fun (x : ℝ) ↦ (-x) ^ r) (Ι 0 (-c))
Tactic: refine m.congr_fun ?_ measurableSet_Ioc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (mα := measurableSpace) (HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) fun (x : ℝ) ↦ x ^ r) (Ι 0 (-c)) volume
x : ℝ
hx : x ∈ Ι 0 (-c)
⊢ 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
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (mα := measurableSpace) (HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) fun (x : ℝ) ↦ x ^ r) (Ι 0 (-c)) volume
x : ℝ
hx : x ∈ Ι 0 (-c)
⊢ HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) (fun (x : ℝ) ↦ x ^ r) x = (fun (x : ℝ) ↦ (-x) ^ r) x
have hx₁ : x ∈ Ioc 0 (-c)
Tactic: rw [uIoc_of_le (by linarith : 0 ≤ -c)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (mα := measurableSpace) (HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) fun (x : ℝ) ↦ x ^ r) (Ι 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 (goal)
Goal:
s t : ℝ
ht : 0 < t
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume ↔ -1 < s
have refine_1 : ∀ (h : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume), -1 < s
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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume ↔ -1 < s
have refine_2 : ∀ (h : -1 < s), 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
⊢ 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
⊢ -1 < s
have refine_1 : ∀ (h : s ≤ -1), ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
⊢ False
have I : 0 < min 1 t
Tactic: have I : 0 < min 1 t := lt_min zero_lt_one ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
⊢ False
have H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 (min 1 t)) volume
Tactic: have H' : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 (min 1 t)) :=
    H.mono (Set.Ioo_subset_Ioo le_rfl (min_le_right _ _)) le_rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 (min 1 t)) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioo 0 (min 1 t)) volume
have apply : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 (min 1 t)), ‖a⁻¹‖ ≤ a ^ s
Tactic: apply H'.mono' measurable_inv.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 (min 1 t)) volume
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 (min 1 t)), ‖a⁻¹‖ ≤ a ^ s
have h₁ : ∀ (x : ℝ) (hx : x ∈ Ioo 0 (min 1 t)), ‖x⁻¹‖ ≤ x ^ s
Tactic: filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 (min 1 t)) volume
x : ℝ
hx : x ∈ Ioo 0 (min 1 t)
⊢ ‖x⁻¹‖ ≤ x ^ s
have h₁ : x⁻¹ ≤ x ^ s
Tactic: simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hx.1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 (min 1 t)) volume
x : ℝ
hx : x ∈ Ioo 0 (min 1 t)
⊢ x⁻¹ ≤ x ^ s
have h₁ : x < 1
Tactic: rwa [← Real.rpow_neg_one x, Real.rpow_le_rpow_left_iff_of_base_lt_one hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 (min 1 t)) volume
⊢ False
have this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioo 0 (min 1 t)) volume
Tactic: have : IntegrableOn (fun x ↦ x⁻¹) (Ioo 0 (min 1 t)) := by
    apply H'.mono' measurable_inv.aestronglyMeasurable
    filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx
    simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hx.1)]
    rwa [← Real.rpow_neg_one x, Real.rpow_le_rpow_left_iff_of_base_lt_one hx.1]
    exact lt_of_lt_of_le hx.2 (min_le_left _ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 (min 1 t)) volume
this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioo 0 (min 1 t)) volume
⊢ False
have this₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x⁻¹) volume 0 (min 1 t)
Tactic: have : IntervalIntegrable (fun x ↦ x⁻¹) volume 0 (min 1 t) := by
    rwa [intervalIntegrable_iff_integrableOn_Ioo_of_le I.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
have pos : ∀ (h2 : 0 ∉ [[a, b]]), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
Tactic: by_cases h2 : (0 : ℝ) ∉ [[a, b]]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]
pos : ∀ (h2 : 0 ∉ [[a, b]]), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
have neg : ∀ (h2 : ¬0 ∉ [[a, b]]), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
Tactic: by_cases h2 : (0 : ℝ) ∉ [[a, b]]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]
h2 : 0 ∉ [[a, b]]
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
have pos : ∀ (x : ℝ) (hx : x ∈ [[a, b]]), ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) x
Tactic: refine (continuousOn_of_forall_continuousAt fun x hx => ?_).intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]
h2 : ¬0 ∉ [[a, b]]
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
have h₁ : 0 ≤ r.re
Tactic: rw [eq_false h2, or_false] at h
Cleared hypotheses: h, h2
-- 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]]
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
have neg : ∀ (h' : 0 < r.re), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
Tactic: rcases lt_or_eq_of_le h with (h' | h')
-- 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]]
neg : ∀ (h' : 0 < r.re), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
have neg₁ : ∀ (h' : 0 = r.re), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
Tactic: rcases lt_or_eq_of_le h with (h' | h')
-- 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
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
have neg : AEStronglyMeasurable (β := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (μ.restrict (Ι a b))
Tactic: refine (IntervalIntegrable.intervalIntegrable_norm_iff ?_).mp ?_
-- 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
neg : AEStronglyMeasurable (β := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (μ.restrict (Ι a b))
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
have neg₁ : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) μ a b
Tactic: refine (IntervalIntegrable.intervalIntegrable_norm_iff ?_).mp ?_
-- 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
⊢ AEStronglyMeasurable (β := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) (μ.restrict (Ι a b))
have neg : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) {0}ᶜ
Tactic: refine (measurable_of_continuousOn_compl_singleton (0 : ℝ) ?_).aestronglyMeasurable
-- 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
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ r‖) μ a b
have neg : ∀ (c : ℝ), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
Tactic: suffices ∀ c : ℝ, IntervalIntegrable (fun x : ℝ => ‖(x : ℂ) ^ r‖) μ 0 c from
    (this a).symm.trans (this b)
-- 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 : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
have neg : ∀ (hc : 0 ≤ c), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
Tactic: rcases le_or_gt 0 c with (hc | hc)
-- 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 : ℝ
neg : ∀ (hc : 0 ≤ c), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
have neg₁ : ∀ (hc : c < 0), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
Tactic: rcases le_or_gt 0 c with (hc | hc)
-- 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 : 0 ≤ c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
have this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) μ 0 c
Tactic: have : IntervalIntegrable (fun _ => 1 : ℝ → ℝ) μ 0 c := intervalIntegrable_const
-- 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 : 0 ≤ c
this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) μ 0 c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
have neg : ∀ (this : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 1) (Ioc 0 c) μ),
  IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioc 0 c) μ
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc] at this ⊢
Cleared hypotheses: this
-- 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 : 0 ≤ c
this : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 1) (Ioc 0 c) μ
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioc 0 c) μ
have neg : ∀ (x : ℝ) (hx : x ∈ Ioc 0 c), 1 = ‖(↑x : ℂ) ^ r‖
Tactic: refine IntegrableOn.congr_fun this (fun x hx => ?_) measurableSet_Ioc
-- 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 : 0 ≤ c
this : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 1) (Ioc 0 c) μ
x : ℝ
hx : x ∈ Ioc 0 c
⊢ 1 = ‖(↑x : ℂ) ^ r‖
have neg : 1 = x ^ r.re
Tactic: rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1, ← h', rpow_zero]
-- 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 : 0 ≤ c
this : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 1) (Ioc 0 c) μ
x : ℝ
hx : x ∈ Ioc 0 c
neg : 1 = x ^ r.re
⊢ 1 = ‖(↑x : ℂ) ^ r‖
have neg₁ : 1 = HPow.hPow (β := ℝ) x 0
Tactic: rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1, ← h', rpow_zero]
-- 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 : 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
⊢ 1 = ‖(↑x : ℂ) ^ r‖
have neg₂ : Eq (α := ℝ) 1 1
Tactic: rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1, ← h', rpow_zero]
-- 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
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ 0 c
have neg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ c 0
Tactic: apply IntervalIntegrable.symm
-- 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
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) μ c 0
have neg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioc c 0) μ
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc.le]
-- 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
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioc c 0) μ
have neg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) {0} μ ∧
  IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioo c 0) μ
Tactic: rw [← Ioo_union_right hc, integrableOn_union, and_comm]
-- 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
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) {0} μ ∧
    IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioo c 0) μ
have neg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) {0} μ
Tactic: constructor
-- 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
neg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) {0} μ
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) {0} μ ∧
    IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioo c 0) μ
have neg₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ r‖) (Ioo c 0) μ
Tactic: constructor
-- 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
⊢ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
have rw : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(-(↑x : ℂ)) ^ 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 (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)‖
⊢ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
have rw₁ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(-(↑x : ℂ)) ^ 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 (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)‖
⊢ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
have rw₂ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑(-x) : ℂ) ^ 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 (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)‖
⊢ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
have rw₃ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = (-x) ^ r.re * ‖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)‖
⊢ ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = ‖(↑x : ℂ) ^ r‖
have rw₄ : ‖Complex.exp ((↑π : ℂ) * Complex.I * r)‖ = HPow.hPow (β := ℝ) (-x) 0 * ‖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]