-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integrableOn_rpow_mul_exp_neg_rpow {p s : ℝ} (hs : -1 < s) (hp : 1 ≤ p) :
    IntegrableOn (fun x : ℝ => x ^ s * exp (- x ^ p)) (Ioi 0)

Proof state:
case inl.right.refine_2
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
⊢ (fun x => x ^ s * rexp (-x ^ p)) =o[atTop] fun x => rexp (-(1 / 2) * x)

Tactic:
convert rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg s hp (by norm_num : (0 : ℝ) < 1) using 3

Result:
case h.e'_7.h.h.e'_6
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
x✝ : ℝ
⊢ rexp (-x✝ ^ p) = rexp (-1 * x✝ ^ p)

Proof state:
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 = p
⊢ 0 < s + 1

Tactic:
linarith

Result:
no goals

Proof state:
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x

Tactic:
intro _ _ hx

Result:
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
x✝ r✝ : ℝ
hx : x✝ ∈ Ici 1
⊢ ContinuousWithinAt (fun x => x ^ r✝) (Ici 1) x✝

Proof state:
case inl.left
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioc 0 1) volume

Tactic:
rw [← integrableOn_Icc_iff_integrableOn_Ioc]

Result:
case inl.left
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Icc 0 1) volume

Proof state:
case inl
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioc 0 1) volume ∧
    IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 1) volume

Tactic:
constructor

Result:
case inl.left
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioc 0 1) volume

case inl.right
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 1) volume

Proof state:
case inr
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 = p
⊢ IntegrableOn (fun x => x ^ s * rexp (-x)) (Ioi 0) volume

Tactic:
convert Real.GammaIntegral_convergent (by linarith : 0 < s + 1) using 2

Result:
case h.e'_6.h
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 = p
x✝ : ℝ
⊢ x✝ ^ s * rexp (-x✝) = rexp (-x✝) * x✝ ^ (s + 1 - 1)

Proof state:
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
⊢ 0 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
case inl
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 0) volume

Tactic:
have h_exp : ∀ x, ContinuousAt (fun x => exp (- x)) x := fun x => continuousAt_neg.rexp

Result:
case inl
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 0) volume

Proof state:
case inl.left.refine_2
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ ContinuousOn (fun x => rexp (-x ^ p)) (Icc 0 1)

Tactic:
intro x _

Result:
case inl.left.refine_2
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
x : ℝ
a✝ : x ∈ Icc 0 1
⊢ ContinuousWithinAt (fun x => rexp (-x ^ p)) (Icc 0 1) x

Proof state:
case inl.right.refine_1
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
x : ℝ
hx : x ∈ Ici 1
⊢ ContinuousWithinAt ((fun x => rexp (-x)) ∘ fun x => x ^ p) (Ici 1) x

Tactic:
exact ContinuousAt.comp_continuousWithinAt (h_exp _) (h_rpow x p hx)

Result:
no goals

Proof state:
case inl.left.refine_1
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntervalIntegrable (fun x => x ^ s) volume 0 1

Tactic:
exact intervalIntegral.intervalIntegrable_rpow' hs

Result:
no goals

Proof state:
case h.e'_7.h.h.e'_6
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
x✝ : ℝ
⊢ rexp (-x✝ ^ p) = rexp (-1 * x✝ ^ p)

Tactic:
rw [neg_mul, one_mul]

Result:
no goals

Proof state:
case inl.right
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 1) volume

Tactic:
have h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x := by
  intro _ _ hx
  refine continuousWithinAt_id.rpow_const (Or.inl ?_)
  exact ne_of_gt (lt_of_lt_of_le zero_lt_one hx)

Result:
case inl.right
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 1) volume

Proof state:
case inl.left.refine_2
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
x : ℝ
a✝ : x ∈ Icc 0 1
⊢ ContinuousWithinAt (fun x => x ^ p) (Icc 0 1) x

Tactic:
exact continuousWithinAt_id.rpow_const (Or.inr (le_of_lt (lt_trans zero_lt_one hp)))

Result:
no goals

Proof state:
p s : ℝ
hs : -1 < s
hp : 1 ≤ p
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 0) volume

Tactic:
obtain hp | hp := le_iff_lt_or_eq.mp hp

Result:
case inl
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 0) volume

case inr
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 = p
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 0) volume

Proof state:
case inl
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 0) volume

Tactic:
rw [← Ioc_union_Ioi_eq_Ioi zero_le_one, integrableOn_union]

Result:
case inl
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioc 0 1) volume ∧
    IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 1) volume

Proof state:
case inl.right
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
⊢ IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 1) volume

Tactic:
refine integrable_of_isBigO_exp_neg (by norm_num : (0 : ℝ) < 1 / 2)
  (ContinuousOn.mul (fun x hx => h_rpow x s hx) (fun x hx => ?_)) (IsLittleO.isBigO ?_)

Result:
case inl.right.refine_1
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
x : ℝ
hx : x ∈ Ici 1
⊢ ContinuousWithinAt (fun x => rexp (-x ^ p)) (Ici 1) x

case inl.right.refine_2
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
⊢ (fun x => x ^ s * rexp (-x ^ p)) =o[atTop] fun x => rexp (-(1 / 2) * x)

Proof state:
p s : ℝ
hs : -1 < s
hp✝ : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (fun x => rexp (-x)) x
h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x
⊢ 0 < 1 / 2

Tactic:
norm_num

Result:
no goals