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

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

Tactic:
simpa using

Goal state after:
b : ℝ
hb : 0 < b
⊢ Integrable (fun x ↦ rexp (-(b * x ^ 2))) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
h : IntegrableOn (fun x ↦ rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
this : ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, ↑‖rexp (-b * x ^ 2)‖₊
⊢ False

Tactic:
simpa using

Goal state after:
b : ℝ
h : IntegrableOn (fun x ↦ rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
this : ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, ↑‖rexp (-b * x ^ 2)‖₊
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

Tactic:
simpa using

Goal state after:
b : ℝ
hb : 0 < b
⊢ Integrable (fun x ↦ x * rexp (-(b * x ^ 2))) volume
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 : ℂ), f p

Tactic:
← (volume_preserving_equiv_real_prod.symm).lintegral_comp_emb
    measurableEquivRealProd.symm.measurableEmbedding,

Goal state after:
f : ℂ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) =
    ∫⁻ (a : ℝ × ℝ), f (measurableEquivRealProd.symm a) ∂MeasureTheory.volume
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
⊢ ∫ (x : (i : ι) → X i), f (x i) ∂Measure.pi μ = ∫ (x : X i), f x ∂μ i

Tactic:
rw [← (measurePreserving_eval μ i).map_eq, integral_map]
  · exact Measurable.aemeasurable (by fun_prop)
  · rwa [(measurePreserving_eval μ i).map_eq]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
| ↑p.1 ^ 2

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

Goal state after:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
| (Complex.sin ↑p.2 ^ 2 + Complex.cos ↑p.2 ^ 2) * ↑p.1 ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) volume

Tactic:
simpa using

Goal state after:
case inl
b : ℝ
hb : b ≤ 0
⊢ b ≤ 0
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:
(conv_lhs => rw [mul_assoc]); (conv_rhs => rw [mul_assoc])
      gcongr _ * ?_
      refine (le_abs_self _).trans ?_
      rw [abs_mul]
      gcongr

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

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

Tactic:
simpa using

Goal state after:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
⊢ -s.re < ↑n
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
h'f : Integrable (𝓕 f) volume
v : V
this : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • 𝓕 f w) volume
⊢ Tendsto (fun c ↦ ∫ (w : V), cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))

Tactic:
convert! tendsto_integral_cexp_sq_smul this using 4 with c w

Goal state after:
case e'_3
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
this : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • 𝓕 f w) volume
c : ℝ
w : V
⊢ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w = cexp (-↑c⁻¹ * ↑‖w‖ ^ 2) • 𝐞 ⟪w, v⟫ • 𝓕 f w

case e'_5
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
this : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • 𝓕 f w) volume
⊢ 𝓕⁻ (𝓕 f) v = ∫ (v_1 : V), 𝐞 ⟪v_1, v⟫ • 𝓕 f v_1
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
y : ℝ
hy : y ∈ uIoc 0 c
⊢ |y| ≤ |c|

Tactic:
simpa using

Goal state after:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
y : ℝ
hy : y ∈ uIoc 0 c
⊢ |y| ≤ |c|
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)
⊢ ↑r⁻¹ * ∫ (x : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑x ^ (a - 1) * cexp (-↑x) =
    1 / ↑r * ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑t ^ (a - 1) * cexp (-↑t)

Tactic:
← one_div,

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ ↑(1 / r) * ∫ (x : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑x ^ (a - 1) * cexp (-↑x) =
    1 / ↑r * ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑t ^ (a - 1) * cexp (-↑t)
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)
⊢ ∫ (x : ℝ) in Iic 0, f x = ∫ (x : ℝ) in Ioi 0, f (-x)

Tactic:
simpa using

Goal state after:
b : ℂ
hb : 0 < b.re
f : ℝ → ℂ := fun x ↦ cexp (-b * ↑x ^ 2)
full_integral : ∫ (x : ℝ), cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2)
⊢ ∫ (x : ℝ) in Iic 0, cexp (-(b * ↑x ^ 2)) = ∫ (x : ℝ) in Ioi 0, cexp (-(b * ↑x ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: ⊢ Gamma 0 = 0

Tactic:
simpa using

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

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

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ Gamma (-↑n) = 0
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 : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)) * 2 = (↑π / b) ^ (1 / 2)
h_eq : ∫ (x : ℝ) in Iic 0, f x = ∫ (x : ℝ) in Ioi 0, f x
⊢ (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)) * 2 = (↑π / b) ^ (1 / 2)

Tactic:
simpa using

Goal state after:
b : ℂ
hb : 0 < b.re
f : ℝ → ℂ := fun x ↦ cexp (-b * ↑x ^ 2)
full_integral : (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)) * 2 = (↑π / b) ^ (1 / 2)
h_eq : ∫ (x : ℝ) in Iic 0, f x = ∫ (x : ℝ) in Ioi 0, f x
⊢ (∫ (x : ℝ) in Ioi 0, cexp (-(b * ↑x ^ 2))) * 2 = (↑π / b) ^ 2⁻¹
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 : ℝ
this :
  (((∫ (x : ℝ) in (-↑T).re..(↑T + ↑c * I).re, cexp (-b * (↑x + ↑(-↑T).im * I) ^ 2)) -
          ∫ (x : ℝ) in (-↑T).re..(↑T + ↑c * I).re, cexp (-b * (↑x + ↑(↑T + ↑c * I).im * I) ^ 2)) +
        I • ∫ (y : ℝ) in (-↑T).im..(↑T + ↑c * I).im, cexp (-b * (↑(↑T + ↑c * I).re + ↑y * I) ^ 2)) -
      I • ∫ (y : ℝ) in (-↑T).im..(↑T + ↑c * I).im, cexp (-b * (↑(-↑T).re + ↑y * I) ^ 2) =
    0
⊢ I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0

Tactic:
simpa using

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 : ℝ
this :
  (((∫ (x : ℝ) in (-↑T).re..(↑T + ↑c * I).re, cexp (-b * (↑x + ↑(-↑T).im * I) ^ 2)) -
          ∫ (x : ℝ) in (-↑T).re..(↑T + ↑c * I).re, cexp (-b * (↑x + ↑(↑T + ↑c * I).im * I) ^ 2)) +
        I • ∫ (y : ℝ) in (-↑T).im..(↑T + ↑c * I).im, cexp (-b * (↑(↑T + ↑c * I).re + ↑y * I) ^ 2)) -
      I • ∫ (y : ℝ) in (-↑T).im..(↑T + ↑c * I).im, cexp (-b * (↑(-↑T).re + ↑y * I) ^ 2) =
    0
⊢ I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e'_2
⊢ Gamma (1 / 2) = ↑(Real.Gamma (1 / 2))

Tactic:
simpa using

Goal state after:
case e'_2
⊢ Gamma 2⁻¹ = ↑(Real.Gamma 2⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

Tactic:
simpa using

Goal state after:
case succ
k : ℕ
⊢ Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : Gamma (s + 1) ≠ 0
⊢ s ≠ 0

Tactic:
simpa using

Goal state after:
case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : Gamma (s + 1) ≠ 0
⊢ ¬s = 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
H : ¬Integrable (fun x ↦ cexp (b * ↑x ^ 2 + c * ↑x + d)) volume
⊢ False

Tactic:
simpa using

Goal state after:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
H : ¬Integrable (fun x ↦ cexp (b * ↑x ^ 2 + c * ↑x + d)) volume
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c d : ℂ
⊢ (-b).re < 0

Tactic:
simpa using

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
⊢ (-↑π * b).re < 0

Tactic:
simpa using

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
⊢ 0 < π * b.re
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ (𝓕 fun x ↦ cexp (-↑π * b * ↑x ^ 2)) = fun t ↦ 1 / b ^ (1 / 2) * cexp (-↑π / b * ↑t ^ 2)

Tactic:
simpa using

Goal state after:
b : ℂ
hb : 0 < b.re
⊢ (𝓕 fun x ↦ cexp (-↑π * b * ↑x ^ 2)) = fun t ↦ 1 / b ^ (1 / 2) * cexp (-↑π / b * ↑t ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ (-b i).re < 0

Tactic:
simpa using

Goal state after:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
⊢ 0 < (b i).re
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
hb : 0 < b.re
⊢ ∫ (v : V), cexp (-b * ↑‖v‖ ^ 2) = (↑π / b) ^ (↑(Module.finrank ℝ V) / 2)

Tactic:
simpa using

Goal state after:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
⊢ ∫ (v : V), cexp (-(b * ↑‖v‖ ^ 2)) = (↑π / b) ^ (↑(Module.finrank ℝ V) / 2)
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
hb : 0 < b.re
w : V
⊢ 𝓕 (fun v ↦ cexp (-b * ↑‖v‖ ^ 2)) w = (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑‖w‖ ^ 2 / b)

Tactic:
simpa using

Goal state after:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
w : V
⊢ 𝓕 (fun v ↦ cexp (-(b * ↑‖v‖ ^ 2))) w = (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (-(↑π ^ 2 * ↑‖w‖ ^ 2) / b)
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
f : 𝓢(V, E)
x : V
⊢ Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume

Tactic:
simpa using

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
f : 𝓢(V, E)
x : V
⊢ Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℂ E
V : Type u_3
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace ℝ V
inst✝⁸ : FiniteDimensional ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℂ G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L⋆[ℂ] F →L[ℂ] G
⊢ ∫ (ξ : V), (M ((𝓕 f) ξ)) ((𝓕 g) ξ) = ∫ (x : V), (M (f x)) (g x)

Tactic:
simpa using

Goal state after:
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℂ E
V : Type u_3
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace ℝ V
inst✝⁸ : FiniteDimensional ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℂ G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L⋆[ℂ] F →L[ℂ] G
⊢ ∫ (ξ : V), (M ((𝓕 f) ξ)) ((𝓕 g) ξ) = ∫ (x : V), (M (f x)) (g x)
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
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : 𝓢(V, F)
⊢ ∀ (x : V), ‖(𝓕 f).toBoundedContinuousFunction x‖ ≤ ‖f.toLp 1 volume‖

Tactic:
simpa using

Goal state after:
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : 𝓢(V, F)
⊢ ∀ (x : V), ‖(𝓕 f) x‖ ≤ ‖f.toLp 1 volume‖
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
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : 𝓢(V, F)
⊢ ∀ (x : V), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑(𝓕 f)) x‖ ≤ ‖f.toLp 1 volume‖

Tactic:
simpa using

Goal state after:
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : 𝓢(V, F)
⊢ ∀ (x : V), ‖(𝓕 f) x‖ ≤ ‖f.toLp 1 volume‖
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 : 𝓢(V, H)
⊢ Complex.ofRealLI (∫ (ξ : V), ‖(𝓕 f) ξ‖ ^ 2) = Complex.ofRealLI (∫ (x : V), ‖f x‖ ^ 2)

Tactic:
simpa using

Goal state after:
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 : 𝓢(V, H)
⊢ ∫ (x : V), ↑‖(𝓕 f) x‖ ^ 2 = ∫ (x : V), ↑‖f x‖ ^ 2
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst✝³ : FunLike F α β
inst✝² : TopologicalSpace α
inst✝¹ : Zero β
inst✝ : Zero V
f : F → V
x : α
⊢ x ∈ dsupport f ↔ ∀ (i : Set α), x ∈ i ∧ IsOpen[inst✝²] i → ¬IsVanishingOn f i

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst✝³ : FunLike F α β
inst✝² : TopologicalSpace α
inst✝¹ : Zero β
inst✝ : Zero V
f : F → V
x : α
⊢ x ∈ dsupport f ↔ ∀ (i : Set α), x ∈ i → IsOpen[inst✝²] i → ¬IsVanishingOn f i
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
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
⊢ (fun a ↦ ↑↑(g.toLp (1 - p⁻¹)⁻¹ μ) a • ↑↑f a) =ᵐ[μ] fun a ↦ g a • ↑↑f a

Tactic:
filter_upwards [g.coeFn_toLp (1 - p⁻¹)⁻¹ μ] with x hg

Goal state after:
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
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
x : E
hg : ↑↑(g.toLp (1 - p⁻¹)⁻¹ μ) x = g x
⊢ ↑↑(g.toLp (1 - p⁻¹)⁻¹ μ) x • ↑↑f x = g x • ↑↑f x
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: case h
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 → ℝ), ContDiff ℝ ∞ g → HasCompactSupport g → ∫ (x : E), g x • ↑↑f x ∂μ = 0

Tactic:
intro g g_smooth g_cpt
    have hg₁ : HasCompactSupport (Complex.ofRealCLM ∘ g) := g_cpt.comp_left rfl
    have hg₂ : ContDiff ℝ ∞ (Complex.ofRealCLM ∘ g) := by fun_prop
    calc
      _ = toTemperedDistributionCLM F μ p f (hg₁.toSchwartzMap hg₂) := by simp
      _ = _ := by simp [hf]

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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
⊢ Integrable (fun p ↦ ‖B‖ * (‖f₁ (p.1 - p.2)‖ * ‖f₂ p.2‖)) (volume.prod volume)

Tactic:
simpa using

Goal state after:
𝕜 : 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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
⊢ Integrable (fun p ↦ ‖f₁ (p.1 - p.2)‖ * ‖f₂ p.2‖ * ‖B‖) (volume.prod volume)
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝¹ : Fintype d
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
⊢ (span ℂ (range (mFourierLp p))).topologicalClosure = ⊤

Tactic:
simpa using

Goal state after:
d : Type u_1
inst✝¹ : Fintype d
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
⊢ (span ℂ (range (mFourierLp p))).topologicalClosure = ⊤
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i ↦ mFourierCoeff (↑↑f) i • mFourierLp 2 i) f

Tactic:
simpa using

Goal state after:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i ↦ mFourierCoeff (↑↑f) i • mFourierBasis i) f
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i ↦ ‖mFourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : UnitAddTorus d), ‖↑↑f t‖ ^ 2)

Tactic:
simpa using

Goal state after:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i ↦ ‖mFourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : UnitAddTorus d), ‖↑↑f t‖ ^ 2)
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ (𝓕 ((toTemperedDistributionCLM E F volume) f)) g = ((toTemperedDistributionCLM E F volume) (𝓕 f)) g

Tactic:
simpa using

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ ∫ (x : E), (𝓕 g) x • f x = ∫ (x : E), g x • (𝓕 f) x
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
sum_L2 : HasSum (fun i ↦ mFourierCoeff (⇑f) i • mFourierLp 2 i) ((ContinuousMap.toLp 2 volume ℂ) f)
⊢ Summable fun a ↦ ‖mFourierCoeff (⇑f) a • mFourier a‖

Tactic:
simpa using

Goal state after:
d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
sum_L2 : HasSum (fun i ↦ mFourierCoeff (⇑f) i • mFourierLp 2 i) ((ContinuousMap.toLp 2 volume ℂ) f)
⊢ Summable fun a ↦ ‖mFourierCoeff (⇑f) a‖