mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
p : ℕ × ℕ
hp : p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)
⊢ Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ

Tactic:
simp only [Finset.mem_product, Finset.mem_range_succ_iff] at hp

Goal state after:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
p : ℕ × ℕ
hp : p.1 ≤ k ∧ p.2 ≤ n
⊢ Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: ⊢ ∫ (x : ℝ) in Ioi 0, rexp (-x) = 1

Tactic:
simpa only [neg_zero, exp_zero] using integral_exp_neg_Ioi 0

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

Goal state before:
pp: a : ℂ
ha : a.re < 0
c : ℝ
⊢ Tendsto (fun x ↦ Complex.exp (a * ↑x)) atTop (𝓝 0)

Tactic:
simpa [Complex.tendsto_exp_nhds_zero_iff] using tendsto_const_nhds.neg_mul_atTop ha tendsto_id

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
f : α → E
g : α → F
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
μ : Measure α
hfm : AEStronglyMeasurable f μ
hf : f =O[⊤] g
hg : IntegrableAtFilter g ⊤ μ
⊢ IntegrableAtFilter f ⊤ μ

Tactic:
exact hf.integrableAtFilter ⟨univ, univ_mem, hfm.restrict⟩ hg

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i ↦ f (i, x)) s μ

Tactic:
obtain ⟨w, hwl, hw⟩ := hfm.exists_mem

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i ↦ f (i, y)) (μ.restrict s)
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i ↦ f (i, x)) s μ
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

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

Tactic:
by simp

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 : ℝ
⊢ ∫ (v : ℝ), Complex.exp (↑(-(2 * π * (v * w))) * Complex.I) • f v =
    ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v

Tactic:
neg_mul,

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ ∫ (v : ℝ), Complex.exp (↑(-(2 * π * (v * w))) * Complex.I) • f v =
    ∫ (v : ℝ), Complex.exp (↑(-(2 * π * v * w)) * Complex.I) • f v
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case left
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))
⊢ AEStronglyMeasurable (fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (volume.restrict (Ioc 0 Y))

Tactic:
refine (continuousOn_const.mul ?_).aestronglyMeasurable measurableSet_Ioc
    apply (continuous_ofReal.comp continuous_neg.rexp).continuousOn.mul
    apply continuousOn_of_forall_continuousAt
    intro x hx
    refine (?_ : ContinuousAt (fun x : ℂ => x ^ (s - 1)) _).comp continuous_ofReal.continuousAt
    exact continuousAt_cpow_const <| ofReal_mem_slitPlane.2 hx.1

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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ (b ^ (-p⁻¹)) ^ s * x✝ ^ s * rexp (-x✝ ^ p) = (b ^ (-p⁻¹)) ^ s * x✝ ^ s * rexp (-b * (b ^ (-p⁻¹ * p) * x✝ ^ p))

pp: case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

pp: case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

pp: case hy
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝

pp: case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

pp: case hy
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝

Tactic:
neg_mul,

Goal state after:
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ (b ^ (-p⁻¹)) ^ s * x✝ ^ s * rexp (-x✝ ^ p) = (b ^ (-p⁻¹)) ^ s * x✝ ^ s * rexp (-(b * (b ^ (-p⁻¹ * p) * x✝ ^ p)))

case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

case hy
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝

case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

case hy
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ (b ^ (-p⁻¹)) ^ s * x✝ ^ s * rexp (-x✝ ^ p) = (b ^ (-p⁻¹)) ^ s * x✝ ^ s * rexp (-(b * (b ^ (-p⁻¹ * p) * x✝ ^ p)))

pp: case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

pp: case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

pp: case hy
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝

pp: case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

pp: case hy
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝

Tactic:
neg_mul,

Goal state after:
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ (b ^ (-p⁻¹)) ^ s * x✝ ^ s * rexp (-x✝ ^ p) = (b ^ (-p⁻¹)) ^ s * x✝ ^ s * rexp (-(b * (b ^ (-(p⁻¹ * p)) * x✝ ^ p)))

case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

case hy
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝

case hx
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ (-p⁻¹)

case hy
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
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ x✝
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: p : ℝ × ℝ
⊢ ‖↑Complex.polarCoord.symm p‖ = |p.1|

Tactic:
by simp

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

Goal state before:
pp: b : ℂ
c T : ℝ
⊢ rexp (-b * (↑T + ↑c * I) ^ 2).re = rexp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2))

Tactic:
neg_mul,

Goal state after:
b : ℂ
c T : ℝ
⊢ rexp (-(b * (↑T + ↑c * I) ^ 2)).re = rexp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
this : (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ s.re * rexp (-x) = x ^ s.re * rexp (-1 * x)

Tactic:
neg_mul,

Goal state after:
s : ℂ
hs : 0 < s.re
this : (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ s.re * rexp (-x) = x ^ s.re * rexp (-(1 * x))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
this✝ : (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
this : (fun e ↦ ‖-↑e ^ s * ↑(rexp (-e))‖) =ᶠ[atTop] fun e ↦ e ^ s.re * rexp (-1 * e)
⊢ Tendsto (fun x ↦ ‖-↑x ^ s * ↑(rexp (-x))‖) atTop (𝓝 0)

Tactic:
exact (tendsto_congr' this).mpr (tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero _ _ zero_lt_one)

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

Goal state before:
pp: case hbc
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ b.im * y ≤ |b.im| * |c|

Tactic:
refine (le_abs_self _).trans ?_

Goal state after:
case hbc
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ |b.im * y| ≤ |b.im| * |c|
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ 0 < re 1

Tactic:
by simp

Goal state after:
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 : ℝ), rexp (-1 * x ^ 2)) = ↑(π / 1) ^ ↑(1 / 2)

Tactic:
← ofReal_cpow,

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 : ℝ), rexp (-1 * x ^ 2)) = ↑((π / 1) ^ (1 / 2))

case hx
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * ↑x ^ 2) = ↑(rexp (-1 * x ^ 2))
⊢ 0 ≤ π / 1
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
f : ℝ → ℂ := fun x ↦ cexp (-b * ↑x ^ 2)
full_integral : ∫ (x : ℝ), cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2)
h_eq : ∫ (x : ℝ) in Iic 0, f x = ∫ (x : ℝ) in Ioi 0, f x
⊢ MeasurableSet (Ioi 0)

Tactic:
by simp

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

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

Tactic:
| succ k ih =>

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

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun c ↦ ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))
⊢ 0 < 1 / 2

Tactic:
by simp

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (↑π / -(-↑π * b)) ^ (1 / 2) * cexp (0 - (-2 * ↑π * I * ↑t + 2 * ↑π * c) ^ 2 / (4 * (-↑π * b))) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
neg_mul,

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (↑π / - -(↑π * b)) ^ (1 / 2) * cexp (0 - (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 / (4 * -(↑π * b))) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ Integrable (fun v ↦ cexp (-b * ∑ i, ↑(v i) ^ 2 + ∑ i, c i * ↑(v i))) volume

Tactic:
neg_mul,

Goal state after:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ Integrable (fun v ↦ cexp (-(b * ∑ i, ↑(v i) ^ 2) + ∑ i, c i * ↑(v i))) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ ∫ (v : ι → ℝ), cexp (-b * ∑ i, ↑(v i) ^ 2 + ∑ i, c i * ↑(v i)) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i, c i ^ 2) / (4 * b))

Tactic:
neg_mul,

Goal state after:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ ∫ (v : ι → ℝ), cexp (-(b * ∑ i, ↑(v i) ^ 2) + ∑ i, c i * ↑(v i)) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i, c i ^ 2) / (4 * b))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : FiniteDimensional ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
f g : 𝓢(V, H)
⊢ ⟪(𝓕 f).toLp 2 volume, (𝓕 g).toLp 2 volume⟫ = ⟪f.toLp 2 volume, g.toLp 2 volume⟫

Tactic:
by simp

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

Goal state before:
pp: case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f✝ f : 𝓢(E, F)
⊢ ‖(↑(toLpCLM ℂ F 2 volume) ∘ₗ ↑(fourierEquiv ℂ 𝓢(E, F))) f‖ ≤ 1 * ‖↑(toLpCLM ℂ F 2 volume) f‖

Tactic:
rw [one_mul]

Goal state after:
case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f✝ f : 𝓢(E, F)
⊢ ‖(↑(toLpCLM ℂ F 2 volume) ∘ₗ ↑(fourierEquiv ℂ 𝓢(E, F))) f‖ ≤ ‖↑(toLpCLM ℂ F 2 volume) f‖
Module: Mathlib.Analysis.Fourier.LpSpace

Goal state before:
pp: case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f✝ f : 𝓢(E, F)
⊢ ‖(↑(toLpCLM ℂ F 2 volume) ∘ₗ ↑(fourierEquiv ℂ 𝓢(E, F)).symm) f‖ ≤ 1 * ‖↑(toLpCLM ℂ F 2 volume) f‖

Tactic:
rw [one_mul]

Goal state after:
case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f✝ f : 𝓢(E, F)
⊢ ‖(↑(toLpCLM ℂ F 2 volume) ∘ₗ ↑(fourierEquiv ℂ 𝓢(E, F)).symm) f‖ ≤ ‖↑(toLpCLM ℂ F 2 volume) f‖
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℂ F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
μ : Measure E
hμ : μ.HasTemperateGrowth
x✝¹ x✝ : 𝓢(E, F)
⊢ (toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F) (integralCLM ℂ μ ∘SL (pairing (lsmul ℂ ℂ).flip) (x✝¹ + x✝)) =
    (toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F) (integralCLM ℂ μ ∘SL (pairing (lsmul ℂ ℂ).flip) x✝¹) +
      (toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F) (integralCLM ℂ μ ∘SL (pairing (lsmul ℂ ℂ).flip) x✝)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℂ F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
μ : Measure E
hμ : μ.HasTemperateGrowth
x✝¹ : ℂ
x✝ : 𝓢(E, F)
⊢ (toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F) (integralCLM ℂ μ ∘SL (pairing (lsmul ℂ ℂ).flip) (x✝¹ • x✝)) =
    (RingHom.id ℂ) x✝¹ •
      (toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F) (integralCLM ℂ μ ∘SL (pairing (lsmul ℂ ℂ).flip) x✝)

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he✝ : Continuous ⇑e
hL✝ : Continuous fun p ↦ (L p.1) p.2
he : Continuous ⇑e
hL : Continuous fun p ↦ (L p.1) p.2
w : W
x y : V
⊢ ‖↑(e ((L x) w))‖ ≤ 1

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he✝ : Continuous ⇑e
hL✝ : Continuous fun p ↦ (L p.1) p.2
he : Continuous ⇑e
hL : Continuous fun p ↦ (L p.1) p.2
w : W
x y : V
⊢ ‖↑(e ((L y) w))‖ ≤ 1

Tactic:
by simp

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

Goal state before:
pp: case h
V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
h : v ≠ v'
w : W
hw : (L (v - v')) w ≠ 0 w
a : ℝ
ha : e a ≠ 1 a
⊢ ¬(↑(e ((L v') ((a / ((L v) w - (L v') w)) • w))))⁻¹ * ↑(e ((L v) ((a / ((L v) w - (L v') w)) • w))) = 1

Tactic:
← Metric.unitSphere.coe_inv,

Goal state after:
case h
V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
h : v ≠ v'
w : W
hw : (L (v - v')) w ≠ 0 w
a : ℝ
ha : e a ≠ 1 a
⊢ ¬↑(e ((L v') ((a / ((L v) w - (L v') w)) • w)))⁻¹ * ↑(e ((L v) ((a / ((L v) w - (L v') w)) • w))) = 1
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
inst✝⁴ : CompleteSpace F
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : (toTemperedDistributionCLM F μ p) f = 0
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
hg₁ : HasCompactSupport (⇑Complex.ofRealCLM ∘ g)
hg₂ : ContDiff ℝ ∞ (⇑Complex.ofRealCLM ∘ g)
⊢ ∫ (x : E), g x • ↑↑f x ∂μ = ((toTemperedDistributionCLM F μ p) f) (hg₁.toSchwartzMap hg₂)

Tactic:
by simp

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
⊢ 2 ≠ ∞

Tactic:
by simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedAddCommGroup F₂
inst✝⁸ : NormedAddCommGroup F₃
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedSpace 𝕜 F₁
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℂ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ : E
hB : Integrable (fun p ↦ (B.flip (f₂ p.2)) (f₁ (p.1 - p.2))) (volume.prod volume)
x y : E
⊢ ‖Function.uncurry (fun x y ↦ 𝐞 (-inner ℝ x ξ) • (B (f₁ (x - y))) (f₂ y)) (x, y)‖ ≤
    ‖(B.flip (f₂ (x, y).2)) (f₁ ((x, y).1 - (x, y).2))‖

Tactic:
by simp

Goal state after: