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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : 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₂
this :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : E) ↦ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖) volume
x : E
h :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦ ‖f₁ (a - x)‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦ ‖f₁ (a - x)‖) * ‖f₂ x‖ =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖

Tactic:
congr 1
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : 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₂
this :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : E) ↦ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖) volume
x : E
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x_1 : E) ↦ ‖f₁ (x_1 - x)‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦ ‖f₁ x‖)

Tactic:
integral_sub_right_eq_self _ x (μ := volume)

Premises used: MeasureTheory.integral_sub_right_eq_self
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : 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₂
this :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : E) ↦ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖) volume
x : E
h : ∀ (x_1 : E), ‖f₁ (x_1 - x)‖ = ‖f₁ (x_1 - x)‖
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦ ‖f₁ (a - x)‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖)

Tactic:
convert! integral_sub_right_eq_self _ x (μ := volume)

Premises used: MeasureTheory.integral_sub_right_eq_self
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : 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₂
this :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : E) ↦ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖) volume
x x_1 : E
⊢ ‖f₁ (x_1 - x)‖ = ‖f₁ (x_1 - x)‖

Tactic:
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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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
rw rw₁ : 𝓕 (f₁ ⋆[B, volume] f₂) ξ = 𝓕 (f₁ ⋆[B, volume] f₂) ξ
⊢ 𝓕 (f₁ ⋆[B, volume] f₂) ξ = 𝓕 (f₂ ⋆[B.flip, volume] f₁) ξ

Tactic:
rw [convolution_flip]

Premises used: MeasureTheory.convolution_flip
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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
⊢ 𝓕 (f₂ ⋆[B.flip, volume] f₁) ξ =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
          (((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y))

Tactic:
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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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 :
  Eq (α := E → F₃)
    (fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
          (((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y)))
    fun (x : E) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
          (((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))

Tactic:
congr
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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 :
  ∀ (x : E),
    HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
          (((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y)) =
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)
⊢ Eq (α := E → F₃)
    (fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
          (((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y)))
    fun (x : E) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)

Tactic:
ext x
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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₂
ξ x : E
e_f :
  HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
        (((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y)) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      HSMul.hSMul (α := ℂ) (β := F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)
⊢ HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
        (((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y)) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)

Tactic:
simp_rw [Circle.smul_def, integral_smul]

Premises used: MeasureTheory.integral_smul, Circle.smul_def
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))

Tactic:
integral_integral_swap ?_

Premises used: MeasureTheory.integral_integral_swap
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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
refine :
  @Integrable.{u_7, u_3} F₃ _ _ (E × E) Prod.instMeasurableSpace
    (Function.uncurry fun (x y : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (Measure.prod volume volume)
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))

Tactic:
refine integral_integral_swap ?_

Premises used: MeasureTheory.integral_integral_swap
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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
⊢ AEStronglyMeasurable.{u_3, u_7} (α := E × E) (β := F₃) (m₀ := Prod.instMeasurableSpace)
    (Function.uncurry fun (x y : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (Measure.prod volume volume)

Tactic:
measurability
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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
apply :
  ∀ᵐ (a : E × E) ∂Measure.prod volume volume,
    Norm.norm.{u_7} (E := F₃)
        (Function.uncurry
          (fun (x y : E) ↦
            HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
              ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
          a) ≤
      ‖‖B‖ * (‖f₁ (a.1 - a.2)‖ * ‖f₂ a.2‖)‖
⊢ @Integrable.{u_7, u_3} F₃ _ _ (E × E) Prod.instMeasurableSpace
    (Function.uncurry fun (x y : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
    (Measure.prod volume volume)

Tactic:
apply (integrable_prod_sub B hf₁ hf₂ hf₁' hf₂').mono (by measurability)

Premises used: Real.integrable_prod_sub, MeasureTheory.Integrable.mono
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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
h :
  ∀ (y x : E),
    Norm.norm.{u_7} (E := F₃)
        (Function.uncurry
          (fun (x y : E) ↦
            HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
              ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
          (y, x)) ≤
      ‖‖B‖ * (‖f₁ ((y, x).1 - (y, x).2)‖ * ‖f₂ (y, x).2‖)‖
⊢ ∀ᵐ (a : E × E) ∂Measure.prod volume volume,
    Norm.norm.{u_7} (E := F₃)
        (Function.uncurry
          (fun (x y : E) ↦
            HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
              ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
          a) ≤
      ‖‖B‖ * (‖f₁ (a.1 - a.2)‖ * ‖f₂ a.2‖)‖

Tactic:
filter_upwards with ⟨y, x⟩
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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 x : E
grw : ‖B‖ * ‖f₁ (y - x)‖ * ‖f₂ x‖ ≤ ‖B‖ * (‖f₁ (y - x)‖ * ‖f₂ x‖)
grw₁ grw₂ : ‖B‖ * (‖f₁ (y - x)‖ * ‖f₂ x‖) ≤ ‖B‖ * (‖f₁ (y - x)‖ * ‖f₂ x‖)
⊢ Norm.norm.{u_7} (E := F₃) ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (y - x)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ x) : F₃) ≤
    ‖B‖ * (‖f₁ (y - x)‖ * ‖f₂ x‖)

Tactic:
grw [B.le_opNorm₂ (f₁ (y - x)) (f₂ x), mul_assoc]

Premises used: mul_assoc, HSub.hSub, ContinuousLinearMap.le_opNorm₂
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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 x : E
⊢ Norm.norm.{u_7} (E := F₃) ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (y - x)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ x) : F₃) ≤
    ‖B‖ * (‖f₁ (y - x)‖ * ‖f₂ x‖)

Tactic:
have : ‖(B (f₁ (y - x))) (f₂ x)‖ ≤ ‖B‖ * (‖f₁ (y - x)‖ * ‖f₂ x‖) := by
      grw [B.le_opNorm₂ (f₁ (y - x)) (f₂ x), mul_assoc]
-- 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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedAddCommGroup F₂
inst_4 : NormedAddCommGroup F₃
inst_5 : InnerProductSpace ℝ E
inst_6 : FiniteDimensional ℝ E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
inst_9 : NormedSpace 𝕜 F₁
inst_10 : NormedSpace 𝕜 F₂
inst_11 : NormedSpace 𝕜 F₃
inst_12 : 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 x : E
this :
  Norm.norm.{u_7} (E := F₃) ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (y - x)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ x) : F₃) ≤
    ‖B‖ * (‖f₁ (y - x)‖ * ‖f₂ x‖)
⊢ Norm.norm.{u_7} (E := F₃)
      (Function.uncurry
        (fun (x y : E) ↦
          HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle)
            ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ (x - y)) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
        (y, x)) ≤
    ‖‖B‖ * (‖f₁ ((y, x).1 - (y, x).2)‖ * ‖f₂ (y, x).2‖)‖

Tactic:
simpa