awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℂ F
f : 𝓢(V, F)
⊢ ∀ (x : V),
    HPow.hPow (β := ℕ) ‖x‖ 0 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_4} ℝ (fun (i : Fin 0) ↦ V) F)
          (iteratedFDeriv ℝ 0 (⇑(𝓕 f) : (a : V) → F) x) ≤
      Norm.norm (E := ↥(Lp F 1 volume)) (f.toLp 1 volume)

Tactic:
simpa using norm_fourier_apply_le_toLp_one f

Premises used: SchwartzMap.norm_fourier_apply_le_toLp_one
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : InnerProductSpace ℂ H
inst_7 : CompleteSpace H
f g : 𝓢(V, H)
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      inner.{0, u_4} ℂ (E := H) ((𝓕 f : (a : V) → H) ξ : H) ((𝓕 g : (a : V) → H) ξ : H))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      inner.{0, u_4} ℂ (E := H) ((f : (a : V) → H) x : H) ((g : (a : V) → H) x : H))

Tactic:
integral_sesq_fourier_fourier f g (innerSL ℂ)

Premises used: SchwartzMap.integral_sesq_fourier_fourier, innerSL, Complex
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : InnerProductSpace ℂ H
inst_7 : CompleteSpace H
f : 𝓢(V, H)
a :
  Eq (α := ℂ)
    ((Complex.ofRealLI : (a : ℝ) → ℂ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
          HPow.hPow (β := ℕ) (Norm.norm.{u_4} (E := H) ((𝓕 f : (a : V) → H) ξ : H)) 2) :
      ℂ)
    ((Complex.ofRealLI : (a : ℝ) → ℂ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
          HPow.hPow (β := ℕ) (Norm.norm.{u_4} (E := H) ((f : (a : V) → H) x : H)) 2) :
      ℂ)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
      HPow.hPow (β := ℕ) (Norm.norm.{u_4} (E := H) ((𝓕 f : (a : V) → H) ξ : H)) 2)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
      HPow.hPow (β := ℕ) (Norm.norm.{u_4} (E := H) ((f : (a : V) → H) x : H)) 2)

Tactic:
apply Complex.ofRealLI.injective

Premises used: LinearIsometry.injective, Complex.ofRealLI
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : InnerProductSpace ℂ H
inst_7 : CompleteSpace H
f : 𝓢(V, H)
⊢ Eq (α := ℂ)
    ((Complex.ofRealLI : (a : ℝ) → ℂ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (ξ : V) ↦
          HPow.hPow (β := ℕ) (Norm.norm.{u_4} (E := H) ((𝓕 f : (a : V) → H) ξ : H)) 2) :
      ℂ)
    ((Complex.ofRealLI : (a : ℝ) → ℂ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
          HPow.hPow (β := ℕ) (Norm.norm.{u_4} (E := H) ((f : (a : V) → H) x : H)) 2) :
      ℂ)

Tactic:
simpa [← LinearIsometry.integral_comp_comm, inner_self_eq_norm_sq_to_K] using
    integral_inner_fourier_fourier f f

Premises used: inner_self_eq_norm_sq_to_K, LinearIsometry.integral_comp_comm, SchwartzMap.integral_inner_fourier_fourier
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : InnerProductSpace ℂ H
inst_7 : CompleteSpace H
f g : 𝓢(V, H)
⊢ inner ℂ (E := ↥(Lp H 2 volume)) ((𝓕 f).toLp 2 volume) ((𝓕 g).toLp 2 volume) =
    inner ℂ (E := ↥(Lp H 2 volume)) (f.toLp 2 volume) (g.toLp 2 volume)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
H : Type u_4
inst_5 : NormedAddCommGroup H
inst_6 : InnerProductSpace ℂ H
inst_7 : CompleteSpace H
f : 𝓢(V, H)
simp_rw :
  √((RCLike.re : (a : ℂ) → ℝ) (inner ℂ (E := ↥(Lp H 2 volume)) ((𝓕 f).toLp 2 volume) ((𝓕 f).toLp 2 volume))) =
    √((RCLike.re : (a : ℂ) → ℝ) (inner ℂ (E := ↥(Lp H 2 volume)) (f.toLp 2 volume) (f.toLp 2 volume)))
⊢ Norm.norm (E := ↥(Lp H 2 volume)) ((𝓕 f).toLp 2 volume) = Norm.norm (E := ↥(Lp H 2 volume)) (f.toLp 2 volume)

Tactic:
simp_rw [norm_eq_sqrt_re_inner (𝕜 := ℂ), inner_fourier_toL2_eq]

Premises used: SchwartzMap.inner_fourier_toL2_eq, norm_eq_sqrt_re_inner
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
h :
  ∀ (f : 𝓢'(E, F)) (x : 𝓢(E, ℂ)),
    Eq.{u_2 + 1} (α := F)
      ((((besselPotential E F 0 : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)
      ((((ContinuousLinearMap.id ℂ 𝓢'(E, F) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (besselPotential E F 0) (ContinuousLinearMap.id ℂ 𝓢'(E, F))

Tactic:
ext f
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
f : 𝓢'(E, F)
x : 𝓢(E, ℂ)
⊢ Eq.{u_2 + 1} (α := F) ((((besselPotential E F 0 : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)
    ((((ContinuousLinearMap.id ℂ 𝓢'(E, F) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x : F)

Tactic:
simp [besselPotential]

Premises used: TemperedDistribution.besselPotential
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
rw :
  Eq (α := 𝓢'(E, F))
    ((fourierMultiplierCLM F
            (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
              (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ)) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        f :
      𝓢'(E, F))
    ((fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        f :
      𝓢'(E, F))
⊢ Eq (α := 𝓢'(E, F))
    ((fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        ((fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f) :
      𝓢'(E, F))
    ((fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        f :
      𝓢'(E, F))

Tactic:
rw [fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]

Premises used: TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
e_a :
  (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
      (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ)) =
    fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ)
⊢ Eq (α := 𝓢'(E, F))
    ((fourierMultiplierCLM F
            (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
              (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ)) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        f :
      𝓢'(E, F))
    ((fourierMultiplierCLM F fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ) :
          (a : 𝓢'(E, F)) → 𝓢'(E, F))
        f :
      𝓢'(E, F))

Tactic:
congr
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
e_a :
  ∀ (x : E),
    HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ))
        (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ)) x =
      (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ)
⊢ (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ)) fun (x : E) ↦
      (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ)) =
    fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ)

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
x : E
e_a :
  (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2) =
    (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)
⊢ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2)) : ℂ) * (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2)) : ℂ) =
    (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
x : E
rw rw₁ : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2)
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2) =
    (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2)

Tactic:
rw [← Real.rpow_add (by positivity)]

Premises used: Real.rpow_add
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
x : E
e_a : s / 2 + s' / 2 = (s + s') / 2
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)

Tactic:
congr
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ s / 2 + s' / 2 = (s + s') / 2

Tactic:
ring
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
x : E
_ :
  (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2) =
    (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2)
_₁ : (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2 + s' / 2) = (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s / 2) * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (s' / 2) =
    (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ ((s + s') / 2)

Tactic:
calc
    _ = (1 + ‖x‖ ^ 2) ^ (s / 2 + s' / 2) := by
      rw [← Real.rpow_add (by positivity)]
    _ = _ := by congr; ring

Premises used: Norm.norm, HDiv.hDiv, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
h :
  ∀ (f : 𝓢'(E, F)),
    Eq (α := 𝓢'(E, F)) ((besselPotential E F s' ∘SL besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
      ((besselPotential E F (s + s') : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (besselPotential E F s' ∘SL besselPotential E F s) (besselPotential E F (s + s'))

Tactic:
ext f : 1
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
⊢ Eq (α := 𝓢'(E, F)) ((besselPotential E F s' ∘SL besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    ((besselPotential E F (s + s') : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))

Tactic:
besselPotential_besselPotential_apply s s' f

Premises used: ContinuousLinearMap.comp, TemperedDistribution.besselPotential_besselPotential_apply
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
⊢ Eq (α := 𝓢'(E, F)) ((besselPotential E F s' ∘SL besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    ((besselPotential E F (s + s') : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))

Tactic:
exact besselPotential_besselPotential_apply s s' f

Premises used: TemperedDistribution.besselPotential_besselPotential_apply
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s : ℝ
f g : 𝓢'(E, F)
mp :
  (besselPotential E F (-s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = g →
    (besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g = f
mpr :
  (besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g = f →
    (besselPotential E F (-s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = g
⊢ (besselPotential E F (-s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = g ↔
    (besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g = f

Tactic:
constructor
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s : ℝ
f g : 𝓢'(E, F)
h : (besselPotential E F (-s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = g
⊢ (besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g = f

Tactic:
simp [← h]
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
s : ℝ
f g : 𝓢'(E, F)
h : (besselPotential E F s : (a : 𝓢'(E, F)) → 𝓢'(E, F)) g = f
⊢ (besselPotential E F (-s) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = g

Tactic:
simp [← h]
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
m : E
f : 𝓢'(E, F)
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑(inner ℝ x m) : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
m : E
f : 𝓢'(E, F)
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
m : E
f : 𝓢'(E, F)
rw :
  HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
      ((fourierMultiplierCLM F
              (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x m) : ℂ)) fun (x : E) ↦
                (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F)) =
    HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
      ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F))
⊢ (besselPotential E F (-1) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (∂_{m} f) =
    HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
      ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F))

Tactic:
rw [lineDeriv_eq_fourierMultiplierCLM, besselPotential,
    ContinuousLinearMap.map_smul_of_tower,
    fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]

Premises used: ContinuousLinearMap.map_smul_of_tower, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, TemperedDistribution.besselPotential
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
m : E
f : 𝓢'(E, F)
e_a :
  (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x m) : ℂ)) fun (x : E) ↦
      (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)) =
    fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)
⊢ HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
      ((fourierMultiplierCLM F
              (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x m) : ℂ)) fun (x : E) ↦
                (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F)) =
    HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
      ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F))

Tactic:
congr
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
m : E
f : 𝓢'(E, F)
e_a :
  ∀ (x : E),
    HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x m) : ℂ))
        (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)) x =
      (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)
⊢ (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x m) : ℂ)) fun (x : E) ↦
      (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)) =
    fun (x : E) ↦ (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
m : E
f : 𝓢'(E, F)
x : E
⊢ HMul.hMul (α := E → ℂ) (β := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x m) : ℂ))
      (fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)) x =
    (↑(inner ℝ x m * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-1 / 2)) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
f : 𝓢'(E, F)
funProp : HasCompactSupport (β := ℝ) fun (a : E) ↦ ‖a‖
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.Sobolev
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℂ F
f : 𝓢'(E, F)
⊢ Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦ (↑((1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-2 / 2)) : ℂ)

Tactic:
fun_prop