awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x_1 : E) ↦
      ‖‖f₁ ((x_1, x).1 - (x_1, x).2)‖ * ‖f₂ (x_1, x).2‖‖) =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖
have h : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x_1 : E) ↦ ‖f₁ (x_1 - x)‖ * ‖f₂ x‖) =
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖
Tactic: simp_rw [norm_mul, norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x_1 : E) ↦ ‖f₁ (x_1 - x)‖ * ‖f₂ x‖) =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖
have h : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦ ‖f₁ (a - x)‖) * ‖f₂ x‖ =
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖
Tactic: rw [integral_mul_const]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦ ‖f₁ (a - x)‖) * ‖f₂ x‖ =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖
have h : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦ ‖f₁ (a - x)‖)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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 (a : E) ↦ ‖f₁ (a - x)‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖)
have h : ∀ (x_1 : E), ‖f₁ (x_1 - x)‖ = ‖f₁ (x_1 - x)‖
Tactic: convert! integral_sub_right_eq_self _ x (μ := volume)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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, volume] f₂) ξ = 𝓕 (f₂ ⋆[B.flip, volume] f₁) ξ
have rw : 𝓕 (f₁ ⋆[B, volume] f₂) ξ = 𝓕 (f₁ ⋆[B, volume] f₂) ξ
Tactic: rw [convolution_flip]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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) ↦
      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₃))
have 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₃)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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 (α := 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₃)
have 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₃)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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₃)
have 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₃)
Tactic: simp_rw [Circle.smul_def, integral_smul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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₃))
have 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)
Tactic: refine integral_integral_swap ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ @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)
have 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‖)‖
Tactic: apply (integrable_prod_sub B hf₁ hf₂ hf₁' hf₂').mono (by measurability)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ ∀ᵐ (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‖)‖
have 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‖)‖
Tactic: filter_upwards with ⟨y, x⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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‖)
have grw : ‖B‖ * ‖f₁ (y - x)‖ * ‖f₂ x‖ ≤ ‖B‖ * (‖f₁ (y - x)‖ * ‖f₂ x‖)
Tactic: grw [B.le_opNorm₂ (f₁ (y - x)) (f₂ x), mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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‖)
⊢ 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‖)
have grw₁ : ‖B‖ * (‖f₁ (y - x)‖ * ‖f₂ x‖) ≤ ‖B‖ * (‖f₁ (y - x)‖ * ‖f₂ x‖)
Tactic: grw [B.le_opNorm₂ (f₁ (y - x)) (f₂ x), mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (hypothesis)
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₃)
      (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‖)‖
have 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‖)
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]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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 (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₃))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
          ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
have e_f : Eq (α := E → F₃)
  (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₃))
  fun (y : E) ↦
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
    HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
      ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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 (α := E → F₃)
    (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₃))
    fun (y : E) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃)
have e_f : ∀ (y : E),
  Eq.{u_7 + 1} (α := F₃)
    (@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₃))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
      HSMul.hSMul (α := Circle) (β := F₃) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ (y + x) ξ) : Circle)
        ((((B : (a : F₁) → F₂ →L[𝕜] F₃) (f₁ x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (f₂ y) : F₃))
Tactic: ext y