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

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

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

Goal state before:
pp: case refine_1
b : ℂ
hb : 0 < b.re
⊢ Continuous fun x ↦ -b * ↑x ^ 2

Tactic:
fun_prop

Goal state after:
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✝ : ∀ (i : ι), IsFiniteMeasure (μ i)
i : ι
f : X i → E
hf : Integrable f (μ i)
⊢ Measurable fun x ↦ x i

Tactic:
fun_prop

Goal state after:
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)
⊢ Measurable (Function.eval i)

Tactic:
fun_prop

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

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

Tactic:
dsimp only [GammaAux]

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 succ
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑(n + 1)
⊢ GammaAux (n + 1) s = GammaAux (n + 1) (s + 1) / s

Tactic:
dsimp only [GammaAux]

Goal state after:
case succ
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑(n + 1)
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
dsimp only [GammaAux]

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 succ
s : ℂ
n : ℕ
h1 : -s.re < ↑(n + 1)
⊢ GammaAux (n + 1) s = GammaAux (n + 1 + 1) s

Tactic:
dsimp only [GammaAux]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x ↦ cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
f_le_bd : ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)
⊢ ∀ (x : ℂ), AEStronglyMeasurable (fun x_1 ↦ cexp (-x * ↑x_1 ^ 2)) volume

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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
hf : Integrable f volume
c : ℝ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun a ↦ cexp (-↑c⁻¹ * ↑‖a‖ ^ 2)

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

Goal state before:
pp: case a
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ -↑(⌊-s⌋₊ + 1) < s

Tactic:
neg_lt,

Goal state after:
case a
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ -s < ↑(⌊-s⌋₊ + 1)
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:
add_right_comm,

Goal state after:
case succ
k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ Gamma (↑(k + 1) + 1 / 2 + 1) = ↑(2 * (k + 1) + 1)‼ * √π / 2 ^ (k + 1 + 1)
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:
fun_prop

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

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
⊢ ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2

Tactic:
fun_prop

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
i : Fin (Module.finrank ℝ E)
x : E
⊢ Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i)

Tactic:
fun_prop

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

Goal state before:
pp: case e'_2
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
b : ℝ
hb : 0 < b
⊢ ∫ (x : V), ofRealLI (rexp (-b * ‖x‖ ^ 2)) = ∫ (v : V), cexp (-↑b * ↑‖v‖ ^ 2)

Tactic:
simp [ofRealLI]

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
⊢ ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2

Tactic:
fun_prop

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
i : Fin (Module.finrank ℝ E)
x : 𝓢(E, ℂ)
⊢ Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i))

Tactic:
fun_prop

Goal state after:
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
𝕜' : Type u_4
inst✝⁶ : NormedField 𝕜'
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G : Type u_6
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℂ G
inst✝¹ : NormedSpace 𝕜' G
inst✝ : SMulCommClass ℝ 𝕜' G
f : 𝓢(V, F →L[ℝ] G)
m : F
⊢ 𝓕 ((SchwartzMap.evalCLM 𝕜' V G m) f) = (SchwartzMap.evalCLM 𝕜' V G m) (𝓕 f)

Tactic:
by
  ext x
  exact (fourier_continuousLinearMap_apply f.integrable).symm

Goal state after:
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 : 𝓢(V, E)
m : V
⊢ Function.HasTemperateGrowth fun x ↦ inner ℝ x m

Tactic:
fun_prop

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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn (⇑f) s
m : E
u : 𝓢(E, ℂ)
hu : tsupport ⇑u ⊆ s
⊢ f (∂_{m} u) = 0

Tactic:
exact hf (∂_{m} u) <| (tsupport_fderiv_apply_subset ℝ m).trans hu

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

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

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

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

Goal state before:
pp: case a
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ dsupport ⇑(TemperedDistribution.delta x) ⊆ {x}

pp: case a
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ {x} ⊆ dsupport ⇑(TemperedDistribution.delta x)

Tactic:
· intro x' hx'
    rw [mem_dsupport_iff] at hx'
    exact hx' {x} (isVanishingOn_delta x) (T1Space.t1 x)

Goal state after:
case a
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ {x} ⊆ dsupport ⇑(TemperedDistribution.delta x)
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: 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)
s : Set E
hf : IsVanishingOn (⇑f) s
m : E
u : 𝓓(Ω, ℝ)
hu : tsupport ⇑u ⊆ s
⊢ f (∂_{m} u) = 0

Tactic:
exact hf (∂_{m} u) <| (tsupport_fderiv_apply_subset ℝ m).trans hu

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

Goal state before:
pp: 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)
⊢ Function.HasTemperateGrowth fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))

Tactic:
fun_prop

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

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

Goal state before:
pp: 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)
⊢ Function.HasTemperateGrowth fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s' / 2))

Tactic:
fun_prop

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

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

Goal state before:
pp: case a
E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
⊢ dsupport ⇑(delta x) ⊆ {x}

pp: case a
E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
⊢ {x} ⊆ dsupport ⇑(delta x)

Tactic:
· intro x' hx'
    rw [mem_dsupport_iff] at hx'
    exact hx' {x} (isVanishingOn_delta x) (T1Space.t1 x)

Goal state after:
case a
E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
⊢ {x} ⊆ dsupport ⇑(delta x)
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ Continuous fun x ↦ ∏ i, (fourier (n i)) (x i)

Tactic:
fun_prop

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

Goal state before:
pp: 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
m : E
f : 𝓢'(E, F)
⊢ Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x m)

Tactic:
fun_prop

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

Goal state before:
pp: 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
m : E
f : 𝓢'(E, F)
⊢ Function.HasTemperateGrowth fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-1 / 2))

Tactic:
fun_prop

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

Goal state before:
pp: 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
f : 𝓢'(E, F)
⊢ Function.HasTemperateGrowth fun x ↦ ↑(‖x‖ ^ 2)

Tactic:
fun_prop

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

Goal state before:
pp: 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
f : 𝓢'(E, F)
⊢ Function.HasTemperateGrowth fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-2 / 2))

Tactic:
fun_prop

Goal state after:
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)
⊢ ContDiff ℝ ∞ (⇑Complex.ofRealCLM ∘ g)

Tactic:
fun_prop

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

Goal state before:
pp: 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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ Function.HasTemperateGrowth fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))

Tactic:
fun_prop

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)
⊢ Continuous fun a ↦ -inner ℝ a.1 ξ

Tactic:
fun_prop

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t = mFourierCoeff (↑↑f) i

Tactic:
· apply integral_congr_ae
    filter_upwards [coeFn_mFourierLp 2 i] with _ ht
    rw [ht, ← mFourier_neg, smul_eq_mul]

Goal state after:
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
f : 𝓢'(E, F)
m : E
u : 𝓢(E, ℂ)
⊢ Function.HasTemperateGrowth fun x ↦ inner ℝ x m

Tactic:
fun_prop

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

Goal state before:
pp: 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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
⊢ Function.HasTemperateGrowth fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : RCLike 𝕜
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → InnerProductSpace 𝕜 (E i)
𝕝 : Type u_5
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : StarModule 𝕝 𝕜
inst✝¹ : (i : ι) → Module 𝕝 (E i)
inst✝ : ∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)
c : 𝕝
w : ι → ℝ
f g : (i : ι) → E i
⊢ ⟪f, c • g⟫_[𝕜, w] = c • ⟪f, g⟫_[𝕜, w]

Tactic:
simp_rw [wInner, Pi.smul_apply, inner_smul_right_eq_smul, smul_sum, smul_comm c]

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

Goal state before:
pp: E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
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✝⁴ : CompleteSpace F₁
inst✝³ : CompleteSpace F₂
inst✝² : CompleteSpace 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
⊢ ∫ (y : E), (∫ (x : E), B (𝐞 (-inner ℝ x ξ) • f₁ x)) (𝐞 (-inner ℝ y ξ) • f₂ y) =
    ∫ (x : E), (B (∫ (x : E), 𝐞 (-inner ℝ x ξ) • f₁ x)) (𝐞 (-inner ℝ x ξ) • f₂ x)

Tactic:
← integral_comp_comm _ (by simpa using hf₁)

Goal state after:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
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✝⁴ : CompleteSpace F₁
inst✝³ : CompleteSpace F₂
inst✝² : CompleteSpace 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
⊢ ∫ (y : E), (∫ (x : E), B (𝐞 (-inner ℝ x ξ) • f₁ x)) (𝐞 (-inner ℝ y ξ) • f₂ y) =
    ∫ (x : E), (∫ (x : E), B (𝐞 (-inner ℝ x ξ) • f₁ x)) (𝐞 (-inner ℝ x ξ) • f₂ x)
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: 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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
this✝ : MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume
this : MemLp (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) 2 volume
⊢ Function.HasTemperateGrowth fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))

Tactic:
fun_prop

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

Goal state before:
pp: 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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
this✝ : MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume
this : MemLp (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) 2 volume
⊢ Function.HasTemperateGrowth fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))

Tactic:
fun_prop

Goal state after: