awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : 0 < x
⊢ x * (b * x ^ (p - 1) + -1) = -x - -b * x ^ p
have rw : x * (b * (x ^ p / x) + -1) = -x - -b * x ^ p
Tactic: rw [rpow_sub_one hx.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - -b * x ^ p) atTop atTop
have suffices : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
Tactic: suffices Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop by
    refine Tendsto.congr' ?_ this
    refine eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ)) (fun x hx => ?_)
    rw [mem_Ioi] at hx
    rw [rpow_sub_one hx.ne']
    field
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
have apply : Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * x ^ (p - 1) + -1) atTop atTop
Tactic: apply tendsto_id.atTop_mul_atTop₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * x ^ (p - 1) + -1) atTop atTop
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * x ^ (p - 1)) atTop atTop
Tactic: refine tendsto_atTop_add_const_right atTop (-1 : ℝ) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ 0 < p - 1
have linarith : p - 1 ≤ 0 → 1 - p + (p - 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) fun (x : ℝ) ↦ rexp (-x)
have simp_rw : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℝ) x 2)) fun (x : ℝ) ↦ rexp (-x)
Tactic: simp_rw [← rpow_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
s b p : ℝ
hp : 1 < p
hb : 0 < b
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-b * x ^ p)) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)
have apply : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-x)) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)
Tactic: apply ((isBigO_refl (fun x : ℝ => x ^ s) atTop).mul_isLittleO
      (exp_neg_mul_rpow_isLittleO_exp_neg hb hp)).trans
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) fun (x : ℝ) ↦
    rexp (-(1 / 2) * x)
have simp_rw : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℝ) x 2)) fun (x : ℝ) ↦
  rexp (-(1 / 2) * x)
Tactic: simp_rw [← rpow_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp : 1 ≤ p
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume
have inl : ∀ (hp : 1 < p),
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume
Tactic: obtain hp | hp := le_iff_lt_or_eq.mp hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp : 1 ≤ p
inl :
  ∀ (hp : 1 < p),
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume
have inr : ∀ (hp : 1 = p),
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume
Tactic: obtain hp | hp := le_iff_lt_or_eq.mp hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume
have h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
Tactic: have h_exp : ∀ x, ContinuousAt (fun x => exp (-x)) x := fun x => continuousAt_neg.rexp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume
have inl : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioc 0 1) volume ∧
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 1) volume
Tactic: rw [← Ioc_union_Ioi_eq_Ioi zero_le_one, integrableOn_union]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioc 0 1) volume ∧
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 1) volume
have inl : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioc 0 1) volume
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
inl :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioc 0 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioc 0 1) volume ∧
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 1) volume
have inl₁ : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 1) volume
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioc 0 1) volume
have inl : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Icc 0 1) volume
Tactic: rw [← integrableOn_Icc_iff_integrableOn_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Icc 0 1) volume
have inl : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Icc 0 1) volume
Tactic: refine IntegrableOn.mul_continuousOn ?_ ?_ isCompact_Icc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
inl : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Icc 0 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Icc 0 1) volume
have inl₁ : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x ^ p)) (Icc 0 1)
Tactic: refine IntegrableOn.mul_continuousOn ?_ ?_ isCompact_Icc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Icc 0 1) volume
have inl : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ s) volume 0 1
Tactic: refine (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
x : ℝ
h : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ ContinuousWithinAt (Y := ℝ) ((fun (x : ℝ) ↦ rexp (-x)) ∘ fun (x : ℝ) ↦ x ^ p) (Icc 0 1) x
have inl : ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ p) (Icc 0 1) x
Tactic: refine ContinuousAt.comp_continuousWithinAt (h_exp _) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 1) volume
have h_rpow : ∀ (x r : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ r) (Ici 1) x
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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
h_rpow :
  ∀ (x r : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ r) (Ici 1) x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 1) volume
have inl : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 1) x),
  ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x ^ p)) (Ici 1) x
Tactic: refine integrable_of_isBigO_exp_neg (by simp : (0 : ℝ) < 1 / 2)
        (ContinuousOn.mul (fun x hx => h_rpow x s hx) (fun x hx => ?_)) (IsLittleO.isBigO ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
h_rpow :
  ∀ (x r : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ r) (Ici 1) x
inl :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 1) x),
    ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x ^ p)) (Ici 1) x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 1) volume
have inl₁ : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)
Tactic: refine integrable_of_isBigO_exp_neg (by simp : (0 : ℝ) < 1 / 2)
        (ContinuousOn.mul (fun x hx => h_rpow x s hx) (fun x hx => ?_)) (IsLittleO.isBigO ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
h_rpow :
  ∀ (x r : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ r) (Ici 1) x
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)
have h : ∀ (x : ℝ), rexp (-x ^ p) = rexp (-1 * x ^ p)
Tactic: convert! rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg s hp (by simp : (0 : ℝ) < 1) using 3
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
h_rpow :
  ∀ (x r : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ r) (Ici 1) x
x : ℝ
⊢ rexp (-x ^ p) = rexp (-1 * x ^ p)
have h : rexp (-x ^ p) = rexp (-(1 * x ^ p))
Tactic: rw [neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
h_rpow :
  ∀ (x r : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ r) (Ici 1) x
x : ℝ
h : rexp (-x ^ p) = rexp (-(1 * x ^ p))
⊢ rexp (-x ^ p) = rexp (-1 * x ^ p)
have h₁ : rexp (-x ^ p) = rexp (-x ^ p)
Tactic: rw [neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 = p
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume
have inr : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x)) (Ioi 0) volume
Tactic: simp_rw [← hp, Real.rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 = p
⊢ 0 < s + 1
have linarith : s + 1 ≤ 0 → -1 - s + (s + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 = p
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x)) (Ioi 0) volume
have h : ∀ (x : ℝ), x ^ s * rexp (-x) = rexp (-x) * x ^ (s + 1 - 1)
Tactic: convert! Real.GammaIntegral_convergent (by linarith : 0 < s + 1) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 = p
x : ℝ
⊢ x ^ s * rexp (-x) = rexp (-x) * x ^ (s + 1 - 1)
have h : x ^ s * rexp (-x) = rexp (-x) * x ^ s
Tactic: rw [add_sub_cancel_right, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 = p
x : ℝ
h : x ^ s * rexp (-x) = rexp (-x) * x ^ s
⊢ x ^ s * rexp (-x) = rexp (-x) * x ^ (s + 1 - 1)
have h₁ : rexp (-x) * x ^ s = rexp (-x) * x ^ s
Tactic: rw [add_sub_cancel_right, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
p s b : ℝ
hs : -1 < s
hp : 1 ≤ p
hb : 0 < b
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-b * x ^ p)) (Ioi 0) volume
have hib : 0 < b ^ (-p⁻¹)
Tactic: have hib : 0 < b ^ (-p⁻¹) := rpow_pos_of_pos hb _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
⊢ 0 = b ^ (-p⁻¹) * 0
have rw : Eq (α := ℝ) 0 0
Tactic: rw [mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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 : ℝ) ↦ x ^ s * rexp (-b * x ^ p)) (Ioi 0) volume
have rw : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
  (fun (x : ℝ) ↦ (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)) (Ioi 0) volume
Tactic: rw [show 0 = b ^ (-p⁻¹) * 0 by rw [mul_zero], ← integrableOn_Ioi_comp_mul_left_iff _ _ hib]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
have 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)
Tactic: refine this.congr_fun (fun _ hx => ?_) measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
⊢ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p)) = (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)
have h : b ≠ 0
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₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
⊢ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p)) = (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)
have rw : p ≠ 0
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₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
⊢ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p)) = (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)
have hx₁ : 0 ≤ b
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₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
⊢ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p)) = (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)
have hx₂ : 0 ≤ b ^ (-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₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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⁻¹)
⊢ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p)) = (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)
have hy : 0 ≤ x
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₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
⊢ b ≠ 0
have linarith : b = 0 → 0 - b + (b - 0) = 0
Tactic: linarith [mem_Ioi.mp hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
⊢ p ≠ 0
have linarith : p = 0 → -1 + (1 - p) + (p - 0) = 0
Tactic: linarith [mem_Ioi.mp hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
⊢ 0 ≤ b
have linarith : b < 0 → 0 - b + (b - 0) = 0
Tactic: linarith [mem_Ioi.mp hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
⊢ 0 ≤ b ^ (-p⁻¹)
have linarith : b ^ (-p⁻¹) < 0 → HMul.hMul (α := ℝ) 1 0 - 1 * b ^ (-p⁻¹) + (1 * b ^ (-p⁻¹) - HMul.hMul (α := ℝ) 1 0) = 0
Tactic: linarith [mem_Ioi.mp hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
⊢ 0 ≤ x
have linarith : x < 0 → x - 0 + (0 - x) = 0
Tactic: linarith [mem_Ioi.mp hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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 (-b * x ^ p)) (Ioi 0) volume
have suffices : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
have refine : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p))
  (Measure.restrict volume (Ioi 0))
Tactic: refine Integrable.const_mul ?_ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
have simp_rw : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℝ) x 2))
  (Ioi 0) volume
Tactic: simp_rw [← rpow_two]