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

Goal state before:
pp: this : Integrable (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-2 / 2)) volume
⊢ Integrable (fun x ↦ (1 + x ^ 2)⁻¹) volume

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: ⊢ ↑(Module.finrank ℝ ℝ) < 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: ⊢ Integrable (fun x ↦ (1 + x ^ 2)⁻¹) volume

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: ⊢ π = π / 2 - -(π / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : V
⊢ ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
⊢ 𝓕 (𝓕⁻ f) = 𝓕⁻ (𝓕 f)

Tactic:
by

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

Goal state before:
pp: a b : ℝ
h : 0 < b
⊢ Tendsto (fun x ↦ -rexp (-b * x) / b) atTop (𝓝 (-0 / b))

Tactic:
by

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

Goal state before:
pp: a b : ℝ
h : 0 < b
⊢ IntegrableOn (fun x ↦ rexp (-b * x)) (Ioi a) volume

Tactic:
by

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
hf : ContinuousOn f (Ici a)
ho : f =O[atTop] fun x ↦ rexp (-b * x)
⊢ ‖f a‖ₑ ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
A : W ≃ₗᵢ[ℝ] V
f : V → E
w : W
⊢ 𝓕⁻ (f ∘ ⇑A) w = 𝓕⁻ f (A w)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
hc : 1 < c
t : ℝ
a✝ : t ∈ Ici c
⊢ t ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
hc : 1 < c
t : ℝ
a✝ : t ∈ Ici c
⊢ t ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
hc : 1 < c
t : ℝ
a✝ : t ∈ Ici c
⊢ t ≠ -1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w = ∫ (v : ℝ), 𝐞 (-(v * w)) • f v

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
hc : 1 < c
t : ℝ
a✝ : t ∈ Ioi c
⊢ 0 < t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
hc : 1 < c
⊢ IntegrableOn (fun t ↦ t⁻¹ / log t ^ 2) (Ioi c) volume

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
hc : 1 < c
⊢ ∫ (t : ℝ) in Ioi c, t⁻¹ / log t ^ 2 = (log c)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
⊢ ‖𝓕 (↑↑f) x‖ ≤ ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
hf : MemLp f 1 volume
⊢ ⇑(Lp.fourierTransform (MemLp.toLp f hf)) = 𝓕 f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f g : ↥(Lp E 1 volume)
⊢ fourierTransform (f + g) = fourierTransform f + fourierTransform g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn✝ : ↑n ≤ N
w : V
Z :
  ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
hn : n ≠ 0
hw : w ≠ 0
⊢ 0 < ‖w‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
c : ℂ
f : ↥(Lp E 1 volume)
⊢ fourierTransform (c • f) = (RingHom.id ℂ) c • fourierTransform f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
⊢ 0 ≤ ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
⊢ ‖{ toFun := fourierTransform, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤ 1 * ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x : V
⊢ 𝓕⁻ f₁ x = 𝓕⁻ f₂ x

Tactic:
by

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

Goal state before:
pp: s : ℝ
⊢ (fun x ↦ rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) = (fun x ↦ rexp (1 / 2 * x) / x ^ s)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
⊢ (fourierTransformInv f) x = 𝓕⁻ (↑↑f) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
⊢ ⇑(fourierTransformInv f) = 𝓕⁻ ↑↑f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
hf : MemLp f 1 volume
⊢ ⇑(fourierTransformInv (MemLp.toLp f hf)) = 𝓕⁻ f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : V
⊢ ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
⊢ (fourierTransformInvCLM V E) f = fourierTransformInv f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
⊢ Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume

Tactic:
by

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

Goal state before:
pp: s : ℝ
h : 0 < s
⊢ -1 < s - 1

Tactic:
by

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

Goal state before:
pp: s : ℝ
h : 0 < s
⊢ ∀ x ∈ Ici 1, id x ≠ 0 ∨ 0 ≤ s - 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := (ContinuousLinearMap.mul ℝ ℝ).flip
this : Integrable (fun v ↦ (L v).smulRight (f v)) volume
⊢ Integrable (fun v ↦ fourierSMulRight L f v) volume

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ IntegrableOn (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioi 0) volume

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := (ContinuousLinearMap.mul ℝ ℝ).flip
⊢ Integrable (fun v ↦ fourierSMulRight L f v) volume

Tactic:
by

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

Goal state before:
pp: s : ℂ
⊢ ((starRingEnd ℂ) s).GammaIntegral = (starRingEnd ℂ) s.GammaIntegral

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
⊢ HasDerivAt (𝓕 f) (𝓕 (fun x ↦ (-2 * ↑π * I * ↑x) • f x) w) w

Tactic:
by

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

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
⊢ deriv (𝓕 f) = 𝓕 fun x ↦ (-2 * ↑π * I * ↑x) • f x

Tactic:
by

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

Goal state before:
pp: s : ℝ
⊢ (↑s).GammaIntegral = ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
⊢ Integrable (fun x ↦ fderiv ℝ f x) volume

Tactic:
by

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

Goal state before:
pp: p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ 0 < p - 1

Tactic:
by

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

Goal state before:
pp: ⊢ GammaIntegral 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
x : ℝ
I : Integrable (fun x ↦ fderiv ℝ f x) volume
⊢ 𝓕 (deriv f) x = (𝓕 (fderiv ℝ f) x) 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: s : ℂ
X : ℝ
hs : 0 < s.re
hX : 0 ≤ X
⊢ IntervalIntegrable (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) volume 0 X

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
⊢ 𝓕 (deriv f) = fun x ↦ (2 * ↑π * I * ↑x) • 𝓕 f x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ IntervalIntegrable (fun x ↦ -(↑(rexp (-x)) * ↑x ^ s)) volume 0 X

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0} → (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg) ∈ Ioi 0 ×ˢ Ioo (-π) π

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
⊢ (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n✝ : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x ↦ x ^ n • f x) volume
hn✝ : ↑n✝ ≤ N
x : ℝ
n : ℕ
hn : ↑n ≤ N
⊢ Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) volume

Tactic:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: p s : ℝ
hs : -1 < s
hp : 0 < p
⊢ 0 < s + 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x ↦ x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) volume
⊢ AEStronglyMeasurable f volume

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ ∀ ⦃x : ℝ × ℝ⦄, x ∈ Ioi 0 ×ˢ Ioo (-π) π → (x.1 * cos x.2, x.1 * sin x.2) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ √(x ^ 2 + y ^ 2) = ‖↑x + ↑y * Complex.I‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0} →
      ((√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).1 *
            cos (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).2,
          (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).1 *
            sin (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).2) =
        x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x ↦ x ^ n • f x) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) volume
B : AEStronglyMeasurable f volume
y : ℝ
this : (-(2 * ↑π * I)) ^ n • y ^ n • f y = (-(2 * ↑π * I * ↑y)) ^ n • f y
⊢ (𝐞 (-inner ℝ y x) • (fourierPowSMulRight (innerSL ℝ) f y n) fun x ↦ 1) =
    𝐞 (-inner ℝ y x) • (-2 * ↑π * I * ↑y) ^ n • f y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ Ioi 0 ×ˢ Ioo (-π) π →
      (√((x.1 * cos x.2, x.1 * sin x.2).1 ^ 2 + (x.1 * cos x.2, x.1 * sin x.2).2 ^ 2),
          (Complex.equivRealProd.symm (x.1 * cos x.2, x.1 * sin x.2)).arg) =
        x

Tactic:
by

Goal state after:
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 : ℝ
⊢ ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ ContinuousOn (fun q ↦ √(q.1 ^ 2 + q.2 ^ 2)) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0})

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
⊢ IntervalIntegrable (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 Y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ ContinuousOn (fun q ↦ (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0})

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ ContinuousOn (fun p ↦ (p.1 * cos p.2, p.1 * sin p.2)) (Ioi 0 ×ˢ Ioo (-π) π)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ Continuous fun x ↦ x.1 * cos x.2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ Continuous fun x ↦ x.1 * sin x.2

Tactic:
by

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

Goal state before:
pp: p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
⊢ IntegrableOn (fun x ↦ x ^ s * rexp (-b * x ^ p)) (Ioi 0) volume

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
⊢ HasDerivAt (fun y ↦ rexp (-y)) (-rexp (-x)) x

Tactic:
by

Goal state after:
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
⊢ 𝓕 (iteratedDeriv n f) = fun x ↦ (2 * ↑π * I * ↑x) ^ n • 𝓕 f x

Tactic:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun y ↦ rexp (-y)) (-rexp (-x)) x
⊢ HasDerivAt (fun y ↦ ↑y ^ s) (s * ↑x ^ (s - 1)) x

Tactic:
by

Goal state after: