mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁷ : TopologicalSpace α
inst✝⁶ : SecondCountableTopology α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
inst✝³ : LinearOrder α
inst✝² : CompactIccSpace α
inst✝¹ : atBot.IsMeasurablyGenerated
inst✝ : OrderTop α
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ Integrable f μ

Tactic:
refine integrable_iff_integrableAtFilter_atBot.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁷ : TopologicalSpace α
inst✝⁶ : SecondCountableTopology α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
inst✝³ : LinearOrder α
inst✝² : CompactIccSpace α
inst✝¹ : atBot.IsMeasurablyGenerated
inst✝ : OrderTop α
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ StronglyMeasurableAtFilter f atBot μ
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✝¹⁰ : TopologicalSpace α
inst✝⁹ : SecondCountableTopology α
inst✝⁸ : MeasurableSpace α
μ : Measure α
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : AddCommGroup α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedAddMonoid α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ Measure.map Neg.neg (μ.restrict (Ici 0)) = Measure.map Neg.neg (μ.restrict (Neg.neg ⁻¹' Iic 0))

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: c : ℝ
hc : 1 < c
⊢ (log c)⁻¹ = 0 - -(log c)⁻¹

Tactic:
simp

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

Goal state before:
pp: case e'_5
c : ℝ
hc : 1 < c
⊢ 𝓝 0 = 𝓝 (-0)

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f g : ↥(Lp E 1 volume)
x✝ x : V
h₁ : ↑↑(f + g) x = (↑↑f + ↑↑g) x
⊢ 𝐞 (-⟪x, x✝⟫) • (↑↑f + ↑↑g) x = 𝐞 (-⟪x, x✝⟫) • ↑↑f x + 𝐞 (-⟪x, x✝⟫) • ↑↑g x

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case right
s : ℂ
hs : 0 < s.re
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re

Tactic:
simp

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

Goal state before:
pp: s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(rexp (-x)) * ↑x ^ ↑(s - 1)

Tactic:
simp

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

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

Tactic:
refine this.congr_fun (fun _ hx => ?_) measurableSet_Ioi

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
⊢ (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) x✝ = (b ^ (-p⁻¹) * x✝) ^ s * rexp (-b * (b ^ (-p⁻¹) * x✝) ^ p)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case right
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))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ (2 * b)⁻¹ * ↑(π - -π) = ↑π / b

Tactic:
simp

Goal state after:
b : ℂ
hb : 0 < b.re
⊢ b⁻¹ * 2⁻¹ * (↑π + ↑π) = ↑π / b
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
simp

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

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

Tactic:
rw [GammaIntegral_add_one h1, mul_div_cancel_left₀]

Goal state after:
case zero.ha
s : ℂ
h1 : 0 < s.re
⊢ s ≠ 0
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
v : V
⊢ f v = cexp (-↑0 * ↑‖v‖ ^ 2) • f v

Tactic:
simp

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

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

Tactic:
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
⊢ 0 < re 1

Tactic:
simp

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

Goal state before:
pp: ⊢ GammaIntegral 1 = 1

Tactic:
simp

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

Goal state before:
pp: ⊢ 0 < re 1

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ Gamma (↑0 + 1) = ↑0!

Tactic:
simp

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

Goal state before:
pp: n : ℕ
IH : Gamma (-↑n) = 0
A : -↑n.succ ≠ 0
⊢ -↑n = -↑n.succ + 1

Tactic:
simp

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

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

Goal state before:
pp: case e_f.e_a.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
⊢ ↑π / ↑c⁻¹ = ↑π * ↑c

Tactic:
simp

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

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 e'_2.e'_7
b : ℝ
hb : 0 < b
x✝ : ℝ
⊢ ↑(rexp (-b * x✝ ^ 2)) = cexp (-↑b * ↑x✝ ^ 2)

Tactic:
simp

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

Goal state before:
pp: case e'_3
b : ℝ
hb : 0 < b
⊢ ↑(π / b) ^ ↑(1 / 2) / ↑2 = ↑(π / b) ^ (1 / 2) / 2

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ Gamma (↑0 + 1 + 1 / 2) = ↑(2 * 0 + 1)‼ * √π / 2 ^ (0 + 1)

Tactic:
simp [-one_div, add_comm (1 : ℝ), Gamma_add_one, Gamma_one_half_eq]

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

Tactic:
simp

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

Goal state after:
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
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))
B : Tendsto (fun c ↦ ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ π ^ ↑2 * (c ^ (2⁻¹ * ↑2) * ‖v - w‖ ^ ↑2) = π ^ ↑2 * (c * ‖v - w‖ ^ ↑2)

Tactic:
simp

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

Goal state before:
pp: case e'_3
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
b : ℝ
hb : 0 < b
⊢ ↑(π / b) ^ ↑(↑(Module.finrank ℝ V) / 2) = ↑(π / b) ^ (↑(Module.finrank ℝ V) / 2)

Tactic:
simp

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

Goal state before:
pp: case e_f.e_a
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
⊢ ↑π ^ 2 * Complex.I ^ 2 * 4 = { toFun := (↑↑(algebraMap ℝ ℂ)).toFun, map_zero' := ⋯ } (-(π ^ 2 * 4))

Tactic:
simp

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
c : ℂ
x✝¹ : 𝓢'(E, F)
x✝ : 𝓢(E, ℂ)
⊢ ((fourierMultiplierCLM F fun x ↦ c) x✝¹) x✝ = ((c • ContinuousLinearMap.id ℂ 𝓢'(E, F)) x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: case e_f.e_a
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, ℂ)
⊢ ↑π ^ 2 * Complex.I ^ 2 * 4 = ↑(-(π ^ 2 * 4))

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: case refine_4
𝕜 : 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
⊢ ∀ (n : ℕ × ℕ),
    ∃ s C,
      0 ≤ C ∧
        ∀ (f : 𝓢(V, E)) (x : V),
          ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (𝓕 ⇑f) x‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 V E)) f

Tactic:
· rintro ⟨k, n⟩
    refine ⟨Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1),
      (2 * π) ^ n * (2 * n + 2) ^ k * (Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card *
        2 ^ integrablePower (volume : Measure V) *
        (∫ x : V, (1 + ‖x‖) ^ (- integrablePower (volume : Measure V) : ℝ)) * 2, by positivity,
      fun f x ↦ ?_⟩
    apply (pow_mul_norm_iteratedFDeriv_fourier_le (f.smooth ⊤)
      (fun k n _hk _hn ↦ integrable_pow_mul_iteratedFDeriv _ f k n) le_top le_top x).trans
    simp only [mul_assoc]
    gcongr
    calc
    _ ≤ ∑ _ ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
        2 ^ integrablePower (volume : Measure V) *
          (∫ x : V, (1 + ‖x‖) ^ (- integrablePower (volume : Measure V) : ℝ)) * 2 *
          (Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1)).sup
          (schwartzSeminormFamily 𝕜 V E) f := by
      gcongr with p
      apply (f.integral_pow_mul_iteratedFDeriv_le 𝕜 ..).trans
      simp only [mul_assoc, two_mul]
      gcongr
      · have : (0, p.2) ∈ Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ
            Finset.range (k + 1) := by simp_all
        apply Seminorm.le_def.mp (Finset.le_sup (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2) this)
      · have : (p.1 + integrablePower (volume : Measure V), p.2) ∈ Finset.range
            (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1) := by simp_all
        apply Seminorm.le_def.mp (Finset.le_sup (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2) this)
    _ = _ := by simp [mul_assoc]

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
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:
simp

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

Goal state before:
pp: case succ
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
n : ℕ
IH : ∀ (m : Fin n → E), IsVanishingOn (⇑(∂^{m} f)) s
m : Fin (n + 1) → E
⊢ IsVanishingOn (⇑(∂^{m} f)) s

Tactic:
exact lineDerivOp (IH <| Fin.tail m) (m 0)

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

Goal state before:
pp: case succ
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
n : ℕ
IH : ∀ (m : Fin n → E), IsVanishingOn (⇑(∂^{m} f)) s
m : Fin (n + 1) → E
⊢ IsVanishingOn (⇑(∂^{m} f)) s

Tactic:
exact lineDerivOp (IH <| Fin.tail m) (m 0)

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✝)) =
    (toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F) (integralCLM ℂ μ ∘SL (pairing (lsmul ℂ ℂ).flip) x✝¹) +
      (toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F) (integralCLM ℂ μ ∘SL (pairing (lsmul ℂ ℂ).flip) x✝)

Tactic:
simp

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

Goal state before:
pp: case e'_4.e'_3
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) f = (𝓕 (𝓕⁻ f)).toLp 2 volume

Tactic:
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:
simp

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✝ : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
x : E
⊢ ↑↑(f.toLp p μ) x = f x → g x • ↑↑(f.toLp p μ) x = g x • f x

Tactic:
hf

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
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
x : E
hf : ↑↑(f.toLp p μ) x = f x
⊢ g x • ↑↑(f.toLp p μ) x = g x • f 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✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
x : E
hf : ↑↑(f.toLp p μ) x = f x
⊢ g x • ↑↑(f.toLp p μ) x = g x • f x

Tactic:
hf

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
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
x : E
hf : ↑↑(f.toLp p μ) x = f x
⊢ g x • f x = g x • f 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
he : Continuous ⇑e
hL : Continuous fun p ↦ (L p.1) p.2
w : W
x y : V
⊢ ‖↑(e ((L x) w))‖ ≤ 1

Tactic:
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:
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
x✝ : V
⊢ (char he hL 0) x✝ = 1 x✝

Tactic:
simp

Goal state after:
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
m : E
f : 𝓢'(E, F)
x : E
⊢ ((fun x ↦ ↑(inner ℝ x m)) * fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-1 / 2))) x = ↑(inner ℝ x m * (1 + ‖x‖ ^ 2) ^ (-1 / 2))

Tactic:
simp

Goal state after: