-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integrable_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (hs : -1 < s) :
    Integrable fun x : ℝ => x ^ s * exp (-b * x ^ 2)

Proof state:
case hf.hf
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ Measurable fun x => (-x) ^ s * rexp (-b * x ^ 2)

Tactic:
exact (measurable_id'.neg.pow measurable_const).mul
  ((measurable_id'.pow measurable_const).const_mul (-b)).exp

Result:
no goals

Proof state:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ Integrable (fun x => x ^ s * rexp (-b * x ^ 2)) volume

Tactic:
rw [← integrableOn_univ, ← @Iio_union_Ici _ _ (0 : ℝ), integrableOn_union,
  integrableOn_Ici_iff_integrableOn_Ioi]

Result:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Iio 0) volume ∧
    IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Ioi 0) volume

Proof state:
case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖(-a) ^ s * rexp (-b * a ^ 2)‖ ≤ a ^ s * rexp (-b * a ^ 2)

Tactic:
filter_upwards [ae_restrict_mem this] with x hx

Result:
case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
⊢ ‖(-x) ^ s * rexp (-b * x ^ 2)‖ ≤ x ^ s * rexp (-b * x ^ 2)

Proof state:
case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ ‖(-x) ^ s * rexp (-b * x ^ 2)‖ ≤ x ^ s * rexp (-b * x ^ 2)

Tactic:
rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg (exp_pos _).le]

Result:
case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ |(-x) ^ s| * rexp (-b * x ^ 2) ≤ x ^ s * rexp (-b * x ^ 2)

Proof state:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Iio 0) volume

Tactic:
rw [← (Measure.measurePreserving_neg (volume : Measure ℝ)).integrableOn_comp_preimage
    (Homeomorph.neg ℝ).measurableEmbedding]

Result:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn ((fun x => x ^ s * rexp (-b * x ^ 2)) ∘ Neg.neg) (Neg.neg ⁻¹' Iio 0) volume

Proof state:
case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖(-a) ^ s * rexp (-b * a ^ 2)‖ ≤ a ^ s * rexp (-b * a ^ 2)

Tactic:
have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi

Result:
case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖(-a) ^ s * rexp (-b * a ^ 2)‖ ≤ a ^ s * rexp (-b * a ^ 2)

Proof state:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Iio 0) volume ∧
    IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Ioi 0) volume

Tactic:
refine ⟨?_, integrableOn_rpow_mul_exp_neg_mul_sq hb hs⟩

Result:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Iio 0) volume

Proof state:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn ((fun x => x ^ s * rexp (-b * x ^ 2)) ∘ Neg.neg) (Neg.neg ⁻¹' Iio 0) volume

Tactic:
simp only [Function.comp_def, neg_sq, neg_preimage, neg_Iio, neg_neg, neg_zero]

Result:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x => (-x) ^ s * rexp (-b * x ^ 2)) (Ioi 0) volume

Proof state:
case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
⊢ ‖(-x) ^ s * rexp (-b * x ^ 2)‖ ≤ x ^ s * rexp (-b * x ^ 2)

Tactic:
have h'x : 0 ≤ x := le_of_lt hx

Result:
case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ ‖(-x) ^ s * rexp (-b * x ^ 2)‖ ≤ x ^ s * rexp (-b * x ^ 2)

Proof state:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x => (-x) ^ s * rexp (-b * x ^ 2)) (Ioi 0) volume

Tactic:
apply Integrable.mono' (integrableOn_rpow_mul_exp_neg_mul_sq hb hs)

Result:
case hf
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ AEStronglyMeasurable (fun x => (-x) ^ s * rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))

case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖(-a) ^ s * rexp (-b * a ^ 2)‖ ≤ a ^ s * rexp (-b * a ^ 2)

Proof state:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ |(-x) ^ s| ≤ x ^ s

Tactic:
simpa [abs_of_nonneg h'x] using abs_rpow_le_abs_rpow (-x) s

Result:
no goals

Proof state:
case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ |(-x) ^ s| * rexp (-b * x ^ 2) ≤ x ^ s * rexp (-b * x ^ 2)

Tactic:
apply mul_le_mul_of_nonneg_right _ (exp_pos _).le

Result:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ |(-x) ^ s| ≤ x ^ s

Proof state:
case hf
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ AEStronglyMeasurable (fun x => (-x) ^ s * rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))

Tactic:
apply Measurable.aestronglyMeasurable

Result:
case hf.hf
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ Measurable fun x => (-x) ^ s * rexp (-b * x ^ 2)