mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(E, F)
c : 𝕜
x : E
⊢ ‖x‖ ^ k * ‖c • iteratedFDeriv ℝ n (⇑f) x‖ = ‖x‖ ^ k * (‖c‖ * ‖iteratedFDeriv ℝ n (⇑f) x‖)

Tactic:
norm_smul c (iteratedFDeriv ℝ n (⇑f) x)

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(E, F)
c : 𝕜
x : E
⊢ ‖x‖ ^ k * (‖c‖ * ‖iteratedFDeriv ℝ n (⇑f) x‖) = ‖x‖ ^ k * (‖c‖ * ‖iteratedFDeriv ℝ n (⇑f) x‖)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ ∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    ∑ i ∈ Finset.range (m.1 + 1), ↑(m.1.choose i) * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
have hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1) := by grind

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
⊢ ∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    ∑ i ∈ Finset.range (m.1 + 1), ↑(m.1.choose i) * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case hbc.succ
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
inst✝⁴ : NormedAddCommGroup D
inst✝³ : NormedSpace ℝ D
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace 𝕜 F
L : E →L[ℝ] G →L[ℝ] ℝ
k : ℕ
f : 𝓢(E, F)
x : E
n : ℕ
⊢ ↑((n + 1).choose 0) * ‖iteratedFDeriv ℝ 0 (⇑L) x‖ * ‖iteratedFDeriv ℝ (n + 1 - 0) (⇑f) x‖ +
      ∑ k ∈ Finset.range (n + 1),
        ↑((n + 1).choose (k + 1)) * ‖iteratedFDeriv ℝ (k + 1) (⇑L) x‖ * ‖iteratedFDeriv ℝ (n + 1 - (k + 1)) (⇑f) x‖ ≤
    ‖L x‖ * ‖iteratedFDeriv ℝ (n + 1) (⇑f) x‖ + ↑(n + 1) * ‖L‖ * ‖iteratedFDeriv ℝ (n + 1 - 1) (⇑f) x‖

Tactic:
have : ∑ k ∈ Finset.range n,
                (((n + 1).choose (k + 1 + 1)) : ℝ) * ‖iteratedFDeriv ℝ (k + 1 + 1) L x‖ *
                ‖iteratedFDeriv ℝ (n + 1 - (k + 1 + 1)) f x‖ = 0 := by
              apply Finset.sum_eq_zero
              simp [iteratedFDeriv_succ_eq_comp_right, iteratedFDeriv_succ_const]
            simp [Finset.sum_range_succ', this]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
⊢ (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'

Tactic:
rw [pow_mul, ← mul_pow]

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
⊢ (1 + ‖x‖) ^ (k + l * n) ≤ ((1 + Cg) * (1 + ‖g x‖) ^ kg) ^ (k + l * n)
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case zero_eq
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
w : W
⊢ (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v 0) w).curry0 =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f w

Tactic:
rw [curry0_apply, Matrix.zero_empty, fourierIntegral_continuousMultilinearMap_apply'
      (integrable_fourierPowSMulRight L (hf 0 bot_le) h'f)]

Goal state after:
case zero_eq
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
w : W
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x ↦ (fourierPowSMulRight L f x 0) ![]) w =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f w
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n ≤ N
w : W
⊢ iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v n) w

Tactic:
exact ((hasFTaylorSeriesUpTo_fourierIntegral' L hf h'f).eq_iteratedFDeriv
    (mod_cast hn) w).symm

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

Goal state before:
pp: E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
n : ℕ
h'f : Integrable (⇑(continuousMultilinearCurryLeftEquiv ℝ (fun x ↦ V) E).symm ∘ fderiv ℝ (iteratedFDeriv ℝ n f)) μ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f) = fun w ↦
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
⊢ Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ

Tactic:
Function.comp_def,

Goal state after:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
n : ℕ
h'f :
  Integrable (fun x ↦ (continuousMultilinearCurryLeftEquiv ℝ (fun x ↦ V) E).symm (fderiv ℝ (iteratedFDeriv ℝ n f) x)) μ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f) = fun w ↦
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
⊢ Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case succ
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f) = fun w ↦
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ
h'n : ↑n < N
⊢ ((fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f)) w)
        (m 0))
      (Fin.tail m) =
    (-(2 * ↑π * I)) ^ (n + 1) • (∏ x, -(L (m x)) w) • ∫ (v : V), 𝐞 (-(L v) w) • f v ∂μ

Tactic:
simp only [ih h'n.le, fourierSMulRight_apply, neg_apply, ContinuousLinearMap.flip_apply,
      neg_smul, smul_neg, neg_neg, smul_apply, fourierPowSMulRight_apply, ← coe_smul (E := E),
      smul_smul]

Goal state after:
case succ
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f) = fun w ↦
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ
h'n : ↑n < N
⊢ (2 * ↑π * I * (↑((L (m 0)) w) * ((-(2 * ↑π * I)) ^ n * ↑(∏ i, -(L (Fin.tail m i)) w)))) •
      fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f w =
    ((-(2 * ↑π * I)) ^ (n + 1) * ↑(∏ x, -(L (m x)) w)) • ∫ (v : V), 𝐞 (-(L v) w) • f v ∂μ
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
m : MeasurableEmbedding fun x ↦ -x := Homeomorph.measurableEmbedding (Homeomorph.neg ℝ)
⊢ IntegrableOn ((fun x ↦ f |x|) ∘ fun x ↦ -x) ((fun x ↦ -x) ⁻¹' Iic 0) volume

Tactic:
Function.comp_def,

Goal state after:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
m : MeasurableEmbedding fun x ↦ -x := Homeomorph.measurableEmbedding (Homeomorph.neg ℝ)
⊢ IntegrableOn (fun x ↦ f |(-x)|) ((fun x ↦ -x) ⁻¹' Iic 0) volume
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := (ContinuousLinearMap.mul ℝ ℝ).flip
⊢ HasDerivAt (𝓕 f) (𝓕 (fun x ↦ (-2 * ↑π * I * ↑x) • f x) w) w

Tactic:
have h_int : Integrable fun v ↦ fourierSMulRight L f v := by
    suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by
      simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using! this.smul (-2 * π * I)
    convert! ((ContinuousLinearMap.toSpanSingletonLIE ℝ
      E).toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with _ v
    apply ContinuousLinearMap.ext_ring
    rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.flip_apply,
      ContinuousLinearMap.mul_apply', one_mul, map_smul]
    exact congr_arg (fun x ↦ v • x) (one_smul ℝ (f v)).symm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := (ContinuousLinearMap.mul ℝ ℝ).flip
h_int : Integrable (fun v ↦ fourierSMulRight L f v) volume
⊢ HasDerivAt (𝓕 f) (𝓕 (fun x ↦ (-2 * ↑π * I * ↑x) • f x) w) w
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (deriv f) volume
⊢ 𝓕 (deriv f) = fun x ↦ (2 * ↑π * I * ↑x) • 𝓕 f x

Tactic:
by
  ext x
  have I : Integrable (fun x ↦ fderiv ℝ f x) := by
    simpa only [← toSpanSingleton_deriv] using!
      (ContinuousLinearMap.smulRightL ℝ ℝ E 1).integrable_comp hf'
  have : 𝓕 (deriv f) x = 𝓕 (fderiv ℝ f) x 1 := by
    simp only [fourier_continuousLinearMap_apply I, fderiv_apply_one_eq_deriv]
  rw [this, fourier_fderiv hf h'f I]
  simp only [fourierSMulRight_apply, neg_apply, innerSL_apply_apply ℝ, smul_smul,
    RCLike.inner_apply', conj_trivial, mul_one, neg_smul, smul_neg, neg_neg, neg_mul, ← coe_smul]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedDeriv n f) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume
⊢ ((𝓕 (iteratedFDeriv ℝ n f) x) fun x ↦ 1) = (2 * ↑π * I * ↑x) ^ n • 𝓕 f x

Tactic:
fourier_iteratedFDeriv hf A hn

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedDeriv n f) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume
⊢ ((fourierPowSMulRight (-innerSL ℝ) (𝓕 f) x n) fun x ↦ 1) = (2 * ↑π * I * ↑x) ^ n • 𝓕 f x
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ |(-x) ^ s * rexp (-b * x ^ 2)| ≤ x ^ s * rexp (-b * x ^ 2)

Tactic:
abs_mul,

Goal state after:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ |(-x) ^ s| * |rexp (-b * x ^ 2)| ≤ x ^ s * rexp (-b * x ^ 2)
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedCommRing 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ Integrable ((fun x ↦ ∏ i, f (e i) (x (e i))) ∘ ⇑(Equiv.piCongrLeft E e)) (Measure.pi fun i' ↦ μ (e i'))

Tactic:
Function.comp_def,

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedCommRing 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ Integrable (fun x ↦ ∏ i, f (e i) ((Equiv.piCongrLeft E e) x (e i))) (Measure.pi fun i' ↦ μ (e i'))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ ContinuousOn (fun {b} ↦ (↑π / b) ^ (1 / 2)) {c | 0 < c.re}

Tactic:
refine
      continuousOn_of_forall_continuousAt fun b hb =>
        (continuousAt_cpow_const (Or.inl ?_)).comp (continuousAt_const.div continuousAt_id (nv hb))
    rw [div_re, ofReal_im, ofReal_re, zero_mul, zero_div, add_zero]
    exact div_pos (mul_pos pi_pos hb) (normSq_pos.mpr (nv hb))

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

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

Tactic:
← add_zero (-b * x ^ 2 + I * t * x)

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
x : ℝ
| cexp (-b * ↑x ^ 2 + I * t * ↑x + 0)
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
m : E
f : 𝓢(E, F)
⊢ ∂_{m} f = (2 * ↑π * Complex.I) • 𝓕⁻ ((smulLeftCLM F fun x ↦ inner ℝ x m) (𝓕 f))

Tactic:
← FourierTransform.fourierInv_smul,

Goal state after:
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
m : E
f : 𝓢(E, F)
⊢ ∂_{m} f = 𝓕⁻ ((2 * ↑π * Complex.I) • (smulLeftCLM F fun x ↦ inner ℝ x m) (𝓕 f))
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 : ℂ
⊢ (fourierMultiplierCLM F fun x ↦ c) = c • ContinuousLinearMap.id ℂ 𝓢'(E, F)

Tactic:
by
  ext
  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
m : E
f : 𝓢'(E, F)
⊢ ∂_{m} f = (2 * ↑π * Complex.I) • 𝓕⁻ ((smulLeftCLM F fun x ↦ ↑(inner ℝ x m)) (𝓕 f))

Tactic:
← FourierTransform.fourierInv_smul,

Goal state after:
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
m : E
f : 𝓢'(E, F)
⊢ ∂_{m} f = 𝓕⁻ ((2 * ↑π * Complex.I) • (smulLeftCLM F fun x ↦ ↑(inner ℝ x m)) (𝓕 f))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: case h
𝕜 : 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
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
a✝ : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 (⇑f) v‖ ≤
    (2 ^ volume.integrablePower * ∫ (x : V), (1 + ‖x‖) ^ (-↑volume.integrablePower)) * 2 *
      ((Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)).sup (schwartzSeminormFamily 𝕜 V E)) f

Tactic:
apply (f.integral_pow_mul_iteratedFDeriv_le 𝕜 ..).trans

Goal state after:
case h
𝕜 : 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
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
a✝ : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ (2 ^ volume.integrablePower * ∫ (x : V), (1 + ‖x‖) ^ (-↑volume.integrablePower) ∂volume) *
      ((SchwartzMap.seminorm 𝕜 0 p.2) f + (SchwartzMap.seminorm 𝕜 (p.1 + volume.integrablePower) p.2) f) ≤
    (2 ^ volume.integrablePower * ∫ (x : V), (1 + ‖x‖) ^ (-↑volume.integrablePower)) * 2 *
      ((Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)).sup (schwartzSeminormFamily 𝕜 V E)) f
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)
⊢ (besselPotential E F (-1)) ((2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x m)) f) =
    (2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x m * (1 + ‖x‖ ^ 2) ^ (-1 / 2))) f

Tactic:
besselPotential,

Goal state after:
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)
⊢ (fourierMultiplierCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-1 / 2)))
      ((2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x m)) f) =
    (2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x m * (1 + ‖x‖ ^ 2) ^ (-1 / 2))) f
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)
⊢ (besselPotential E F (-2)) (-(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2)) f) =
    -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))) f

Tactic:
besselPotential,

Goal state after:
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)
⊢ (fourierMultiplierCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-2 / 2)))
      (-(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2)) f) =
    -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))) f
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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 g : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf : (besselPotential E F s) f = Lp.toTemperedDistribution f'
g' : ↥(Lp F p volume)
hg : (besselPotential E F s) g = Lp.toTemperedDistribution g'
⊢ (besselPotential E F s) (f + g) = Lp.toTemperedDistribution (f' + g')

Tactic:
rw [← Lp.toTemperedDistributionCLM_apply]

Goal state after:
case h
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 g : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf : (besselPotential E F s) f = Lp.toTemperedDistribution f'
g' : ↥(Lp F p volume)
hg : (besselPotential E F s) g = Lp.toTemperedDistribution g'
⊢ (besselPotential E F s) (f + g) = (Lp.toTemperedDistributionCLM F volume p) (f' + g')