awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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₃) :
      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₃)
have 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))
Tactic: rw [integral_apply ?_ (f₂ y)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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))
⊢ 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₃)
have 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
Tactic: rw [integral_apply ?_ (f₂ y)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (hypothesis)
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 (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
have this : @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 _
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ ∀ᵐ (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‖‖
have 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‖‖
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ ‖HSMul.hSMul (α := ℂ) (β := F₂ →L[ℂ] F₃) (↑((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ)) : ℂ)
        ((B : (a : F₁) → F₂ →L[ℂ] F₃) (f₁ x) : F₂ →L[ℂ] F₃)‖ ≤
    ‖‖B‖ * ‖f₁ x‖‖
have 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‖
Tactic: simpa [← Circle.smul_def] using le_opNorm B (f₁ x)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ Eq.{u_7 + 1} (α := F₃)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume 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)) :
      F₃)
    (((B : (a : F₁) → F₂ →L[ℂ] F₃)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
              HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) :
          (a : F₂) → F₃)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ y ξ) : Circle) (f₂ y)) :
      F₃)
have rw : Eq.{u_7 + 1} (α := F₃)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume 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)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
    ((B : (a : F₁) → F₂ →L[ℂ] F₃)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₁ x)) :
        (a : F₂) → F₃)
      (HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-inner ℝ x ξ) : Circle) (f₂ x)))
Tactic: rw [← integral_comp_comm _ (by simpa using hf₂), ← integral_comp_comm _ (by simpa using hf₁)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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 := (y : E) → F₃) (fun (y : E) ↦ 𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂)) y) x
have 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
Tactic: rw [fourierInv_coe]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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 := (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
have 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)
Tactic: apply MeasureTheory.integral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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)
have 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)
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 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)
have 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)
Tactic: rw [fourier_convolution_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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 := (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
have h : Continuous.{u_3, u_7} (X := E) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))
Tactic: rw [Continuous.fourierInv_fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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₂))
⊢ 𝓕⁻ (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
have hf : @Integrable.{u_7, u_3} _ _ _ E MeasureSpace.toMeasurableSpace ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))
  volume
Tactic: rw [Continuous.fourierInv_fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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
⊢ 𝓕⁻ (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
have h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace
  (𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))) volume
Tactic: rw [Continuous.fourierInv_fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (goal)
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₂))
have h : BddAbove (α := ℝ) (Set.range fun (x : E) ↦ norm.{u_6} (E := F₂) ((g : (a : E) → F₂) x : F₂))
Tactic: refine BddAbove.continuous_convolution_right_of_integrable B ?_ f.integrable g.continuous
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Convolution (hypothesis)
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 _ _ _ _ MeasureSpace.toMeasurableSpace
    (𝓕 (E := E → F₃) ((⇑f : (a : E) → F₁) ⋆[B, volume] (⇑g : (a : E) → F₂))) volume
have 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
Tactic: have : Integrable (fun ξ ↦ B (𝓕 f ξ) (𝓕 g ξ)) volume := (pairing B (𝓕 f) (𝓕 g)).integrable