awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
Goal:
b : ℂ
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
hb : 0 < b.re
w : V
⊢ 𝓕 (E := (v : V) → ℂ) (fun (v : V) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑‖v‖ : ℂ) 2)) w =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Module.finrank ℝ V) : ℂ) 2 *
      cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) (↑‖w‖ : ℂ) 2 / b)

Tactic:
simpa using fourier_gaussian_innerProductSpace' hb 0 w

Premises used: fourier_gaussian_innerProductSpace', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - -b * x ^ p) atTop atTop
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-b * x ^ p)) fun (x : ℝ) ↦ rexp (-x)

Tactic:
rw [isLittleO_exp_comp_exp_comp]

Premises used: Real.isLittleO_exp_comp_exp_comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - -b * x ^ p) atTop atTop

Tactic:
Tendsto.congr' ?_ this

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
refine : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) fun (x : ℝ) ↦ -x - -b * x ^ p
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - -b * x ^ p) atTop atTop

Tactic:
refine Tendsto.congr' ?_ this

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) fun (x : ℝ) ↦ -x - -b * x ^ p

Tactic:
eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ)) (fun x hx => ?_)

Premises used: Filter.eventuallyEq_of_mem, Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), x * (b * x ^ (p - 1) + -1) = -x - -b * x ^ p
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) fun (x : ℝ) ↦ -x - -b * x ^ p

Tactic:
refine eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ)) (fun x hx => ?_)

Premises used: Filter.eventuallyEq_of_mem, Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < x

Tactic:
rw [mem_Ioi] at hx

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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
rw : x * (b * (x ^ p / x) + -1) = -x - -b * x ^ p
⊢ x * (b * x ^ (p - 1) + -1) = -x - -b * x ^ p

Tactic:
rw [rpow_sub_one hx.ne']

Premises used: Real.rpow_sub_one, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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 / x) + -1) = -x - -b * x ^ p

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
suffices : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - -b * x ^ p) 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
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
apply : Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * x ^ (p - 1) + -1) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop

Tactic:
apply tendsto_id.atTop_mul_atTop₀

Premises used: Filter.tendsto_id, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * x ^ (p - 1) + -1) atTop atTop

Tactic:
tendsto_atTop_add_const_right atTop (-1 : ℝ) ?_

Premises used: Filter.tendsto_atTop_add_const_right, Filter.atTop, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * x ^ (p - 1)) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * x ^ (p - 1) + -1) atTop atTop

Tactic:
refine tendsto_atTop_add_const_right atTop (-1 : ℝ) ?_

Premises used: Filter.tendsto_atTop_add_const_right, Filter.atTop, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
linarith : p - 1 ≤ 0 → 1 - p + (p - 1 - 0) = 0
⊢ 0 < p - 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * x ^ (p - 1)) atTop atTop

Tactic:
exact Tendsto.const_mul_atTop hb (tendsto_rpow_atTop (by linarith))

Premises used: Filter.Tendsto.const_mul_atTop, tendsto_rpow_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
simp_rw : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℝ) x 2)) fun (x : ℝ) ↦ rexp (-x)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) fun (x : ℝ) ↦ rexp (-x)

Tactic:
simp_rw [← rpow_two]

Premises used: Real.rpow_two
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℝ) x 2)) fun (x : ℝ) ↦ rexp (-x)

Tactic:
exp_neg_mul_rpow_isLittleO_exp_neg hb one_lt_two

Premises used: exp_neg_mul_rpow_isLittleO_exp_neg, one_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℝ) x 2)) fun (x : ℝ) ↦ rexp (-x)

Tactic:
exact exp_neg_mul_rpow_isLittleO_exp_neg hb one_lt_two

Premises used: exp_neg_mul_rpow_isLittleO_exp_neg, one_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
s b p : ℝ
hp : 1 < p
hb : 0 < b
apply : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-x)) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-b * x ^ p)) 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

Premises used: Filter.atTop, Asymptotics.IsBigO.mul_isLittleO, HPow.hPow, exp_neg_mul_rpow_isLittleO_exp_neg, Asymptotics.IsLittleO.trans, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
s b p : ℝ
hp : 1 < p
hb : 0 < b
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-x)) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)

Tactic:
simpa only [mul_comm] using Real.Gamma_integrand_isLittleO s

Premises used: mul_comm, Real.Gamma_integrand_isLittleO
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
s : ℝ
simp_rw :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℝ) x 2)) fun (x : ℝ) ↦
    rexp (-(1 / 2) * x)
⊢ 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]

Premises used: Real.rpow_two
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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)

Tactic:
rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg s one_lt_two hb

Premises used: one_lt_two, rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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)

Tactic:
exact rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg s one_lt_two hb

Premises used: one_lt_two, rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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
inr :
  ∀ (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

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

Premises used: le_iff_lt_or_eq, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
⊢ ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x

Tactic:
have h_exp : ∀ x, ContinuousAt (fun x => exp (-x)) x := fun x => continuousAt_neg.rexp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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)) (Ioi 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume

Tactic:
rw [← Ioc_union_Ioi_eq_Ioi zero_le_one, integrableOn_union]

Premises used: MeasureTheory.integrableOn_union, Set.Ioc_union_Ioi_eq_Ioi, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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
inl₁ : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 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

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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)) (Icc 0 1) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioc 0 1) volume

Tactic:
rw [← integrableOn_Icc_iff_integrableOn_Ioc]

Premises used: integrableOn_Icc_iff_integrableOn_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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

Tactic:
IntegrableOn.mul_continuousOn ?_ ?_ isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, MeasureTheory.IntegrableOn.mul_continuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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
inl₁ : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x ^ p)) (Icc 0 1)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Icc 0 1) volume

Tactic:
refine IntegrableOn.mul_continuousOn ?_ ?_ isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, MeasureTheory.IntegrableOn.mul_continuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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

Tactic:
(intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp ?_

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, zero_le_one, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
inl : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ s) volume 0 1
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Icc 0 1) volume

Tactic:
refine (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp ?_

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, zero_le_one, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ s) volume 0 1

Tactic:
intervalIntegral.intervalIntegrable_rpow' hs

Premises used: intervalIntegral.intervalIntegrable_rpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ s) volume 0 1

Tactic:
exact intervalIntegral.intervalIntegrable_rpow' hs

Premises used: intervalIntegral.intervalIntegrable_rpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
x : ℝ
inl : Membership.mem (γ := Set ℝ) (Icc 0 1) x → ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x ^ p)) (Icc 0 1) x
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) x → ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x ^ p)) (Icc 0 1) x

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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

Tactic:
ContinuousAt.comp_continuousWithinAt (h_exp _) ?_

Premises used: ContinuousAt.comp_continuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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
inl : ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ p) (Icc 0 1) x
⊢ ContinuousWithinAt (Y := ℝ) ((fun (x : ℝ) ↦ rexp (-x)) ∘ fun (x : ℝ) ↦ x ^ p) (Icc 0 1) x

Tactic:
refine ContinuousAt.comp_continuousWithinAt (h_exp _) ?_

Premises used: ContinuousAt.comp_continuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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 : ℝ) ↦ x ^ p) (Icc 0 1) x

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

Premises used: ContinuousWithinAt.rpow_const, lt_trans, le_of_lt, continuousWithinAt_id, zero_lt_one, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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 : ℝ) ↦ x ^ p) (Icc 0 1) x

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

Premises used: ContinuousWithinAt.rpow_const, lt_trans, le_of_lt, continuousWithinAt_id, zero_lt_one, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
x : ℝ
_ : ∀ (r : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ r) (Ici 1) x
⊢ ∀ (r : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ r) (Ici 1) x

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
x r : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 1) x
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ r) (Ici 1) x

Tactic:
continuousWithinAt_id.rpow_const (Or.inl ?_)

Premises used: ContinuousWithinAt.rpow_const, continuousWithinAt_id, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
x r : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 1) x
⊢ id x ≠ 0

Tactic:
ne_of_gt (lt_of_lt_of_le zero_lt_one hx)

Premises used: ne_of_gt, zero_lt_one, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
x r : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 1) x
⊢ id x ≠ 0

Tactic:
exact ne_of_gt (lt_of_lt_of_le zero_lt_one hx)

Premises used: ne_of_gt, zero_lt_one, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 < p
h_exp : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x)) x
⊢ ∀ (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)
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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
⊢ 0 < 1 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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
inl₁ : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 1) volume

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 ?_)

Premises used: Asymptotics.IsLittleO.isBigO, integrable_of_isBigO_exp_neg, ContinuousOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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 : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 1) x
⊢ ContinuousWithinAt (Y := ℝ) ((fun (x : ℝ) ↦ rexp (-x)) ∘ fun (x : ℝ) ↦ x ^ p) (Ici 1) x

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

Premises used: ContinuousAt.comp_continuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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 : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 1) x
⊢ ContinuousWithinAt (Y := ℝ) ((fun (x : ℝ) ↦ rexp (-x)) ∘ fun (x : ℝ) ↦ x ^ p) (Ici 1) x

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

Premises used: ContinuousAt.comp_continuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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
h : ∀ (x : ℝ), rexp (-x ^ p) = rexp (-1 * x ^ p)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) fun (x : ℝ) ↦ rexp (-(1 / 2) * x)

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

Premises used: rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
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))
h₁ h₂ : rexp (-x ^ p) = rexp (-x ^ p)
⊢ rexp (-x ^ p) = rexp (-1 * x ^ p)

Tactic:
rw [neg_mul, one_mul]

Premises used: neg_mul, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 = p
inr : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x)) (Ioi 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x ^ p)) (Ioi 0) volume

Tactic:
simp_rw [← hp, Real.rpow_one]

Premises used: Real.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 = p
linarith : s + 1 ≤ 0 → -1 - s + (s + 1 - 0) = 0
⊢ 0 < s + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 = p
h : ∀ (x : ℝ), x ^ s * rexp (-x) = rexp (-x) * x ^ (s + 1 - 1)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-x)) (Ioi 0) volume

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

Premises used: Real.GammaIntegral_convergent
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
p s : ℝ
hs : -1 < s
hp_1 : 1 ≤ p
hp : 1 = p
x : ℝ
h : x ^ s * rexp (-x) = rexp (-x) * x ^ s
h₁ h₂ : rexp (-x) * x ^ s = rexp (-x) * x ^ s
⊢ x ^ s * rexp (-x) = rexp (-x) * x ^ (s + 1 - 1)

Tactic:
rw [add_sub_cancel_right, mul_comm]

Premises used: mul_comm, add_sub_cancel_right