awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃
inst_18 : CompleteSpace F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
⊢ 𝓕 (E := 𝓢(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₃)) =
    ((((pairing 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)

Tactic:
simp [convolution]

Premises used: SchwartzMap.convolution
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ (𝓕 (E := 𝓢(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₃)) :
        (a : E) → F₃)
      x =
    𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x

Tactic:
simp [fourier_convolution, fourier_coe,
    Real.fourier_bilin_convolution_eq B f.integrable g.integrable f.continuous g.continuous]

Premises used: SchwartzMap.continuous, Real.fourier_bilin_convolution_eq, SchwartzMap.fourier_coe, SchwartzMap.integrable, SchwartzMap.fourier_convolution
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ Eq.{u_7 + 1} (α := 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₃)) :
          (a : E) → F₃)
        x :
      F₃)
    ((𝓕⁻
            (𝓕 (E := 𝓢(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₃))) :
          (a : E) → F₃)
        x :
      F₃)

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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
rw :
  𝓕⁻ (E := (a : E) → F₃)
      (⇑(𝓕 (E := 𝓢(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₃))) :
        (a : E) → F₃)
      x =
    𝓕⁻ (E := (y : E) → F₃) (fun (y : E) ↦ 𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) y) x
⊢ (𝓕⁻
          (𝓕 (E := 𝓢(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₃))) :
        (a : E) → F₃)
      x =
    𝓕⁻ (E := (y : E) → F₃) (fun (y : E) ↦ 𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) y) x

Tactic:
rw [fourierInv_coe]

Premises used: SchwartzMap.fourierInv_coe
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
h :
  Filter.EventuallyEq.{u_3, u_7} (β := F₃) (ae (F := Measure E) volume)
    (fun (a : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃)
        ((𝐞 : (a : ℝ) → Circle)
            (-((((-innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x) :
          Circle)
        ((𝓕 (E := 𝓢(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₃)) :
              (a : E) → F₃)
            a :
          F₃))
    fun (a : E) ↦
    HSMul.hSMul (α := Circle) (β := F₃)
      ((𝐞 : (a : ℝ) → Circle)
          (-((((-innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x) :
        Circle)
      ((fun (y : E) ↦ 𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) y) a)
⊢ 𝓕⁻ (E := (a : E) → F₃)
      (⇑(𝓕 (E := 𝓢(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₃))) :
        (a : E) → F₃)
      x =
    𝓕⁻ (E := (y : E) → F₃) (fun (y : E) ↦ 𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) y) x

Tactic:
apply MeasureTheory.integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
h :
  ∀ (x_1 : E),
    HSMul.hSMul (α := Circle) (β := F₃)
        ((𝐞 : (a : ℝ) → Circle)
            (-((((-innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x_1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x) :
          Circle)
        ((𝓕 (E := 𝓢(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₃)) :
              (a : E) → F₃)
            x_1 :
          F₃) =
      HSMul.hSMul (α := Circle)
        ((𝐞 : (a : ℝ) → Circle)
            (-((((-innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x_1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x) :
          Circle)
        (𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x_1)
⊢ Filter.EventuallyEq.{u_3, u_7} (β := F₃) (ae (F := Measure E) volume)
    (fun (a : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃)
        ((𝐞 : (a : ℝ) → Circle)
            (-((((-innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x) :
          Circle)
        ((𝓕 (E := 𝓢(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₃)) :
              (a : E) → F₃)
            a :
          F₃))
    fun (a : E) ↦
    HSMul.hSMul (α := Circle) (β := F₃)
      ((𝐞 : (a : ℝ) → Circle)
          (-((((-innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x) :
        Circle)
      ((fun (y : E) ↦ 𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) y) 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x_1 x : E
h h₁ :
  HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle)
          (-((((-innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x_1) :
        Circle)
      (𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x) =
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle)
          (-((((-innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x_1) :
        Circle)
      (𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x)
⊢ HSMul.hSMul (α := Circle) (β := F₃)
      ((𝐞 : (a : ℝ) → Circle)
          (-((((-innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x_1) :
        Circle)
      ((𝓕 (E := 𝓢(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₃)) :
            (a : E) → F₃)
          x :
        F₃) =
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle)
          (-((((-innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x_1) :
        Circle)
      (𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x)

Tactic:
rw [fourier_convolution_apply]

Premises used: SchwartzMap.fourier_convolution_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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
h : Continuous.{u_3, u_7} (X := E) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))
hf :
  @Integrable.{u_7, u_3} _ _ _ E MeasureSpace.toMeasurableSpace ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))
    volume
h'f :
  @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace
    (𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))) volume
⊢ 𝓕⁻ (E := (y : E) → F₃) (fun (y : E) ↦ 𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) y) x =
    ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x

Tactic:
rw [Continuous.fourierInv_fourier_eq]

Premises used: Continuous.fourierInv_fourier_eq
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ Continuous.{u_3, u_7} (X := E) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))

Tactic:
BddAbove.continuous_convolution_right_of_integrable B ?_ f.integrable g.continuous

Premises used: BddAbove.continuous_convolution_right_of_integrable, SchwartzMap.continuous, SchwartzMap.integrable
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
h : BddAbove (α := ℝ) (Set.range fun (x : E) ↦ norm.{u_6} (E := F₂) ((g : (a : E) → F₂) x : F₂))
⊢ Continuous.{u_3, u_7} (X := E) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))

Tactic:
refine BddAbove.continuous_convolution_right_of_integrable B ?_ f.integrable g.continuous

Premises used: BddAbove.continuous_convolution_right_of_integrable, SchwartzMap.continuous, SchwartzMap.integrable
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ BddAbove (α := ℝ) (Set.range fun (x : E) ↦ norm.{u_6} (E := F₂) ((g : (a : E) → F₂) x : F₂))

Tactic:
⟨SchwartzMap.seminorm ℝ 0 0 g, fun x ⟨y, hy⟩ ↦ hy ▸ norm_le_seminorm ℝ g y⟩

Premises used: _private.0.SchwartzMap.convolution_apply.match_1, SchwartzMap.norm_le_seminorm, Real, Eq.rec, LE.le, BddAbove, SchwartzMap.seminorm, Set.Nonempty, Exists.intro, OfNat.ofNat, DFunLike.coe
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ BddAbove (α := ℝ) (Set.range fun (x : E) ↦ norm.{u_6} (E := F₂) ((g : (a : E) → F₂) x : F₂))

Tactic:
exact ⟨SchwartzMap.seminorm ℝ 0 0 g, fun x ⟨y, hy⟩ ↦ hy ▸ norm_le_seminorm ℝ g 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ @Integrable.{u_7, u_3} _ _ _ E MeasureSpace.toMeasurableSpace ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))
    volume

Tactic:
f.integrable.integrable_convolution B g.integrable

Premises used: MeasureTheory.Integrable.integrable_convolution, SchwartzMap.integrable
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ @Integrable.{u_7, u_3} _ _ _ E MeasureSpace.toMeasurableSpace ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))
    volume

Tactic:
exact f.integrable.integrable_convolution B g.integrable

Premises used: MeasureTheory.Integrable.integrable_convolution, SchwartzMap.integrable
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ @Integrable.{u_7, u_3} F₃ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (ξ : E) ↦
      (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) ξ) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) ξ : F₂))
    volume

Tactic:
have : Integrable (fun ξ ↦ B (𝓕 f ξ) (𝓕 g ξ)) volume := (pairing B (𝓕 f) (𝓕 g)).integrable
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
this :
  @Integrable.{u_7, u_3} F₃ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (ξ : E) ↦
      (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) ξ) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) ξ : F₂))
    volume
⊢ @Integrable.{u_7, u_3} F₃ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (ξ : E) ↦
      (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) ξ) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) ξ : F₂))
    volume

Tactic:
this
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
this :
  @Integrable.{u_7, u_3} F₃ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (ξ : E) ↦
      (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) ξ) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) ξ : F₂))
    volume
h :
  ∀ (x : E),
    𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x =
      (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) x : F₂)
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace
    (𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))) volume

Tactic:
convert! this
-- 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 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F₁
inst_6 : NormedSpace ℂ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace ℂ F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace ℂ F₃
inst_11 : CompleteSpace F₃
inst_12 : CompleteSpace F₁
inst_13 : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
this :
  @Integrable.{u_7, u_3} F₃ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (ξ : E) ↦
      (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) ξ) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) ξ : F₂))
    volume
x_1 : E
h :
  Eq.{u_7 + 1} (α := F₃)
    ((𝓕 (E := 𝓢(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₃)) :
          (a : E) → F₃)
        x_1 :
      F₃)
    ((((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) x_1 : F₂) :
      F₃)
h₁ :
  Eq.{u_7 + 1} (α := F₃)
    (((((((pairing 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₃)) :
          (a : E) → F₃)
        x_1 :
      F₃)
    ((((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) x_1 : F₂) :
      F₃)
h₂ h₃ :
  Eq.{u_7 + 1} (α := F₃)
    ((((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) x_1 : F₂) :
      F₃)
    ((((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
        ((𝓕 g : (a : E) → F₂) x_1 : F₂) :
      F₃)
⊢ 𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) x_1 =
    (((B : (a : F₁) → F₂ →L[ℂ] F₃) ((𝓕 f : (a : E) → F₁) x_1) : F₂ →L[ℂ] F₃) : (a : F₂) → F₃)
      ((𝓕 g : (a : E) → F₂) x_1 : F₂)

Tactic:
rw [← fourier_convolution_apply B f g, fourier_convolution, pairing_apply_apply]

Premises used: SchwartzMap.pairing_apply_apply, SchwartzMap.fourier_convolution_apply, SchwartzMap.fourier_convolution
-- Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
Goal:
G : Type u_1
R : Type u_3
inst : AddGroup G
inst_1 : Fintype G
inst_2 : Semifield R
inst_3 : IsDomain R
inst_4 : CharZero R
ψ : AddChar G R
⊢ Eq.{u_3 + 1} (α := R) (𝔼 a : G, (ψ : (a : G) → R) a) (if ψ = 0 then 1 else 0)

Tactic:
simp [Fintype.expect_eq_sum_div_card, sum_eq_ite, ite_div]

Premises used: AddChar.sum_eq_ite, ite_div, Fintype.expect_eq_sum_div_card