mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
s : ℝ
⊢ (fun x ↦ x ^ s * rexp (-b * x ^ 2)) =o[atTop] fun x ↦ rexp (-(1 / 2) * x)

Tactic:
[

Goal state after:
b : ℝ
hb : 0 < b
s : ℝ
⊢ (fun x ↦ x ^ s * rexp (-b * x ^ 2)) =o[atTop] fun x ↦ rexp (-(1 / 2) * x)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ HasFiniteIntegral (fun a ↦ ‖s * (↑(rexp (-a)) * ↑a ^ (s - 1))‖) (volume.restrict (Ioc 0 Y))

Tactic:
[

Goal state after:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ HasFiniteIntegral (fun a ↦ ‖s * (↑(rexp (-a)) * ↑a ^ (s - 1))‖) (volume.restrict (Ioc 0 Y))
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedDeriv n f) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume
⊢ 𝓕 (fun x ↦ iteratedDeriv n f x) x = (2 * ↑π * I * ↑x) ^ n • 𝓕 f x

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedDeriv n f) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume
⊢ 𝓕 (fun x ↦ iteratedDeriv n f x) x = (2 * ↑π * I * ↑x) ^ n • 𝓕 f x
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x ↦ x ^ s * rexp (-b * x ^ 2)) (Ioi 0) volume

Tactic:
[

Goal state after:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x ↦ x ^ s * rexp (-b * x ^ 2)) (Ioi 0) volume
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) (μ i)) → Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi μ)
⊢ Integrable ((fun x ↦ ∏ i, f i (x i)) ∘ ⇑(MeasurableEquiv.piFinSuccAbove E 0).symm)
    ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))

Tactic:
[

Goal state after:
case succ
𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) (μ i)) → Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi μ)
⊢ Integrable ((fun x ↦ ∏ i, f i (x i)) ∘ ⇑(MeasurableEquiv.piFinSuccAbove E 0).symm)
    ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedCommRing 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)

Tactic:
[

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedCommRing 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun a ↦ ‖cexp (-b * ↑a ^ 2)‖) volume

Tactic:
[

Goal state after:
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun a ↦ ‖cexp (-b * ↑a ^ 2)‖) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun a ↦ rexp (-b.re * a ^ 2)) volume

Tactic:
exact (integrable_exp_neg_mul_sq hb).2

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ ∫ (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))),
      ∏ i, f i ((MeasurableEquiv.piFinSuccAbove E 0).symm x i) ∂(μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)) =
    ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i, f i.succ (x.2 i) ∂(μ 0).prod (Measure.pi fun i ↦ μ i.succ)

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ ∫ (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))),
      ∏ i, f i ((MeasurableEquiv.piFinSuccAbove E 0).symm x i) ∂(μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)) =
    ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i, f i.succ (x.2 i) ∂(μ 0).prod (Measure.pi fun i ↦ μ i.succ)
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (x : ℝ × ℝ) in polarCoord.target, |(fderivPolarCoordSymm x).det| • f (↑polarCoord.symm x) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, |p.1| • f (↑polarCoord.symm p)

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (x : ℝ × ℝ) in polarCoord.target, |(fderivPolarCoordSymm x).det| • f (↑polarCoord.symm x) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, |p.1| • f (↑polarCoord.symm p)
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ (∫ (x : E 0), f 0 x ∂μ 0) * ∏ i, ∫ (x : E i.succ), f i.succ x ∂μ i.succ = ∏ i, ∫ (x : E i), f i x ∂μ i

Tactic:
Fin.prod_univ_succ

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ (∫ (x : E 0), f 0 x ∂μ 0) * ∏ i, ∫ (x : E i.succ), f i.succ x ∂μ i.succ =
    (∫ (x : E 0), f 0 x ∂μ 0) * ∏ i, ∫ (x : E i.succ), f i.succ x ∂μ i.succ
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |(fderivPolarCoordSymm x).det| * f (↑polarCoord.symm x) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (↑polarCoord.symm p)

Tactic:
[

Goal state after:
f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |(fderivPolarCoordSymm x).det| * f (↑polarCoord.symm x) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (↑polarCoord.symm p)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x ↦ -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
⊢ Tendsto (fun x ↦ ‖cexp (-b * ↑x ^ 2)‖) atTop (𝓝 0)

Tactic:
[

Goal state after:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A : ∀ (x : ℂ), HasDerivAt (fun x ↦ -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x
⊢ Tendsto (fun x ↦ ‖cexp (-b * ↑x ^ 2)‖) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: a : ℂ
⊢ ↑Complex.polarCoord a = (‖a‖, a.arg)

Tactic:
[

Goal state after:
a : ℂ
⊢ ↑Complex.polarCoord a = (‖a‖, a.arg)
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : RCLike 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ (∫ (x : (b : Fin (card ι)) → E (e b)),
      ∏ i, f i ((MeasurableEquiv.piCongrLeft E e) x i) ∂Measure.pi fun i' ↦ μ (e i')) =
    ∏ i, ∫ (x : E i), f i x ∂μ i

Tactic:
[

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : RCLike 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ (∫ (x : (b : Fin (card ι)) → E (e b)),
      ∏ i, f i ((MeasurableEquiv.piCongrLeft E e) x i) ∂Measure.pi fun i' ↦ μ (e i')) =
    ∏ i, ∫ (x : E i), f i x ∂μ i
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e_f
b : ℂ
hb : 0 < b.re
⊢ (fun p ↦ cexp (-b * ↑p.1 ^ 2) * cexp (-b * ↑p.2 ^ 2)) = fun p ↦ cexp (-b * (↑p.1 ^ 2 + ↑p.2 ^ 2))

Tactic:
ext1 p

Goal state after:
case e_f
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ cexp (-b * ↑p.1 ^ 2) * cexp (-b * ↑p.2 ^ 2) = cexp (-b * (↑p.1 ^ 2 + ↑p.2 ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: f : ℂ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))

Tactic:
[

Goal state after:
f : ℂ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
p : ι → ℝ × ℝ
⊢ (fderivPiPolarCoordSymm p).det = ∏ i, (p i).1

Tactic:
[

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
p : ι → ℝ × ℝ
⊢ (fderivPiPolarCoordSymm p).det = ∏ i, (p i).1
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x ↦ polarCoord.target
⊢ ((∏ i, (x i).1) • f fun i ↦ ↑polarCoord.symm (x i)) =
    |(fderivPiPolarCoordSymm x).det| • f fun i ↦ ↑polarCoord.symm (x i)

Tactic:
[

Goal state after:
case e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x ↦ polarCoord.target
⊢ ((∏ i, (x i).1) • f fun i ↦ ↑polarCoord.symm (x i)) =
    |(fderivPiPolarCoordSymm x).det| • f fun i ↦ ↑polarCoord.symm (x i)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : b.re ≠ 0
c T : ℝ
this :
  b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2 = b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)
⊢ rexp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2)) =
    rexp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))

Tactic:
this

Goal state after:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
this :
  b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2 = b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)
⊢ rexp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re))) =
    rexp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case e'_2
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x ↦ polarCoord.target
⊢ ((∏ i, ENNReal.ofReal (x i).1) * f fun i ↦ ↑polarCoord.symm (x i)) =
    ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun i ↦ ↑polarCoord.symm (x i)

Tactic:
[

Goal state after:
case e'_2
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x ↦ polarCoord.target
⊢ ((∏ i, ENNReal.ofReal (x i).1) * f fun i ↦ ↑polarCoord.symm (x i)) =
    ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun i ↦ ↑polarCoord.symm (x i)
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℂ) → ℝ≥0∞
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x ↦ Complex.polarCoord.target,
      (∏ i, ENNReal.ofReal (p i).1) * f fun i ↦ ↑Complex.polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℂ), f p

Tactic:
let e := MeasurableEquiv.piCongrRight (fun _ : ι ↦ measurableEquivRealProd.symm)
  have := volume_preserving_pi (fun _ : ι ↦ Complex.volume_preserving_equiv_real_prod.symm)
  rw [← MeasurePreserving.lintegral_comp_emb this e.measurableEmbedding]
  exact lintegral_comp_pi_polarCoord_symm (f ∘ e)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑(n + 1)
this : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1)
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s

Tactic:
this

Goal state after:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑(n + 1)
this : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1)
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1) / s
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x ↦ cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_le_bd : ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)
⊢ ContinuousAt (fun c ↦ ∫ (x : ℝ), cexp (-c * ↑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))

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
t2 : -(s + 1).re < ↑n
⊢ GammaAux n (s + 1) = s * GammaAux n s

Tactic:
GammaAux_recurrence1 s n t1

Goal state after:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
t2 : -(s + 1).re < ↑n
⊢ GammaAux n (s + 1) = s * (GammaAux n (s + 1) / s)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * ↑x ^ 2) = ↑(rexp (-1 * x ^ 2))
⊢ ∫ (x : ℝ), cexp (-1 * ↑x ^ 2) = (↑π / 1) ^ (1 / 2)

Tactic:
[

Goal state after:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * ↑x ^ 2) = ↑(rexp (-1 * x ^ 2))
⊢ ∫ (x : ℝ), cexp (-1 * ↑x ^ 2) = (↑π / 1) ^ (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: ⊢ Gamma 0 = 0

Tactic:
[

Goal state after:
⊢ Gamma 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * (↑r * ↑t) ^ (a - 1) * cexp (-(↑r * ↑t)) =
    1 / ↑r * ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑t ^ (a - 1) * cexp (-↑t)

Tactic:
[

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * (↑r * ↑t) ^ (a - 1) * cexp (-(↑r * ↑t)) =
    1 / ↑r * ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑t ^ (a - 1) * cexp (-↑t)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ 1 / ↑r * ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑t ^ (a - 1) * cexp (-↑t) =
    1 / ↑r * (1 / ↑r) ^ (a - 1) * ∫ (t : ℝ) in Ioi 0, ↑t ^ (a - 1) * cexp (-↑t)

Tactic:
[

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ 1 / ↑r * ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑t ^ (a - 1) * cexp (-↑t) =
    1 / ↑r * (1 / ↑r) ^ (a - 1) * ∫ (t : ℝ) in Ioi 0, ↑t ^ (a - 1) * cexp (-↑t)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x ↦ b.re * x ^ 2 - 2 * |b.im| * |c| * x) atTop atTop

Tactic:
[

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x ↦ b.re * x ^ 2 - 2 * |b.im| * |c| * x) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun a ↦ ‖cexp (-b * (↑a + ↑c * I) ^ 2)‖) volume

Tactic:
[

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun a ↦ ‖cexp (-b * (↑a + ↑c * I) ^ 2)‖) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Integrable (fun x ↦ rexp (-(b.re * x ^ 2))) volume

Tactic:
[

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Integrable (fun x ↦ rexp (-(b.re * x ^ 2))) volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
hs : s ≠ 0
⊢ Gamma (s + 1) = s * Gamma s

Tactic:
[

Goal state after:
s : ℝ
hs : s ≠ 0
⊢ Gamma (s + 1) = s * Gamma s
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2

Tactic:
let f : ℝ → ℂ := fun x => cexp (-b * (x : ℂ) ^ 2)
  have full_integral := integral_gaussian_complex hb
  have h_eq := calc
    ∫ x : ℝ in Iic 0, f x = ∫ x : ℝ in Ioi 0, f (-x) := by
      simpa [f] using (integral_comp_neg_Ioi 0 f).symm
    _ = ∫ x : ℝ in Ioi 0, f x :=
      setIntegral_congr_fun measurableSet_Ioi fun _ _ ↦ (by simp [f])
  rw [← integral_add_compl (s := Ioi 0) (by simp) (integrable_cexp_neg_mul_sq hb), compl_Ioi, h_eq,
    ← mul_two] at full_integral
  exact (eq_div_iff two_ne_zero).2 (by simpa using full_integral)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case e'_2
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑(t ^ (a - 1) * rexp (-(r * t))) = ↑t ^ ↑(a - 1) * ↑(rexp (-(r * t)))

Tactic:
[

Goal state after:
case e'_2
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑(t ^ (a - 1) * rexp (-(r * t))) = ↑t ^ ↑(a - 1) * ↑(rexp (-(r * t)))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in -i..id i, cexp (-b * (↑x + ↑c * I) ^ 2)) atTop (𝓝 ((↑π / b) ^ (1 / 2)))

Tactic:
[

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in -i..id i, cexp (-b * (↑x + ↑c * I) ^ 2)) atTop (𝓝 ((↑π / b) ^ (1 / 2)))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ 2 * x ^ (2 - 1) * (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) = 2 * rexp (-1 * x ^ 2)

Tactic:
this

Goal state after:
case e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ 2 * x ^ (2 - 1) * (rexp (-x ^ 2) * x⁻¹) = 2 * rexp (-1 * x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: k : ℕ
⊢ Gamma (↑k + 1 / 2) = ↑(2 * k - 1)‼ * √π / 2 ^ k

Tactic:
cases k with

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T =
    I₂ T + I * ((∫ (x : ℝ) in 0..c, cexp (-b * (↑T + ↑x * I) ^ 2)) - ∫ (x : ℝ) in 0..c, cexp (-b * (↑T - ↑x * I) ^ 2))

Tactic:
[

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T =
    I₂ T + I * ((∫ (x : ℝ) in 0..c, cexp (-b * (↑T + ↑x * I) ^ 2)) - ∫ (x : ℝ) in 0..c, cexp (-b * (↑T - ↑x * I) ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
⊢ cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))

Tactic:
[

Goal state after:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
x : ℝ
⊢ cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))