awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  ∀ (c : ℝ),
    Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
t1 :
  Tendsto (β := ℂ) (fun (i : ℝ) ↦ ∫ (x : ℝ) in 0..id i, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
⊢ IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) (Iic 0)
    volume

Tactic:
apply (integrable_cexp_neg_mul_sq hb).integrableOn

Premises used: MeasureTheory.Integrable.integrableOn, integrable_cexp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  ∀ (c : ℝ),
    Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
t1 :
  Tendsto (β := ℂ) (fun (i : ℝ) ↦ ∫ (x : ℝ) in 0..id i, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
⊢ Tendsto (β := ℂ) (fun (c : ℝ) ↦ ∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))

Tactic:
have t2 :
    Tendsto (fun c : ℝ => ∫ x : ℝ in (0 : ℝ)..c, cexp (-b * (x : ℂ) ^ 2)) atTop
      (𝓝 (∫ x : ℝ in Iic 0, cexp (-b * (x : ℂ) ^ 2))) := by
    simp_rw [this]
    refine intervalIntegral_tendsto_integral_Iic _ ?_ tendsto_neg_atTop_atBot
    apply (integrable_cexp_neg_mul_sq hb).integrableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  ∀ (c : ℝ),
    Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
t1 :
  Tendsto (β := ℂ) (fun (i : ℝ) ↦ ∫ (x : ℝ) in 0..id i, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
t2 :
  Tendsto (β := ℂ) (fun (c : ℝ) ↦ ∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))

Tactic:
tendsto_nhds_unique t2 t1

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  ∀ (c : ℝ),
    Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
t1 :
  Tendsto (β := ℂ) (fun (i : ℝ) ↦ ∫ (x : ℝ) in 0..id i, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
t2 :
  Tendsto (β := ℂ) (fun (c : ℝ) ↦ ∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))

Tactic:
exact tendsto_nhds_unique t2 t1

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
inl :
  ∀ (hb : b ≤ 0),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-b * HPow.hPow (β := ℕ) x 2)) =
      √(π / b) / 2
inr :
  ∀ (hb : 0 < b),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-b * HPow.hPow (β := ℕ) x 2)) =
      √(π / b) / 2
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-b * HPow.hPow (β := ℕ) x 2)) =
    √(π / b) / 2

Tactic:
rcases le_or_gt b 0 with (hb | hb)

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : b ≤ 0
inl : π / b ≤ 0
inl₁ :
  ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
      (Measure.restrict volume (Ioi 0))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-b * HPow.hPow (β := ℕ) x 2)) =
    √(π / b) / 2

Tactic:
rw [integral_undef, sqrt_eq_zero_of_nonpos, zero_div]

Premises used: MeasureTheory.integral_undef, zero_div, Real.sqrt_eq_zero_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : b ≤ 0
inl :
  ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
      (Ioi 0) volume
inl₁ : ¬0 < b
inl₂ inl₃ inl₄ inl₅ : b ≤ 0
⊢ ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
      (Measure.restrict volume (Ioi 0))

Tactic:
rwa [← IntegrableOn, integrableOn_Ioi_exp_neg_mul_sq_iff, not_lt]

Premises used: MeasureTheory.IntegrableOn, not_lt, integrableOn_Ioi_exp_neg_mul_sq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
inr :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ)) =
    (↑(√(π / b) / 2) : ℂ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-b * HPow.hPow (β := ℕ) x 2)) =
    √(π / b) / 2

Tactic:
rw [← RCLike.ofReal_inj (K := ℂ), ← integral_ofReal, ← RCLike.algebraMap_eq_ofReal,
    coe_algebraMap]

Premises used: RCLike.ofReal_inj, RCLike.algebraMap_eq_ofReal, Complex.coe_algebraMap, integral_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
h : ∀ (x : ℝ), (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
h₁ : (↑(√(π / b) / 2) : ℂ) = ((↑π : ℂ) / (↑b : ℂ)) ^ (1 / 2) / 2
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ)) =
    (↑(√(π / b) / 2) : ℂ)

Tactic:
convert! integral_gaussian_complex_Ioi (by rwa [ofReal_re] : 0 < (b : ℂ).re)

Premises used: integral_gaussian_complex_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
x : ℝ
⊢ (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
h : (↑(π / b) : ℂ) ^ (↑(1 / 2) : ℂ) / (↑2 : ℂ) = (↑(π / b) : ℂ) ^ (1 / 2) / 2
h₁ : 0 ≤ π / b
⊢ (↑(√(π / b) / 2) : ℂ) = ((↑π : ℂ) / (↑b : ℂ)) ^ (1 / 2) / 2

Tactic:
rw [sqrt_eq_rpow, ← ofReal_div, ofReal_div, ofReal_cpow]

Premises used: Complex.ofReal_cpow, Complex.ofReal_div, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
⊢ (↑(π / b) : ℂ) ^ (↑(1 / 2) : ℂ) / (↑2 : ℂ) = (↑(π / b) : ℂ) ^ (1 / 2) / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
⊢ 0 ≤ π / b

Tactic:
(div_pos pi_pos hb).le

Premises used: Real.pi_pos, LT.lt.le, div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
⊢ 0 ≤ π / b

Tactic:
exact (div_pos pi_pos hb).le

Premises used: Real.pi_pos, LT.lt.le, div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1))) =
    √π
⊢ Gamma (1 / 2) = √π

Tactic:
rw [Gamma_eq_integral one_half_pos, ← integral_comp_rpow_Ioi_of_pos zero_lt_two]

Premises used: MeasureTheory.integral_comp_rpow_Ioi_of_pos, Real.Gamma_eq_integral, one_half_pos, zero_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
⊢ Eq (α := ℝ)
    ((fun (x : ℝ) ↦ 2 * x)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-1 * HPow.hPow (β := ℕ) x 2)))
    ((fun (x : ℝ) ↦ 2 * x) (√(π / 1) / 2))

Tactic:
congr_arg (fun x : ℝ => 2 * x) (integral_gaussian_Ioi 1)

Premises used: HMul.hMul, congr_arg, integral_gaussian_Ioi, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
h :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1))) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-1 * HPow.hPow (β := ℕ) x 2))
h₁ : √π = 2 * (√(π / 1) / 2)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1))) =
    √π

Tactic:
convert! congr_arg (fun x : ℝ => 2 * x) (integral_gaussian_Ioi 1) using 1

Premises used: HMul.hMul, congr_arg, integral_gaussian_Ioi, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
h :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      2 * rexp (-1 * HPow.hPow (β := ℕ) a 2))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1))) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-1 * HPow.hPow (β := ℕ) x 2))

Tactic:
rw [← integral_const_mul]

Premises used: MeasureTheory.integral_const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      2 * rexp (-1 * HPow.hPow (β := ℕ) a 2))

Tactic:
setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
h :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1)) =
      2 * rexp (-1 * HPow.hPow (β := ℕ) x 2)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      2 * rexp (-1 * HPow.hPow (β := ℕ) a 2))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : x ^ (2 * (1 / 2 - 1)) = x⁻¹
⊢ HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1) = x⁻¹

Tactic:
rw [← rpow_mul (le_of_lt hx)]

Premises used: le_of_lt, Real.rpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
norm_num : HPow.hPow (β := ℝ) x (-1) = x⁻¹
⊢ x ^ (2 * (1 / 2 - 1)) = x⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : (HPow.hPow (β := ℝ) x 1)⁻¹ = x⁻¹
rw₁ rw₂ : x⁻¹ = x⁻¹
⊢ HPow.hPow (β := ℝ) x (-1) = x⁻¹

Tactic:
rw [rpow_neg (le_of_lt hx), rpow_one]

Premises used: le_of_lt, Real.rpow_one, Real.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1) = x⁻¹

Tactic:
have : (x ^ (2 : ℝ)) ^ (1 / (2 : ℝ) - 1) = x⁻¹ := by
      rw [← rpow_mul (le_of_lt hx)]
      norm_num
      rw [rpow_neg (le_of_lt hx), rpow_one]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
this : HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1) = x⁻¹
h : 2 * x ^ HSub.hSub (α := ℝ) 2 1 * (rexp (-HPow.hPow (β := ℝ) x 2) * x⁻¹) = 2 * rexp (-1 * HPow.hPow (β := ℕ) x 2)
⊢ (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1)) =
    2 * rexp (-1 * HPow.hPow (β := ℕ) x 2)

Tactic:
rw [smul_eq_mul, this]

Premises used: smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
this : HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1) = x⁻¹
h : x ^ HSub.hSub (α := ℝ) 2 1 = x
⊢ 2 * x ^ HSub.hSub (α := ℝ) 2 1 * (rexp (-HPow.hPow (β := ℝ) x 2) * x⁻¹) = 2 * rexp (-1 * HPow.hPow (β := ℕ) x 2)

Tactic:
simp [field, (ne_of_lt (show 0 < x from hx)).symm]

Premises used: Ne.symm, ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
this : HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1) = x⁻¹
⊢ x ^ HSub.hSub (α := ℝ) 2 1 = x

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
h : √π = 2 * (√π / 2)
h₁ : √π = 2 * √π / 2
h₂ : √π = √π * 2 / 2
h₃ h₄ : √π = √π
⊢ √π = 2 * (√(π / 1) / 2)

Tactic:
rw [div_one, ← mul_div_assoc, mul_comm, mul_div_cancel_right₀ _ (two_ne_zero' ℝ)]

Premises used: Real, mul_div_assoc, mul_div_cancel_right₀, two_ne_zero', mul_comm, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
⊢ (↑(Real.Gamma (1 / 2)) : ℂ) = (↑√π : ℂ)

Tactic:
congr_arg ((↑) : ℝ → ℂ) Real.Gamma_one_half_eq

Premises used: Real.Gamma_one_half_eq, Complex.ofReal, congr_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
h : Gamma (1 / 2) = (↑(Real.Gamma (1 / 2)) : ℂ)
h₁ : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
⊢ Gamma (1 / 2) = (↑π : ℂ) ^ (1 / 2)

Tactic:
convert! congr_arg ((↑) : ℝ → ℂ) Real.Gamma_one_half_eq

Premises used: Real.Gamma_one_half_eq, Complex.ofReal, congr_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
⊢ Gamma (1 / 2) = (↑(Real.Gamma (1 / 2)) : ℂ)

Tactic:
simpa only [one_div, ofReal_inv, ofReal_ofNat] using Gamma_ofReal (1 / 2)

Premises used: HDiv.hDiv, one_div, Complex.ofReal_ofNat, OfNat.ofNat, Complex.ofReal_inv, Complex.Gamma_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
h : (↑π : ℂ) ^ (1 / 2) = (↑(π ^ (1 / 2)) : ℂ)
h₁ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ (↑(1 / 2) : ℂ)
h₂ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ ((↑1 : ℂ) / (↑2 : ℂ))
h₃ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ ((↑1 : ℂ) / 2)
h₄ h₅ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ HDiv.hDiv (α := ℂ) 1 2
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)

Tactic:
rw [sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_ofNat, ofReal_one]

Premises used: Complex.ofReal_cpow, Real.pi_pos, LT.lt.le, Complex.ofReal_one, Complex.ofReal_div, Complex.ofReal_ofNat, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
zero : 1 / 2 * √π = √π / 2
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + 1 / 2) =
    (↑(HMul.hMul (α := ℕ) 2 0 + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp [-one_div, add_comm (1 : ℝ), Gamma_add_one, Gamma_one_half_eq]

Premises used: Real.Gamma_one_half_eq, Real.Gamma_add_one, add_comm, one_div, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
⊢ 1 / 2 * √π = √π / 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
k : ℕ
ih : Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) = (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)
⊢ (↑(k + 1) : ℝ) + 1 / 2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
k : ℕ
ih : Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) = (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)
succ :
  (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) * ((↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)) =
    (↑(2 * k + HMul.hMul (α := ℕ) 2 1 + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1 + 1)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑(k + 1) : ℝ) 1 + 1 / 2) =
    (↑(2 * (k + 1) + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1 + 1)

Tactic:
rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih, Nat.mul_add]

Premises used: add_right_comm, Real.Gamma_add_one, Nat.cast_add, Nat.mul_add, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
k : ℕ
ih : Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) = (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)
succ :
  (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 2⁻¹) * ((↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)) =
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1 + 2) * (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1 + 1)
⊢ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) * ((↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)) =
    (↑(2 * k + HMul.hMul (α := ℕ) 2 1 + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1 + 1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
k : ℕ
ih : Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) = (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)
⊢ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 2⁻¹) * ((↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)) =
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1 + 2) * (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1 + 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
k : ℕ
zero :
  Gamma (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + 1 / 2) =
    (↑(HMul.hMul (α := ℕ) 2 0 + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 1)
succ :
  ∀ (k : ℕ)
    (ih : Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) = (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)),
    Gamma (HAdd.hAdd (α := ℝ) (↑(k + 1) : ℝ) 1 + 1 / 2) =
      (↑(2 * (k + 1) + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1 + 1)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) = (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)

Tactic:
induction k with
  | zero => simp [-one_div, add_comm (1 : ℝ), Gamma_add_one, Gamma_one_half_eq]; ring
  | succ k ih =>
    rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih, Nat.mul_add]
    simp
    ring

Premises used: Real.Gamma_one_half_eq, add_right_comm, Real.Gamma_add_one, add_comm, Nat.cast_add, one_div, OfNat.ofNat, Nat.mul_add, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
⊢ Gamma ((↑0 : ℝ) + 1 / 2) = (↑(HMul.hMul (α := ℕ) 2 0 - 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) (β := ℕ) 2 0

Tactic:
simp [-one_div, Gamma_one_half_eq]

Premises used: Real.Gamma_one_half_eq, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
k : ℕ
⊢ Gamma ((↑(k + 1) : ℝ) + 1 / 2) = (↑(2 * (k + 1) - 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)

Tactic:
simpa [-one_div, mul_add] using Gamma_nat_add_one_add_half k

Premises used: Real.Gamma_nat_add_one_add_half, one_div, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
k : ℕ
zero : Gamma ((↑0 : ℝ) + 1 / 2) = (↑(HMul.hMul (α := ℕ) 2 0 - 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) (β := ℕ) 2 0
succ : ∀ (k : ℕ), Gamma ((↑(k + 1) : ℝ) + 1 / 2) = (↑(2 * (k + 1) - 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)
⊢ Gamma ((↑k : ℝ) + 1 / 2) = (↑(2 * k - 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 k

Tactic:
cases k with
  | zero => simp [-one_div, Gamma_one_half_eq]
  | succ k => simpa [-one_div, mul_add] using Gamma_nat_add_one_add_half k

Premises used: Real.Gamma_one_half_eq, Real.Gamma_nat_add_one_add_half, one_div, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : a < 0
b s : ℝ
this :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ rexp (-x)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ x ^ s

Tactic:
this.trans ?_

Premises used: Asymptotics.IsLittleO.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : a < 0
b s : ℝ
this :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ rexp (-x)
refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-x)) fun (x : ℝ) ↦ x ^ s
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ x ^ s

Tactic:
refine this.trans ?_

Premises used: Asymptotics.IsLittleO.trans