awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ : E
e_f :
  ∀ (y : E),
    Eq.{u_7 + 1} (α := F₃)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
            (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
              ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)) :
        F₃)
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
              (B : (a : F₁) → F₂ →L[ℂ] F₃)
                (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) :
            (a : F₂) → F₃)
          (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle) (f₂ y)) :
        F₃)
⊢ Eq (α := E → F₃)
    (fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
          (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
            ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)))
    fun (y : E) ↦
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
          (B : (a : F₁) → F₂ →L[ℂ] F₃)
            (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) :
        (a : F₂) → F₃)
      (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle) (f₂ y))

Tactic:
ext y
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ y : E
e_f :
  HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ)) : ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦
        HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ a ξ)) : ℂ)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ a) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)) =
    HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ)) : ℂ)
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
              HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
                ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) :
            (a : F₂) → F₃)
          (f₂ y) :
        F₃)
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle)
          (HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
            ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)) :
      F₃)
    ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
            (B : (a : F₁) → F₂ →L[ℂ] F₃)
              (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) :
          (a : F₂) → F₃)
        (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle) (f₂ y)) :
      F₃)

Tactic:
simp_rw [Circle.smul_def, map_smul, MeasureTheory.integral_smul]

Premises used: MeasureTheory.integral_smul, Circle.smul_def, map_smul
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ y : E
e_f :
  Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦
        HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ a ξ)) : ℂ)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ a) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃) :
      F₃)
    ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
            HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
              ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) :
          (a : F₂) → F₃)
        (f₂ y) :
      F₃)
⊢ HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ)) : ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦
        HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ a ξ)) : ℂ)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ a) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)) =
    HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ)) : ℂ)
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
              HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
                ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) :
            (a : F₂) → F₃)
          (f₂ y) :
        F₃)

Tactic:
congr
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ y : E
e_f :
  Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦
      HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ a ξ)) : ℂ)
        ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ a) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      (HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
            ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) :
          (a : F₂) → F₃)
        (f₂ y))
rw :
  @Integrable (F₂ →L[ℂ] F₃) _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : E) ↦
      HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
        ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃))
    volume
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦
        HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ a ξ)) : ℂ)
          ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ a) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃) :
      F₃)
    ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
            HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
              ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) :
          (a : F₂) → F₃)
        (f₂ y) :
      F₃)

Tactic:
rw [integral_apply ?_ (f₂ y)]

Premises used: ContinuousLinearMap.integral_apply
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ y : E
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦
      HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ a ξ)) : ℂ)
        ((((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ a) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      (HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
            ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃) :
          (a : F₂) → F₃)
        (f₂ y))

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ y : E
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ ‖B‖ * ‖f₁ x‖) volume

Tactic:
have : MeasureTheory.Integrable (fun x ↦ ‖B‖ * ‖f₁ x‖) MeasureTheory.volume :=
      hf₁.norm.const_mul _
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ y : E
this : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ ‖B‖ * ‖f₁ x‖) volume
⊢ AEStronglyMeasurable (β := F₂ →L[ℂ] F₃) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦
      HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
        ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃))
    volume

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ y : E
this : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ ‖B‖ * ‖f₁ x‖) volume
h :
  ∀ (x : E),
    ‖HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
          ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃)‖ ≤
      ‖‖B‖ * ‖f₁ x‖‖
⊢ ∀ᵐ (a : E),
    ‖HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ a ξ)) : ℂ)
          ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ a) : F₂ →L[ℂ] F₃)‖ ≤
      ‖‖B‖ * ‖f₁ a‖‖

Tactic:
filter_upwards with x
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ y : E
this : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ ‖B‖ * ‖f₁ x‖) volume
x : E
h :
  ‖HSMul.hSMul (α := Circle) (β := F₂ →L[ℂ] F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃)‖ ≤
    |‖B‖| * ‖f₁ x‖
⊢ ‖HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
        ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃)‖ ≤
    ‖‖B‖ * ‖f₁ x‖‖

Tactic:
simpa [← Circle.smul_def] using le_opNorm B (f₁ x)

Premises used: ContinuousLinearMap.le_opNorm, Circle.smul_def
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ : E
⊢ @Integrable.{u_6, u_3} F₂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : E) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle) (f₂ y)) volume

Tactic:
simpa using hf₂
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedAddCommGroup F₂
inst_3 : NormedAddCommGroup F₃
inst_4 : InnerProductSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : NormedSpace ℂ F₃
inst_9 : CompleteSpace F₁
inst_10 : CompleteSpace F₂
inst_11 : CompleteSpace F₃
inst_12 : NormedSpace ℂ F₁
inst_13 : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ : E
⊢ @Integrable.{u_5, u_3} F₁ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : E) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) volume

Tactic:
simpa using hf₁
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
E : Type u_3
F₁ : Type u_5
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 : CompleteSpace F₁
inst_7 : NormedSpace ℂ F₁
f₁ : E → ℂ
f₂ : E → F₁
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ : E
⊢ 𝓕 (f₁ ⋆[lsmul ℂ ℂ, volume] f₂) ξ = 𝓕 f₁ ξ • 𝓕 f₂ ξ

Tactic:
fourier_bilin_convolution_eq (lsmul ℂ ℂ) hf₁ hf₂ hf₁' hf₂' ξ

Premises used: Real.fourier_bilin_convolution_eq, Complex, ContinuousLinearMap.lsmul
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
R : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedRing R
inst_6 : NormedSpace ℂ R
inst_7 : IsScalarTower ℂ R R
inst_8 : SMulCommClass ℂ R R
inst_9 : CompleteSpace R
f₁ f₂ : E → R
hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₁ volume
hf₂ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f₂ volume
hf₁' : Continuous f₁
hf₂' : Continuous f₂
ξ : E
⊢ 𝓕 (E := E → R) (convolution (𝕜 := ℂ) f₁ f₂ (mul ℂ R) volume) ξ = 𝓕 f₁ ξ * 𝓕 f₂ ξ

Tactic:
fourier_bilin_convolution_eq (mul ℂ R) hf₁ hf₂ hf₁' hf₂' ξ

Premises used: Real.fourier_bilin_convolution_eq, ContinuousLinearMap.mul, Complex
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
𝕜 : Type u_1
R : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace ℂ F₁
inst_8 : NormedSpace 𝕜 F₁
inst_9 : SMulCommClass ℂ 𝕜 F₁
inst_10 : NormedAddCommGroup F₂
inst_11 : NormedSpace ℂ F₂
inst_12 : NormedSpace 𝕜 F₂
inst_13 : SMulCommClass ℂ 𝕜 F₂
inst_14 : NormedAddCommGroup F₃
inst_15 : NormedSpace ℂ F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : SMulCommClass ℂ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
⊢ ∀ (x y : 𝓢(E, F₁)),
    ContinuousLinearMap.comp (M₂ := 𝓢(E, F₃)) (fourierInvCLM 𝕜 𝓢(E, F₃))
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          (((pairing B : 𝓢(E, F₁) →ₗ[𝕜] 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃))
            (𝓕 (x + y)))
          (fourierCLM 𝕜 𝓢(E, F₂))) =
      HAdd.hAdd (α := 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃))
        (ContinuousLinearMap.comp (M₂ := 𝓢(E, F₃)) (fourierInvCLM 𝕜 𝓢(E, F₃))
          (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            (((pairing B : 𝓢(E, F₁) →ₗ[𝕜] 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) (𝓕 x))
            (fourierCLM 𝕜 𝓢(E, F₂))))
        (ContinuousLinearMap.comp (M₂ := 𝓢(E, F₃)) (fourierInvCLM 𝕜 𝓢(E, F₃))
          (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            (((pairing B : 𝓢(E, F₁) →ₗ[𝕜] 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) (𝓕 y))
            (fourierCLM 𝕜 𝓢(E, F₂))))

Tactic:
simp [FourierTransform.fourier_add]

Premises used: FourierAdd.fourier_add
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
𝕜 : Type u_1
R : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace ℂ F₁
inst_8 : NormedSpace 𝕜 F₁
inst_9 : SMulCommClass ℂ 𝕜 F₁
inst_10 : NormedAddCommGroup F₂
inst_11 : NormedSpace ℂ F₂
inst_12 : NormedSpace 𝕜 F₂
inst_13 : SMulCommClass ℂ 𝕜 F₂
inst_14 : NormedAddCommGroup F₃
inst_15 : NormedSpace ℂ F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : SMulCommClass ℂ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
⊢ ∀ (m : 𝕜) (x : 𝓢(E, F₁)),
    ContinuousLinearMap.comp (M₂ := 𝓢(E, F₃)) (fourierInvCLM 𝕜 𝓢(E, F₃))
        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
          (((pairing B : 𝓢(E, F₁) →ₗ[𝕜] 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃))
            (𝓕 (m • x)))
          (fourierCLM 𝕜 𝓢(E, F₂))) =
      HSMul.hSMul (α := 𝕜) (β := 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜)
        (ContinuousLinearMap.comp (M₂ := 𝓢(E, F₃)) (fourierInvCLM 𝕜 𝓢(E, F₃))
          (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
            (((pairing B : 𝓢(E, F₁) →ₗ[𝕜] 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) (𝓕 x))
            (fourierCLM 𝕜 𝓢(E, F₂))))

Tactic:
simp [FourierTransform.fourier_smul]

Premises used: FourierSMul.fourier_smul
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace ℂ F₁
inst_8 : NormedSpace 𝕜 F₁
inst_9 : SMulCommClass ℂ 𝕜 F₁
inst_10 : NormedAddCommGroup F₂
inst_11 : NormedSpace ℂ F₂
inst_12 : NormedSpace 𝕜 F₂
inst_13 : SMulCommClass ℂ 𝕜 F₂
inst_14 : NormedAddCommGroup F₃
inst_15 : NormedSpace ℂ F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : SMulCommClass ℂ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
⊢ Eq (α := 𝓢(E, F₃))
    (((((convolution
                    (ContinuousLinearMap.flip.{u_1, u_1, u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := F₁)
                      (F := F₂) (G := F₃) (σ₂₃ := RingHom.id 𝕜) (σ₁₃ := RingHom.id 𝕜) B) :
                  𝓢(E, F₂) →ₗ[𝕜] 𝓢(E, F₁) →L[𝕜] 𝓢(E, F₃)) :
                (a : 𝓢(E, F₂)) → 𝓢(E, F₁) →L[𝕜] 𝓢(E, F₃))
              g :
            𝓢(E, F₁) →L[𝕜] 𝓢(E, F₃)) :
          (a : 𝓢(E, F₁)) → 𝓢(E, F₃))
        f :
      𝓢(E, F₃))
    (((((convolution B : 𝓢(E, F₁) →ₗ[𝕜] 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) f :
            𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) :
          (a : 𝓢(E, F₂)) → 𝓢(E, F₃))
        g :
      𝓢(E, F₃))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Fourier.Convolution
Goal:
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace ℂ F₁
inst_8 : NormedSpace 𝕜 F₁
inst_9 : SMulCommClass ℂ 𝕜 F₁
inst_10 : NormedAddCommGroup F₂
inst_11 : NormedSpace ℂ F₂
inst_12 : NormedSpace 𝕜 F₂
inst_13 : SMulCommClass ℂ 𝕜 F₂
inst_14 : NormedAddCommGroup F₃
inst_15 : NormedSpace ℂ F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : SMulCommClass ℂ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : 𝓢(E, F₂)
⊢ Continuous (Y := 𝓢(E, F₃)) fun (x : 𝓢(E, F₁)) ↦
    ((((convolution B : 𝓢(E, F₁) →ₗ[𝕜] 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) : (a : 𝓢(E, F₁)) → 𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) x :
          𝓢(E, F₂) →L[𝕜] 𝓢(E, F₃)) :
        (a : 𝓢(E, F₂)) → 𝓢(E, F₃))
      g

Tactic:
(convolution B.flip g).continuous

Premises used: ContinuousLinearMap.continuous, ContinuousLinearMap.flip, SchwartzMap.convolution, DFunLike.coe