awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
e_f :
  HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
      HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2 =
    (HPow.hPow (β := ℕ) (Complex.sin (↑p.2 : ℂ)) 2 + HPow.hPow (β := ℕ) (Complex.cos (↑p.2 : ℂ)) 2) *
      HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2
⊢ HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
      HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2 =
    HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2

Tactic:
conv_rhs => rw [← one_mul ((p.1 : ℂ) ^ 2), ← sin_sq_add_cos_sq (p.2 : ℂ)]

Premises used: Complex.ofReal, Prod.fst, Complex.sin_sq_add_cos_sq, HPow.hPow, OfNat.ofNat, Prod.snd, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
      HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2 =
    (HPow.hPow (β := ℕ) (Complex.sin (↑p.2 : ℂ)) 2 + HPow.hPow (β := ℕ) (Complex.cos (↑p.2 : ℂ)) 2) *
      HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
simp : (2 * b)⁻¹ * (↑(Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioo (-π) π)) : ℂ) = (↑π : ℂ) / b
⊢ HMul.hMul (α := ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (r : ℝ) ↦
        (↑r : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑r : ℂ) 2))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo (-π) π)) fun (θ : ℝ) ↦ 1) =
    (↑π : ℂ) / b

Tactic:
simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply,
        univ_inter, real_smul, mul_one, integral_mul_cexp_neg_mul_sq hb]

Premises used: Complex.real_smul, integral_mul_cexp_neg_mul_sq, Set.univ_inter, MeasureTheory.integral_const, mul_one, MeasureTheory.measureReal_restrict_apply, MeasurableSet.univ
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
linarith : π < -π → π - -π + 2 * (0 - π) = 0
linarith₁ : π < -π → GT.gt (α := ℝ) 2 0
⊢ -π ≤ π

Tactic:
linarith [pi_nonneg]

Premises used: Real.pi_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
rw : (2 * b)⁻¹ * (↑(π - -π) : ℂ) = (↑π : ℂ) / b
⊢ (2 * b)⁻¹ * (↑(Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioo (-π) π)) : ℂ) = (↑π : ℂ) / b

Tactic:
rw [volume_real_Ioo_of_le (by linarith [pi_nonneg])]

Premises used: Real.volume_real_Ioo_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
simp : b⁻¹ * 2⁻¹ * ((↑π : ℂ) + (↑π : ℂ)) = (↑π : ℂ) / b
⊢ (2 * b)⁻¹ * (↑(π - -π) : ℂ) = (↑π : ℂ) / b

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ b⁻¹ * 2⁻¹ * ((↑π : ℂ) + (↑π : ℂ)) = (↑π : ℂ) / b

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

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)) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) = √(π / b)

Tactic:
rw [integral_undef, sqrt_eq_zero_of_nonpos]

Premises used: MeasureTheory.integral_undef, Real.sqrt_eq_zero_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : b ≤ 0
⊢ π / b ≤ 0

Tactic:
div_nonpos_of_nonneg_of_nonpos pi_pos.le hb

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

Tactic:
exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb

Premises used: Real.pi_pos, LT.lt.le, div_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : b ≤ 0
⊢ ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) volume

Tactic:
simpa only [not_lt, integrable_exp_neg_mul_sq_iff] using hb

Premises used: not_lt, integrable_exp_neg_mul_sq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))

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

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
inr :
  HPow.hPow (α := ℝ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) 2 =
    HPow.hPow (β := ℕ) (√(π / b)) 2
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) = √(π / b)

Tactic:
refine (sq_eq_sq₀ (by positivity) (by positivity)).1 ?_

Premises used: Iff.mp, sq_eq_sq₀
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
inr :
  HPow.hPow (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ))
      2 =
    (↑π : ℂ) / (↑b : ℂ)
⊢ HPow.hPow (α := ℝ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) 2 =
    HPow.hPow (β := ℕ) (√(π / b)) 2

Tactic:
rw [← ofReal_inj, ofReal_pow, ← coe_algebraMap, RCLike.algebraMap_eq_ofReal, ← integral_ofReal,
    sq_sqrt (div_pos pi_pos hb).le, ← RCLike.algebraMap_eq_ofReal, coe_algebraMap, ofReal_div]

Premises used: RCLike.algebraMap_eq_ofReal, Real.pi_pos, LT.lt.le, Real.sq_sqrt, Complex.coe_algebraMap, Complex.ofReal_div, Complex.ofReal_inj, div_pos, integral_ofReal, Complex.ofReal_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℝ
hb : 0 < b
rwa rwa₁ rwa₂ rwa₃ : 0 < b
⊢ 0 < (↑b : ℂ).re

Tactic:
rwa [ofReal_re]

Premises used: Complex.ofReal_re
-- 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)
⊢ HPow.hPow (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ))
      2 =
    (↑π : ℂ) / (↑b : ℂ)

Tactic:
convert! integral_gaussian_sq_complex (by rwa [ofReal_re] : 0 < (b : ℂ).re) with _ x

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

Tactic:
rw [ofReal_exp, ofReal_mul, ofReal_pow, ofReal_neg]

Premises used: Complex.ofReal_neg, Complex.ofReal_exp, Complex.ofReal_pow, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
obtain :
  ∀ (d : ℝ) (hd : 0 < d) (hd' : d < b.re),
    ContinuousAt (Y := ℂ)
      (fun (c : ℂ) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      b
⊢ ContinuousAt (Y := ℂ)
    (fun (c : ℂ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    b

Tactic:
obtain ⟨d, hd, hd'⟩ := exists_between hb

Premises used: exists_between
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
⊢ ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)

Tactic:
eventually_of_mem ((continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds hd') ?_

Premises used: Complex.continuous_re, Filter.eventually_of_mem, isOpen_Ioi, IsOpen.mem_nhds, Continuous.isOpen_preimage
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
refine : ∀ x ∈ re ⁻¹' Ioi d, ∀ᵐ (x_1 : ℝ), ‖f x x_1‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x_1 2)
⊢ ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)

Tactic:
refine eventually_of_mem ((continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds hd') ?_

Premises used: Complex.continuous_re, Filter.eventually_of_mem, isOpen_Ioi, IsOpen.mem_nhds, Continuous.isOpen_preimage
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
h : ∀ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
⊢ ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)

Tactic:
filter_upwards with x
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
h : rexp (-c.re * HPow.hPow (β := ℕ) x 2) ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
⊢ ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)

Tactic:
rw [norm_cexp_neg_mul_sq]

Premises used: norm_cexp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
h : d ≤ c.re
⊢ rexp (-c.re * HPow.hPow (β := ℕ) x 2) ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
⊢ d ≤ c.re

Tactic:
le_of_lt hc

Premises used: le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
⊢ d ≤ c.re

Tactic:
exact le_of_lt hc

Premises used: le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
⊢ ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)

Tactic:
have f_le_bd : ∀ᶠ c : ℂ in 𝓝 b, ∀ᵐ x : ℝ, ‖f c x‖ ≤ exp (-d * x ^ 2) := by
    refine eventually_of_mem ((continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds hd') ?_
    intro c hc; filter_upwards with x
    rw [norm_cexp_neg_mul_sq]
    gcongr
    exact le_of_lt hc
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_le_bd : ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
⊢ ∀ (x : ℂ),
    AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (x_1 : ℝ) ↦ cexp (-x * HPow.hPow (β := ℕ) (↑x_1 : ℂ) 2)) volume

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_le_bd : ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
⊢ ∀ (a : ℝ), ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ cexp (-x * HPow.hPow (β := ℕ) (↑a : ℂ) 2)) b

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_le_bd : ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
⊢ ContinuousAt (Y := ℂ)
    (fun (c : ℂ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    b

Tactic:
exact continuousAt_of_dominated (Eventually.of_forall (by fun_prop)) f_le_bd
    (integrable_exp_neg_mul_sq hd) (ae_of_all _ (by fun_prop))

Premises used: Filter.Eventually.of_forall, MeasureTheory.ae_of_all, MeasureTheory.continuousAt_of_dominated, integrable_exp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b_1 : ℂ
hb_1 : 0 < b_1.re
b : ℂ
hb : 0 < b.re
contrapose! : ∀ (hb : b = 0), b.re ≤ 0
⊢ b ≠ 0

Tactic:
contrapose! hb
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b_1 : ℂ
hb_1 : 0 < b_1.re
b : ℂ
hb : b = 0
rw : re 0 ≤ 0
⊢ b.re ≤ 0

Tactic:
rw [hb]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b_1 : ℂ
hb_1 : 0 < b_1.re
b : ℂ
hb : b = 0
⊢ re 0 ≤ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ ∀ {b : ℂ}, 0 < b.re → b ≠ 0

Tactic:
have nv : ∀ {b : ℂ}, 0 < re b → b ≠ 0 := by intro b hb; contrapose! hb; rw [hb]; simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ 0 < re 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c :
  ContinuousOn (Y := ℂ)
    (fun {b : ℂ} ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    {c : ℂ | 0 < c.re}
c₁ : ContinuousOn (Y := ℂ) (fun {b : ℂ} ↦ ((↑π : ℂ) / b) ^ (1 / 2)) {c : ℂ | 0 < c.re}
c₂ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / 1) ^ (1 / 2)
c₃ :
  ∀ (c : ℂ) (hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c),
    HPow.hPow (α := ℂ → ℂ) (β := ℕ)
        (fun {b : ℂ} ↦
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
            cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
        2 c =
      HPow.hPow (α := ℂ → ℂ) (β := ℕ) (fun {b : ℂ} ↦ ((↑π : ℂ) / b) ^ (1 / 2)) 2 c
c₄ : ∀ {c : ℂ} (hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c), ((↑π : ℂ) / c) ^ (1 / 2) ≠ 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)

Tactic:
apply
    (convex_halfSpace_re_gt 0).isPreconnected.eq_of_sq_eq ?_ ?_ (fun c hc => ?_) (fun {c} hc => ?_)
      (by simp : 0 < re (1 : ℂ)) ?_ hb

Premises used: IsPreconnected.eq_of_sq_eq, OfNat.ofNat, convex_halfSpace_re_gt, Convex.isPreconnected
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ ContinuousOn (Y := ℂ)
    (fun {b : ℂ} ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    {c : ℂ | 0 < c.re}

Tactic:
continuousOn_of_forall_continuousAt continuousAt_gaussian_integral

Premises used: continuousOn_of_forall_continuousAt, continuousAt_gaussian_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ ContinuousOn (Y := ℂ)
    (fun {b : ℂ} ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    {c : ℂ | 0 < c.re}

Tactic:
exact continuousOn_of_forall_continuousAt continuousAt_gaussian_integral

Premises used: continuousOn_of_forall_continuousAt, continuousAt_gaussian_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ ContinuousOn (Y := ℂ) (fun {b : ℂ} ↦ ((↑π : ℂ) / b) ^ (1 / 2)) {c : ℂ | 0 < c.re}

Tactic:
continuousOn_of_forall_continuousAt fun b hb =>
        (continuousAt_cpow_const (Or.inl ?_)).comp (continuousAt_const.div continuousAt_id (nv hb))

Premises used: continuousOn_of_forall_continuousAt, continuousAt_const, continuousAt_cpow_const, ContinuousAt.comp, ContinuousAt.div, Or.inl, continuousAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
continuousOn_of_forall_continuousAt :
  ∀ (b : ℂ) (hb : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} b), 0 < ((↑π : ℂ) / b).re
⊢ ContinuousOn (Y := ℂ) (fun {b : ℂ} ↦ ((↑π : ℂ) / b) ^ (1 / 2)) {c : ℂ | 0 < c.re}

Tactic:
refine
      continuousOn_of_forall_continuousAt fun b hb =>
        (continuousAt_cpow_const (Or.inl ?_)).comp (continuousAt_const.div continuousAt_id (nv hb))

Premises used: continuousOn_of_forall_continuousAt, continuousAt_const, continuousAt_cpow_const, ContinuousAt.comp, ContinuousAt.div, Or.inl, continuousAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b_1 : ℂ
hb_1 : 0 < b_1.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
b : ℂ
hb : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} b
rw : 0 < HDiv.hDiv (β := ℝ) (π * b.re) ((normSq : (a : ℂ) → ℝ) b : ℝ)
⊢ 0 < ((↑π : ℂ) / b).re

Tactic:
rw [div_re, ofReal_im, ofReal_re, zero_mul, zero_div, add_zero]

Premises used: MulZeroClass.zero_mul, zero_div, Complex.div_re, Complex.ofReal_re, Complex.ofReal_im, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b_1 : ℂ
hb_1 : 0 < b_1.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
b : ℂ
hb : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} b
⊢ 0 < HDiv.hDiv (β := ℝ) (π * b.re) ((normSq : (a : ℂ) → ℝ) b : ℝ)

Tactic:
div_pos (mul_pos pi_pos hb) (normSq_pos.mpr (nv hb))

Premises used: Iff.mpr, Complex.normSq_pos, Real.pi_pos, mul_pos, div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b_1 : ℂ
hb_1 : 0 < b_1.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
b : ℂ
hb : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} b
⊢ 0 < HDiv.hDiv (β := ℝ) (π * b.re) ((normSq : (a : ℂ) → ℝ) b : ℝ)

Tactic:
exact div_pos (mul_pos pi_pos hb) (normSq_pos.mpr (nv hb))

Premises used: Iff.mpr, Complex.normSq_pos, Real.pi_pos, mul_pos, div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
x : ℝ
⊢ cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)

Tactic:
simp only [ofReal_exp, neg_mul, one_mul, ofReal_neg, ofReal_pow]

Premises used: Complex.ofReal_neg, Complex.ofReal_exp, neg_mul, Complex.ofReal_pow, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)

Tactic:
have : ∀ x : ℝ, cexp (-(1 : ℂ) * (x : ℂ) ^ 2) = exp (-(1 : ℝ) * x ^ 2) := by
      intro x
      simp only [ofReal_exp, neg_mul, one_mul, ofReal_neg, ofReal_pow]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
simp_rw :
  (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ) =
    ((↑π : ℂ) / 1) ^ (1 / 2)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / 1) ^ (1 / 2)

Tactic:
simp_rw [this, ← coe_algebraMap, RCLike.algebraMap_eq_ofReal, integral_ofReal,
      ← RCLike.algebraMap_eq_ofReal, coe_algebraMap]

Premises used: RCLike.algebraMap_eq_ofReal, Complex.coe_algebraMap, integral_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
a : (↑π : ℂ) / 1
a₁ : 1 / 2
| ((↑π : ℂ) / 1) ^ (1 / 2)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
a : (↑(π / 1) : ℂ)
| (↑π : ℂ) / 1

Tactic:
rw [← ofReal_one, ← ofReal_div]

Premises used: Complex.ofReal_one, Complex.ofReal_div
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
| (↑π : ℂ) / 1

Tactic:
· rw [← ofReal_one, ← ofReal_div]

Premises used: Complex.ofReal_one, Complex.ofReal_div
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
a : (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ)
| 1 / 2

Tactic:
rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]

Premises used: Complex.ofReal_one, Complex.ofReal_div, Complex.ofReal_ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
a : (↑1 : ℂ) / 2
a₁ : (↑1 : ℂ) / (↑2 : ℂ)
a₂ : (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ)
| 1 / 2

Tactic:
· rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]

Premises used: Complex.ofReal_one, Complex.ofReal_div, Complex.ofReal_ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
a : (↑π : ℂ) / 1
a₁ a₂ : 1 / 2
| ((↑π : ℂ) / 1) ^ (1 / 2)

Tactic:
congr
      · rw [← ofReal_one, ← ofReal_div]
      · rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]

Premises used: Complex.ofReal_one, Complex.ofReal_div, Complex.ofReal_ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
conv_rhs :
  (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ) =
    (↑(π / 1) : ℂ) ^ (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ)
⊢ (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ) =
    ((↑π : ℂ) / 1) ^ (1 / 2)

Tactic:
conv_rhs =>
      congr
      · rw [← ofReal_one, ← ofReal_div]
      · rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]

Premises used: Complex.ofReal_one, Complex.ofReal_div, Complex.ofReal_ofNat