awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
rw : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r) (Ioc 0 c) volume
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c

Tactic:
rw [intervalIntegrable_iff, uIoc_of_le hc]

Premises used: intervalIntegrable_iff, Set.uIoc_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioo 0 c
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) ((r + 1) * x ^ (r + 1 - 1) / (r + 1)) x

Tactic:
(Real.hasDerivAt_rpow_const (p := r + 1) (Or.inl hx.1.ne')).div_const (r + 1)

Premises used: Real.hasDerivAt_rpow_const, LT.lt.ne', And.left, HAdd.hAdd, HasDerivAt.div_const, Or.inl, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioo 0 c
h₁ : x ^ r = (r + 1) * x ^ (r + 1 - 1) / (r + 1)
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x

Tactic:
convert! (Real.hasDerivAt_rpow_const (p := r + 1) (Or.inl hx.1.ne')).div_const (r + 1) using 1

Premises used: Real.hasDerivAt_rpow_const, LT.lt.ne', And.left, HAdd.hAdd, HasDerivAt.div_const, Or.inl, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioo 0 c
linarith : r + 1 = 0 → -1 - r + (r + 1 - 0) = 0
⊢ r + 1 ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x

Tactic:
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
      simp [(by linarith : r + 1 ≠ 0)]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
apply : ∀ x ∈ Ioo 0 c, 0 ≤ x ^ r
apply₁ : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (Icc 0 c)
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r) (Ioc 0 c) volume

Tactic:
apply integrableOn_deriv_of_nonneg _ hderiv

Premises used: intervalIntegral.integrableOn_deriv_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
hx : x ∈ Ioo 0 c
⊢ 0 ≤ x ^ r

Tactic:
apply rpow_nonneg hx.1.le

Premises used: LT.lt.le, And.left, Real.rpow_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (Icc 0 c)

Tactic:
(continuousOn_id.rpow_const ?_).div_const _

Premises used: ContinuousOn.div_const, ContinuousOn.rpow_const, continuousOn_id
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
refine : ∀ x ∈ Icc 0 c, id x ≠ 0 ∨ 0 ≤ r + 1
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (Icc 0 c)

Tactic:
refine (continuousOn_id.rpow_const ?_).div_const _

Premises used: ContinuousOn.div_const, ContinuousOn.rpow_const, continuousOn_id
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
_ : x ∈ Icc 0 c → id x ≠ 0 ∨ 0 ≤ r + 1
⊢ x ∈ Icc 0 c → id x ≠ 0 ∨ 0 ≤ r + 1

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
h_1 : x ∈ Icc 0 c
h₁ : 0 ≤ r + 1
⊢ id x ≠ 0 ∨ 0 ≤ r + 1

Tactic:
right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
h_1 : x ∈ Icc 0 c
linarith : r + 1 < 0 → -1 - r + (r + 1 - 0) = 0
⊢ 0 ≤ r + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
⊢ ∀ (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_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
      simp [(by linarith : r + 1 ≠ 0)]
    apply integrableOn_deriv_of_nonneg _ hderiv
    · intro x hx; apply rpow_nonneg hx.1.le
    · refine (continuousOn_id.rpow_const ?_).div_const _; intro x _; right; linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
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
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
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
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
inr : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (-x) ^ r) volume 0 (-c)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c

Tactic:
rw [IntervalIntegrable.iff_comp_neg, neg_zero]

Premises used: IntervalIntegrable.iff_comp_neg, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
linarith : -c < 0 → c - 0 + (-c - 0) = 0
⊢ 0 ≤ -c

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) fun (x : ℝ) ↦ x ^ r) volume 0 (-c)

Tactic:
have m := (this (-c) (by linarith)).smul (cos (r * π))
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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)
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
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (-x) ^ r) volume 0 (-c)

Tactic:
rw [intervalIntegrable_iff] at m ⊢

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

Tactic:
m.congr_fun ?_ measurableSet_Ioc

Premises used: measurableSet_Ioc, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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
inr : EqOn (HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) fun (x : ℝ) ↦ x ^ r) (fun (x : ℝ) ↦ (-x) ^ r) (Ι 0 (-c))
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (-x) ^ r) (Ι 0 (-c)) volume

Tactic:
refine m.congr_fun ?_ measurableSet_Ioc

Premises used: measurableSet_Ioc, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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)
linarith : -c < 0 → c - 0 + (-c - 0) = 0
⊢ 0 ≤ -c

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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)
⊢ x ∈ Ioc 0 (-c)

Tactic:
rw [uIoc_of_le (by linarith : 0 ≤ -c)] at hx

Premises used: Set.uIoc_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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)
linarith : 0 ≤ -x → 0 - -x + (0 - x) = 0
⊢ -x < 0

Tactic:
linarith [hx.1]

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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)
⊢ HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) (fun (x : ℝ) ↦ x ^ r) x = (fun (x : ℝ) ↦ (-x) ^ r) x

Tactic:
simp only [Pi.smul_apply, 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)]

Premises used: Real.rpow_def_of_pos, Real.log_neg_eq_log, Real.rpow_def_of_neg, And.left, mul_comm, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s t : ℝ
ht : 0 < t
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume ↔ -1 < s

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s t : ℝ
ht : 0 < t
refine_1 :
  ∀ (h : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume), -1 < s
refine_2 :
  ∀ (h : -1 < s), IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume ↔ -1 < s

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s t : ℝ
ht : 0 < t
h : -1 < s
refine_2 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ s) volume 0 t
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume

Tactic:
rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]

Premises used: LT.lt.le, intervalIntegrable_iff_integrableOn_Ioo_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s t : ℝ
ht : 0 < t
h : -1 < s
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ s) volume 0 t

Tactic:
apply intervalIntegrable_rpow' h (a := 0) (b := t)

Premises used: intervalIntegral.intervalIntegrable_rpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s t : ℝ
ht : 0 < t
h : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
refine_1 :
  ∀ (h : s ≤ -1), ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
⊢ -1 < s

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 t) volume
⊢ 0 < min 1 t

Tactic:
have I : 0 < min 1 t := lt_min zero_lt_one ht
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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
apply : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 (min 1 t)), ‖a⁻¹‖ ≤ a ^ s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioo 0 (min 1 t)) volume

Tactic:
apply H'.mono' measurable_inv.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.Integrable.mono', MeasurableInv.measurable_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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
h₁ : ∀ (x : ℝ) (hx : x ∈ Ioo 0 (min 1 t)), ‖x⁻¹‖ ≤ x ^ s
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 (min 1 t)), ‖a⁻¹‖ ≤ a ^ s

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioo] with x hx

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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)
h₁ : x⁻¹ ≤ x ^ s
⊢ ‖x⁻¹‖ ≤ x ^ s

Tactic:
simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hx.1)]

Premises used: le_of_lt, norm_inv, And.left, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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)
h₁ : x < 1
⊢ x⁻¹ ≤ x ^ s

Tactic:
rwa [← Real.rpow_neg_one x, Real.rpow_le_rpow_left_iff_of_base_lt_one hx.1]

Premises used: Real.rpow_neg_one, Real.rpow_le_rpow_left_iff_of_base_lt_one, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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 < 1

Tactic:
lt_of_lt_of_le hx.2 (min_le_left _ _)

Premises used: min_le_left, And.right, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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 < 1

Tactic:
exact lt_of_lt_of_le hx.2 (min_le_left _ _)

Premises used: min_le_left, And.right, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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

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 _ _)
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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
rwa rwa₁ rwa₂ rwa₃ : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioo 0 (min 1 t)) volume
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x⁻¹) volume 0 (min 1 t)

Tactic:
rwa [intervalIntegrable_iff_integrableOn_Ioo_of_le I.le]

Premises used: LT.lt.le, intervalIntegrable_iff_integrableOn_Ioo_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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
⊢ 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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_1 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioo 0 (min 1 t)) volume
this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x⁻¹) volume 0 (min 1 t)
⊢ False

Tactic:
simp [intervalIntegrable_inv_iff, I.ne] at this

Premises used: intervalIntegrable_inv_iff, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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
neg : ∀ (h2 : ¬0 ∉ [[a, b]]), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b

Tactic:
by_cases h2 : (0 : ℝ) ∉ [[a, b]]

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

Tactic:
(continuousOn_of_forall_continuousAt fun x hx => ?_).intervalIntegrable

Premises used: continuousOn_of_forall_continuousAt, ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]
h2 : 0 ∉ [[a, b]]
pos : ∀ (x : ℝ) (hx : x ∈ [[a, b]]), ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) x
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b

Tactic:
refine (continuousOn_of_forall_continuousAt fun x hx => ?_).intervalIntegrable

Premises used: continuousOn_of_forall_continuousAt, ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]
h2 : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) x

Tactic:
Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_mem_of_not_mem hx h2)

Premises used: ne_of_mem_of_not_mem, Or.inr, Complex.continuousAt_ofReal_cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]
h2 : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) x

Tactic:
exact Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_mem_of_not_mem hx h2)

Premises used: ne_of_mem_of_not_mem, Or.inr, Complex.continuousAt_ofReal_cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]
h2 : ¬0 ∉ [[a, b]]
⊢ 0 ≤ r.re

Tactic:
rw [eq_false h2, or_false] at h

Premises used: eq_false, or_false
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
Goal:
a b : ℝ
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]
h2 : ¬0 ∉ [[a, b]]
h₁ : 0 ≤ r.re
⊢ ¬0 ∉ [[a, b]]

Tactic:
rw [eq_false h2, or_false] at h

Premises used: eq_false, or_false
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic
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
neg₁ : ∀ (h' : 0 = r.re), IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b

Tactic:
rcases lt_or_eq_of_le h with (h' | h')

Premises used: lt_or_eq_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
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b

Tactic:
(Complex.continuous_ofReal_cpow_const h').intervalIntegrable _ _

Premises used: Continuous.intervalIntegrable, Complex.continuous_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
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b

Tactic:
exact (Complex.continuous_ofReal_cpow_const h').intervalIntegrable _ _

Premises used: Continuous.intervalIntegrable, Complex.continuous_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
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ r) μ a b

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

Premises used: IntervalIntegrable.intervalIntegrable_norm_iff, Iff.mp