awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
⊢ 0 < b ^ (-p⁻¹)

Tactic:
have hib : 0 < b ^ (-p⁻¹) := rpow_pos_of_pos hb _
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
rw rw₁ : Eq (α := ℝ) 0 0
⊢ 0 = b ^ (-p⁻¹) * 0

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
rw :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)) (Ioi 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-b * x ^ p)) (Ioi 0) volume

Tactic:
rw [show 0 = b ^ (-p⁻¹) * 0 by rw [mul_zero], ← integrableOn_Ioi_comp_mul_left_iff _ _ hib]

Premises used: MeasureTheory.integrableOn_Ioi_comp_mul_left_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)) (Ioi 0) volume

Tactic:
this.congr_fun (fun _ hx => ?_) measurableSet_Ioi

Premises used: measurableSet_Ioi, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p)) = (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)) (Ioi 0) volume

Tactic:
refine this.congr_fun (fun _ hx => ?_) measurableSet_Ioi

Premises used: measurableSet_Ioi, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
h : b ≠ 0
rw : p ≠ 0
hx₁ : 0 ≤ b
hx₂ : 0 ≤ b ^ (-p⁻¹)
hy : 0 ≤ x
hx₃ : 0 ≤ b ^ (-p⁻¹)
hy₁ : 0 ≤ x
⊢ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p)) = (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)

Tactic:
rw [← mul_assoc, mul_rpow, mul_rpow, ← rpow_mul (z := p), neg_mul, neg_mul, inv_mul_cancel₀,
      rpow_neg_one, mul_inv_cancel_left₀]

Premises used: mul_inv_cancel_left₀, Real.rpow_neg_one, mul_assoc, Real.mul_rpow, neg_mul, Real.rpow_mul, inv_mul_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
linarith : b = 0 → 0 - b + (b - 0) = 0
⊢ b ≠ 0

Tactic:
linarith [mem_Ioi.mp hx]

Premises used: Set.mem_Ioi, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
linarith : p = 0 → -1 + (1 - p) + (p - 0) = 0
⊢ p ≠ 0

Tactic:
linarith [mem_Ioi.mp hx]

Premises used: Set.mem_Ioi, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
linarith : b < 0 → 0 - b + (b - 0) = 0
⊢ 0 ≤ b

Tactic:
linarith [mem_Ioi.mp hx]

Premises used: Set.mem_Ioi, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
linarith : b ^ (-p⁻¹) < 0 → HMul.hMul (α := ℝ) 1 0 - 1 * b ^ (-p⁻¹) + (1 * b ^ (-p⁻¹) - HMul.hMul (α := ℝ) 1 0) = 0
⊢ 0 ≤ b ^ (-p⁻¹)

Tactic:
linarith [mem_Ioi.mp hx]

Premises used: Set.mem_Ioi, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
linarith : x < 0 → x - 0 + (0 - x) = 0
⊢ 0 ≤ x

Tactic:
linarith [mem_Ioi.mp hx]

Premises used: Set.mem_Ioi, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
suffices :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-b * x ^ p)) (Ioi 0) volume

Tactic:
suffices IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * exp (-x ^ p))) (Ioi 0) by
    rw [show 0 = b ^ (-p⁻¹) * 0 by rw [mul_zero], ← integrableOn_Ioi_comp_mul_left_iff _ _ hib]
    refine this.congr_fun (fun _ hx => ?_) measurableSet_Ioi
    rw [← mul_assoc, mul_rpow, mul_rpow, ← rpow_mul (z := p), neg_mul, neg_mul, inv_mul_cancel₀,
      rpow_neg_one, mul_inv_cancel_left₀]
    all_goals linarith [mem_Ioi.mp hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume

Tactic:
Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.IntegrableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
refine :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p))
    (Measure.restrict volume (Ioi 0))
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume

Tactic:
refine Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume

Tactic:
integrableOn_rpow_mul_exp_neg_rpow hs hp

Premises used: integrableOn_rpow_mul_exp_neg_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume

Tactic:
exact integrableOn_rpow_mul_exp_neg_rpow hs hp

Premises used: integrableOn_rpow_mul_exp_neg_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
simp_rw :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℝ) x 2)) (Ioi 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0) volume

Tactic:
simp_rw [← rpow_two]

Premises used: Real.rpow_two
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℝ) x 2)) (Ioi 0) volume

Tactic:
integrableOn_rpow_mul_exp_neg_mul_rpow hs one_le_two hb

Premises used: one_le_two, integrableOn_rpow_mul_exp_neg_mul_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℝ) x 2)) (Ioi 0) volume

Tactic:
exact integrableOn_rpow_mul_exp_neg_mul_rpow hs one_le_two hb

Premises used: one_le_two, integrableOn_rpow_mul_exp_neg_mul_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
rw :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Iio 0) volume ∧
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0) volume
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) volume

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

Premises used: Set.Iio_union_Ici, MeasureTheory.integrableOn_union, integrableOn_Ici_iff_integrableOn_Ioi, MeasureTheory.integrableOn_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Iio 0) volume ∧
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0) volume

Tactic:
⟨?_, integrableOn_rpow_mul_exp_neg_mul_sq hb hs⟩

Premises used: And.intro, integrableOn_rpow_mul_exp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
refine :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Iio 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Iio 0) volume ∧
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0) volume

Tactic:
refine ⟨?_, integrableOn_rpow_mul_exp_neg_mul_sq hb hs⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
rw :
  IntegrableOn (α := ℝ) (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    ((fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) ∘ Neg.neg) (Neg.neg ⁻¹' Iio 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Iio 0) volume

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

Premises used: MeasureTheory.Measure.measurePreserving_neg, MeasureTheory.MeasurePreserving.integrableOn_comp_preimage, Real, Homeomorph.measurableEmbedding, Homeomorph.neg, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
simp :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0) volume
⊢ IntegrableOn (α := ℝ) (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    ((fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) ∘ Neg.neg) (Neg.neg ⁻¹' Iio 0) volume

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

Premises used: neg_sq, Function.comp_def, Set.neg_Iio, Set.neg_preimage, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
hf :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Measure.restrict volume (Ioi 0))
h :
  ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi 0),
    ‖(-a) ^ s * rexp (-b * HPow.hPow (β := ℕ) a 2)‖ ≤ a ^ s * rexp (-b * HPow.hPow (β := ℕ) a 2)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0) volume

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

Premises used: MeasureTheory.Integrable.mono', integrableOn_rpow_mul_exp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
hf : Measurable (β := ℝ) fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Measure.restrict volume (Ioi 0))

Tactic:
apply Measurable.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)

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

Premises used: Measurable.mul, Measurable.neg, measurable_id', measurable_const, Measurable.const_mul, Measurable.exp, Measurable.pow, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)

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

Premises used: Measurable.mul, Measurable.neg, measurable_id', measurable_const, Measurable.const_mul, Measurable.exp, Measurable.pow, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ MeasurableSet (α := ℝ) (Ioi 0)

Tactic:
have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (α := ℝ) (Ioi 0)
h :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    ‖(-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)‖ ≤ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi 0),
    ‖(-a) ^ s * rexp (-b * HPow.hPow (β := ℕ) a 2)‖ ≤ a ^ s * rexp (-b * HPow.hPow (β := ℕ) a 2)

Tactic:
filter_upwards [ae_restrict_mem this] with x hx

Premises used: MeasureTheory.ae_restrict_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (α := ℝ) (Ioi 0)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 ≤ x

Tactic:
have h'x : 0 ≤ x := le_of_lt hx
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (α := ℝ) (Ioi 0)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
h'x : 0 ≤ x
h : |(-x) ^ s| * rexp (-b * HPow.hPow (β := ℕ) x 2) ≤ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)
⊢ ‖(-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)‖ ≤ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)

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

Premises used: abs_mul, LT.lt.le, abs_of_nonneg, Real.norm_eq_abs, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (α := ℝ) (Ioi 0)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
h'x : 0 ≤ x
apply : |(-x) ^ s| ≤ x ^ s
⊢ |(-x) ^ s| * rexp (-b * HPow.hPow (β := ℕ) x 2) ≤ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)

Tactic:
apply mul_le_mul_of_nonneg_right _ (exp_pos _).le

Premises used: LT.lt.le, mul_le_mul_of_nonneg_right, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (α := ℝ) (Ioi 0)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
h'x : 0 ≤ x
⊢ |(-x) ^ s| ≤ x ^ s

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

Premises used: Real.abs_rpow_le_abs_rpow, abs_of_nonneg, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
⊢ LT.lt (α := ℝ) (-1) 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) volume

Tactic:
simpa using integrable_rpow_mul_exp_neg_mul_sq hb (by simp : (-1 : ℝ) < 0)

Premises used: integrable_rpow_mul_exp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
      (Ioi 0) volume ↔
    0 < b

Tactic:
⟨fun h => ?_, fun h => (integrable_exp_neg_mul_sq h).integrableOn⟩

Premises used: Iff.intro, MeasureTheory.Integrable.integrableOn, integrable_exp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
refine :
  ∀
    (h :
      IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
        (Ioi 0) volume),
    0 < b
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
      (Ioi 0) volume ↔
    0 < b

Tactic:
refine ⟨fun h => ?_, fun h => (integrable_exp_neg_mul_sq h).integrableOn⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
h :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Ioi 0) volume
by_contra! : ∀ (hb : b ≤ 0), False
⊢ 0 < b

Tactic:
by_contra! hb
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
h :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Ioi 0) volume
hb : b ≤ 0
apply : ∀ (x : ℝ), 1 ≤ (↑‖rexp (-b * HPow.hPow (β := ℕ) x 2)‖₊ : ENNReal)
⊢ ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, (↑‖rexp (-b * HPow.hPow (β := ℕ) x 2)‖₊ : ENNReal)

Tactic:
apply lintegral_mono (fun x ↦ _)

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
h :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Ioi 0) volume
hb : b ≤ 0
simp : ∀ (x : ℝ), b * HPow.hPow (β := ℕ) x 2 ≤ 0
⊢ ∀ (x : ℝ), 1 ≤ (↑‖rexp (-b * HPow.hPow (β := ℕ) x 2)‖₊ : ENNReal)

Tactic:
simp only [neg_mul, ENNReal.one_le_coe_iff, ← toNNReal_one, toNNReal_le_iff_le_coe,
      Real.norm_of_nonneg (exp_pos _).le, coe_nnnorm, one_le_exp_iff, Right.nonneg_neg_iff]

Premises used: Real.one_le_exp_iff, Right.nonneg_neg_iff, LT.lt.le, Real.toNNReal_one, coe_nnnorm, Real.toNNReal_le_iff_le_coe, neg_mul, ENNReal.one_le_coe_iff, Real.norm_of_nonneg, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
h :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Ioi 0) volume
hb : b ≤ 0
⊢ ∀ (x : ℝ), b * HPow.hPow (β := ℕ) x 2 ≤ 0

Tactic:
fun x ↦ mul_nonpos_of_nonpos_of_nonneg hb (sq_nonneg x)

Premises used: mul_nonpos_of_nonpos_of_nonneg, sq_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
h :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Ioi 0) volume
hb : b ≤ 0
⊢ ∀ (x : ℝ), b * HPow.hPow (β := ℕ) x 2 ≤ 0

Tactic:
exact fun x ↦ mul_nonpos_of_nonpos_of_nonneg hb (sq_nonneg x)

Premises used: mul_nonpos_of_nonpos_of_nonneg, sq_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
h :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Ioi 0) volume
hb : b ≤ 0
⊢ ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, (↑‖rexp (-b * HPow.hPow (β := ℕ) x 2)‖₊ : ENNReal)

Tactic:
have : ∫⁻ _ : ℝ in Ioi 0, 1 ≤ ∫⁻ x : ℝ in Ioi 0, ‖exp (-b * x ^ 2)‖₊ := by
    apply lintegral_mono (fun x ↦ _)
    simp only [neg_mul, ENNReal.one_le_coe_iff, ← toNNReal_one, toNNReal_le_iff_le_coe,
      Real.norm_of_nonneg (exp_pos _).le, coe_nnnorm, one_le_exp_iff, Right.nonneg_neg_iff]
    exact fun x ↦ mul_nonpos_of_nonpos_of_nonneg hb (sq_nonneg x)
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
h :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Ioi 0) volume
hb : b ≤ 0
this : ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, (↑‖rexp (-b * HPow.hPow (β := ℕ) x 2)‖₊ : ENNReal)
⊢ False

Tactic:
simpa using this.trans_lt h.2

Premises used: And.right, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) volume ↔ 0 < b

Tactic:
⟨fun h => integrableOn_Ioi_exp_neg_mul_sq_iff.mp h.integrableOn, integrable_exp_neg_mul_sq⟩

Premises used: Iff.intro, integrableOn_Ioi_exp_neg_mul_sq_iff, Iff.mp, MeasureTheory.Integrable.integrableOn, integrable_exp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
⊢ LT.lt (α := ℝ) (-1) 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * rexp (-b * HPow.hPow (β := ℕ) x 2)) volume

Tactic:
simpa using integrable_rpow_mul_exp_neg_mul_sq hb (by simp : (-1 : ℝ) < 1)

Premises used: integrable_rpow_mul_exp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
x : ℝ
rw : rexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₁ : rexp (-b * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₂ : rexp ((↑(HPow.hPow (β := ℕ) x 2) : ℂ) * -b).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₃ : rexp (HPow.hPow (β := ℕ) x 2 * (-b).re) = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₄ : rexp (HPow.hPow (β := ℕ) x 2 * -b.re) = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₅ rw₆ : rexp (-b.re * HPow.hPow (β := ℕ) x 2) = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = rexp (-b.re * HPow.hPow (β := ℕ) x 2)

Tactic:
rw [norm_exp, ← ofReal_pow, mul_comm (-b) _, re_ofReal_mul, neg_re, mul_comm]

Premises used: Complex.neg_re, Complex.norm_exp, mul_comm, Complex.ofReal_pow, Neg.neg, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume

Tactic:
fun_prop