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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 0 < (s + 1).re

Tactic:
;

Goal state after:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 0 < (s + 1).re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 0 < s.re + 1

Tactic:
;

Goal state after:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 0 < s.re + 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:
det_fderivPiPolarCoordSymm,

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)) = |∏ i, (x i).1| • f fun i ↦ ↑polarCoord.symm (x i)
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
⊢ (fun e ↦ ‖-↑e ^ s * ↑(rexp (-e))‖) x = (fun e ↦ e ^ s.re * rexp (-1 * e)) x

Tactic:
;

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
⊢ (fun e ↦ ‖-↑e ^ s * ↑(rexp (-e))‖) x = (fun e ↦ e ^ s.re * rexp (-1 * e)) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = (s + 1).GammaIntegral / s

Tactic:
;

Goal state after:
case zero
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = (s + 1).GammaIntegral / s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero.hb
s : ℂ
h1 : 0 < s.re
⊢ s ≠ 0

Tactic:
;

Goal state after:
case zero.hb
s : ℂ
h1 : 0 < s.re
⊢ s ≠ 0
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:
det_fderivPiPolarCoordSymm,

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 |∏ i, (x i).1| * f fun i ↦ ↑polarCoord.symm (x i)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero.hb
s : ℂ
h1 : s = 0
⊢ s.re ≤ 0

Tactic:
;

Goal state after:
case zero.hb
s : ℂ
h1 : s = 0
⊢ s.re ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑n + 1
⊢ -(s.re + 1) < ↑n

Tactic:
;

Goal state after:
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑n + 1
⊢ -(s.re + 1) < ↑n
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
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
⊢ ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)

Tactic:
;

Goal state after:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x ↦ cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
⊢ ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
n : ℕ
h1 : -s.re < ↑n + 1
⊢ -(s.re + 1) < ↑n

Tactic:
;

Goal state after:
s : ℂ
n : ℕ
h1 : -s.re < ↑n + 1
⊢ -(s.re + 1) < ↑n
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|
⊢ 2 * (b.im * y) ≤ 2 * |b.im| * |c|

Tactic:
;

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

Goal state before:
pp: b✝ : ℂ
hb✝ : 0 < b✝.re
b : ℂ
hb : 0 < b.re
⊢ b ≠ 0

Tactic:
;

Goal state after:
b✝ : ℂ
hb✝ : 0 < b✝.re
b : ℂ
hb : 0 < b.re
⊢ b ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b✝ : ℂ
hb✝ : 0 < b✝.re
b : ℂ
hb : b = 0
⊢ b.re ≤ 0

Tactic:
;

Goal state after:
b✝ : ℂ
hb✝ : 0 < b✝.re
b : ℂ
hb : b = 0
⊢ b.re ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b✝ : ℂ
hb✝ : 0 < b✝.re
b : ℂ
hb : b = 0
⊢ re 0 ≤ 0

Tactic:
;

Goal state after:
b✝ : ℂ
hb✝ : 0 < b✝.re
b : ℂ
hb : b = 0
⊢ re 0 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < ↑⌊1 - s.re⌋₊
⊢ 0 ≤ k

Tactic:
;

Goal state after:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < ↑⌊1 - s.re⌋₊
⊢ 0 ≤ k
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ n = ⌊1 - s.re⌋₊ + (n - ⌊1 - s.re⌋₊)

Tactic:
;

Goal state after:
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ n = ⌊1 - s.re⌋₊ + (n - ⌊1 - s.re⌋₊)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
;

Goal state after:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
⊢ -(s.re + 1) < ↑n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ -s.re < 0

Tactic:
;

Goal state after:
s : ℂ
hs : 0 < s.re
⊢ -s.re < 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero
s : ℂ
⊢ ∀ (s : ℂ), ((starRingEnd ℂ) s).GammaIntegral = (starRingEnd ℂ) s.GammaIntegral

Tactic:
;

Goal state after:
case zero
s : ℂ
⊢ ∀ (s : ℂ), ((starRingEnd ℂ) s).GammaIntegral = (starRingEnd ℂ) s.GammaIntegral
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

Tactic:
;

Goal state after:
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 ≤ π
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e_f.e_a.e_a
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
h'f : Integrable (𝓕 f) volume
v : V
A : Tendsto (fun c ↦ ∫ (w : V), cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto (fun c ↦ ∫ (w : V), 𝓕 (fun w ↦ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫)) w • f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
w : V
⊢ ↑π ^ 2 * ↑‖v - w‖ ^ 2 * ↑c = ↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2

Tactic:
;

Goal state after:
case e_f.e_a.e_a
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
h'f : Integrable (𝓕 f) volume
v : V
A : Tendsto (fun c ↦ ∫ (w : V), cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto (fun c ↦ ∫ (w : V), 𝓕 (fun w ↦ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫)) w • f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
w : V
⊢ ↑π ^ 2 * ↑‖v - w‖ ^ 2 * ↑c = ↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case zero
⊢ 1 / 2 * √π = √π / 2

Tactic:
;

Goal state after:
case zero
⊢ 1 / 2 * √π = √π / 2
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
⊢ (∀ (m : ℕ), s ≠ -↑m) → Gamma s ≠ 0

Tactic:
;

Goal state after:
s : ℝ
⊢ (∀ (m : ℕ), s ≠ -↑m) → Gamma s ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: m : ℕ
⊢ Gamma (-↑m) = 0

Tactic:
;

Goal state after:
m : ℕ
⊢ Gamma (-↑m) = 0
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
a b : ℂ
⊢ (a - b * I) * (a - b * I) = (-a + b * 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
a b : ℂ
⊢ (a - b * I) * (a - b * I) = (-a + b * I) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

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

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: b c d : ℂ
hb : b = 0
⊢ 0 ≤ b.re

Tactic:
;

Goal state after:
b c d : ℂ
hb : b = 0
⊢ 0 ≤ b.re
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
t : ℂ
x : ℝ
| cexp (I * t * ↑x) * cexp (-b * ↑x ^ 2)

Tactic:
;

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
x : ℝ
| cexp (I * t * ↑x) * cexp (-b * ↑x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b c : ℂ
hb : b = 0
⊢ b.re ≤ 0

Tactic:
;

Goal state after:
b c : ℂ
hb : b = 0
⊢ b.re ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

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

Tactic:
;

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

Goal state before:
pp: b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
x w : V
hb : b = 0
⊢ b.re ≤ 0

Tactic:
;

Goal state after:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
x w : V
hb : b = 0
⊢ b.re ≤ 0
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : RCLike 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : FiniteDimensional ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : CompleteSpace E
f : 𝓢(V, E)
x : V
⊢ 𝓕 (𝓕⁻ ⇑f) x = f x

Tactic:
f.continuous.fourier_fourierInv_eq f.integrable
      (𝓕 f).integrable

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : RCLike 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : FiniteDimensional ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : CompleteSpace E
f : 𝓢(V, E)
x : V
⊢ f x = f x
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
g : E → ℂ
hg : Function.HasTemperateGrowth g
⊢ ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
      IsVanishingOn (⇑f) s → IsVanishingOn (⇑((TemperedDistribution.smulLeftCLM F g) f)) s

Tactic:
;

Goal state after:
case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
g : E → ℂ
hg : Function.HasTemperateGrowth g
⊢ ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
      IsVanishingOn (⇑f) s → IsVanishingOn (⇑((TemperedDistribution.smulLeftCLM F g) f)) s
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
m : E
⊢ ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsVanishingOn (⇑f) s → IsVanishingOn (⇑(∂_{m} f)) s

Tactic:
;

Goal state after:
case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
m : E
⊢ ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsVanishingOn (⇑f) s → IsVanishingOn (⇑(∂_{m} f)) s
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
n : ℕ
m : Fin n → E
⊢ ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsVanishingOn (⇑f) s → IsVanishingOn (⇑(∂^{m} f)) s

Tactic:
;

Goal state after:
case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
n : ℕ
m : Fin n → E
⊢ ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsVanishingOn (⇑f) s → IsVanishingOn (⇑(∂^{m} f)) s
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: case h
E : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_12
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
f : 𝓓'(Ω, F)
m : E
⊢ ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsVanishingOn (⇑f) s → IsVanishingOn (⇑(∂_{m} f)) s

Tactic:
;

Goal state after:
case h
E : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_12
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
f : 𝓓'(Ω, F)
m : E
⊢ ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsVanishingOn (⇑f) s → IsVanishingOn (⇑(∂_{m} f)) s
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: case h
E : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_12
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
f : 𝓓'(Ω, F)
n : ℕ
m : Fin n → E
⊢ ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsVanishingOn (⇑f) s → IsVanishingOn (⇑(∂^{m} f)) s

Tactic:
;

Goal state after:
case h
E : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_12
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
f : 𝓓'(Ω, F)
n : ℕ
m : Fin n → E
⊢ ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsVanishingOn (⇑f) s → IsVanishingOn (⇑(∂^{m} f)) s
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case e_a
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ s / 2 + s' / 2 = (s + s') / 2

Tactic:
;

Goal state after:
case e_a
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ s / 2 + s' / 2 = (s + s') / 2
Module: Mathlib.Analysis.Fourier.LpSpace

Goal state before:
pp: 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 : ↥(Lp F 2 volume)
⊢ f = 𝓕 (𝓕⁻ f)

Tactic:
;

Goal state after:
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 : ↥(Lp F 2 volume)
⊢ f = 𝓕 (𝓕⁻ f)
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
x✝ : V
⊢ (char he hL 0) x✝ = 1 x✝

Tactic:
;

Goal state after:
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
x✝ : V
⊢ (char he hL 0) x✝ = 1 x✝
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
w : W
x✝ : V
⊢ (char he hL (-w)) x✝ = (star (char he hL w)) x✝

Tactic:
;

Goal state after:
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
w : W
x✝ : V
⊢ (char he hL (-w)) x✝ = (star (char he hL w)) x✝
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:
← Submonoid.coe_mul,

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.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
w : W
x✝ : V
⊢ ((charAlgHom he hL).toRingHom (AddMonoidAlgebra.single w 1)) x✝ = (char he hL w) x✝

Tactic:
;

Goal state after:
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
w : W
x✝ : V
⊢ ((charAlgHom he hL).toRingHom (AddMonoidAlgebra.single w 1)) x✝ = (char he hL w) x✝
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
c : ℂ
f : 𝓢'(E, F)
x✝ : 𝓢(E, ℂ)
⊢ ((smulLeftCLM F fun x ↦ c) f) x✝ = (c • f) x✝

Tactic:
;

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
c : ℂ
f : 𝓢'(E, F)
x✝ : 𝓢(E, ℂ)
⊢ ((smulLeftCLM F fun x ↦ c) f) x✝ = (c • f) x✝