awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
hvv' : v ≠ v'
w : W
hw : Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
h :
  (∃ a ∈ charPoly he hL,
      Eq (α := V → ℂ) (⇑((toContinuousMapStarₐ ℂ : (a : V →ᵇ ℂ) → C(V, ℂ)) a : C(V, ℂ)) : (a : V) → ℂ)
        (⇑(char he hL w) : (a : V) → ℂ)) ∧
    ¬Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
⊢ Membership.mem (γ := Set (V → ℂ))
      ((fun (f : C(V, ℂ)) ↦ (⇑f : (a : V) → ℂ)) ''
        (↑(StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL))) : Set C(V, ℂ)))
      (⇑(char he hL w) : (a : V) → ℂ) ∧
    Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)

Tactic:
simp only [StarSubalgebra.coe_toSubalgebra, StarSubalgebra.coe_map, Set.mem_image,
    SetLike.mem_coe, exists_exists_and_eq_and, ne_eq]

Premises used: StarSubalgebra.coe_map, Set.mem_image, ne_eq, exists_exists_and_eq_and, SetLike.mem_coe, StarSubalgebra.coe_toSubalgebra
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
hvv' : v ≠ v'
w : W
hw : Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
⊢ (∃ a ∈ charPoly he hL,
      Eq (α := V → ℂ) (⇑((toContinuousMapStarₐ ℂ : (a : V →ᵇ ℂ) → C(V, ℂ)) a : C(V, ℂ)) : (a : V) → ℂ)
        (⇑(char he hL w) : (a : V) → ℂ)) ∧
    ¬Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)

Tactic:
⟨⟨char he hL w, char_mem_charPoly w, rfl⟩, hw⟩

Premises used: BoundedContinuousFunction.char, And.intro, Exists.intro, rfl, BoundedContinuousFunction.char_mem_charPoly
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
hvv' : v ≠ v'
w : W
hw : Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
⊢ (∃ a ∈ charPoly he hL,
      Eq (α := V → ℂ) (⇑((toContinuousMapStarₐ ℂ : (a : V →ᵇ ℂ) → C(V, ℂ)) a : C(V, ℂ)) : (a : V) → ℂ)
        (⇑(char he hL w) : (a : V) → ℂ)) ∧
    ¬Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)

Tactic:
exact ⟨⟨char he hL w, char_mem_charPoly w, rfl⟩, hw⟩
-- 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₂
h :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (x : E × E) ↦ ‖f₁ (x.1 - x.2)‖ * ‖f₂ x.2‖)
    (Measure.prod volume volume)
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (p : E × E) ↦ ‖B‖ * (‖f₁ (p.1 - p.2)‖ * ‖f₂ p.2‖))
    (Measure.prod volume volume)

Tactic:
apply Integrable.const_mul

Premises used: MeasureTheory.Integrable.const_mul
-- 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₂
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Prod.instMeasurableSpace) (fun (x : E × E) ↦ ‖f₁ (x.1 - x.2)‖ * ‖f₂ x.2‖)
    (Measure.prod volume volume)

Tactic:
fun_prop
-- 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₂
h :
  (∀ᵐ (y : E),
      @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ ‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖)
        volume) ∧
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
      (fun (y : E) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
          ‖‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖‖)
      volume
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (x : E × E) ↦ ‖f₁ (x.1 - x.2)‖ * ‖f₂ x.2‖)
    (Measure.prod volume volume)

Tactic:
rw [integrable_prod_iff' (by fun_prop)]

Premises used: MeasureTheory.integrable_prod_iff'
-- 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₂
h :
  ∀ᵐ (y : E),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ ‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖) volume
h₁ :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        ‖‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖‖)
    volume
⊢ (∀ᵐ (y : E),
      @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ ‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖)
        volume) ∧
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
      (fun (y : E) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
          ‖‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖‖)
      volume

Tactic:
constructor
-- 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₂
h : ∀ (x : E), @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : E) ↦ ‖f₁ (x_1 - x)‖ * ‖f₂ x‖) volume
⊢ ∀ᵐ (y : E),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ ‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖) volume

Tactic:
filter_upwards with 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₃
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
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : E) ↦ ‖f₁ (x_1 - x)‖ * ‖f₂ x‖) volume

Tactic:
(hf₁.comp_sub_right x).norm.mul_const _

Premises used: MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.norm, MeasureTheory.Integrable.comp_sub_right
-- 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₂
x : E
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : E) ↦ ‖f₁ (x_1 - x)‖ * ‖f₂ x‖) volume

Tactic:
exact (hf₁.comp_sub_right x).norm.mul_const _

Premises used: MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.norm, MeasureTheory.Integrable.comp_sub_right
-- 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₂
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : E) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) volume

Tactic:
fun_prop
-- 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₂
apply :
  ∀ᵐ (x : E),
    Norm.norm (E := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) ≤
      Norm.norm (E := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖)
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : E) ↦ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖) volume

Tactic:
apply hf₂.norm.bdd_mul (by fun_prop) (c := ‖(∫ y, ‖f₁ y‖)‖)

Premises used: MeasureTheory.Integrable.bdd_mul, MeasureTheory.Integrable.norm
-- 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₂
h :
  ∀ (a : E),
    Norm.norm (E := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) ≤
      Norm.norm (E := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖)
⊢ ∀ᵐ (x : E),
    Norm.norm (E := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) ≤
      Norm.norm (E := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖)

Tactic:
filter_upwards with
-- 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₂
a : E
⊢ Norm.norm (E := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) ≤
    Norm.norm (E := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖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₃
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₂
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : E) ↦ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖) volume

Tactic:
have : Integrable (fun x ↦ ((∫ y, ‖f₁ y‖) * ‖f₂ x‖)) := by
    apply hf₂.norm.bdd_mul (by fun_prop) (c := ‖(∫ y, ‖f₁ y‖)‖)
    filter_upwards with; 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₃
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
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : E) ↦ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖) volume

Tactic:
this
-- 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
h :
  Eq.{u_3 + 1} (α := E → ℝ)
    (fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        ‖‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖‖)
    fun (x : E) ↦ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        ‖‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖‖)
    volume

Tactic:
convert! this using 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
h :
  ∀ (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‖
⊢ Eq.{u_3 + 1} (α := E → ℝ)
    (fun (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        ‖‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖‖)
    fun (x : E) ↦ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖

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₃
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 :
  (@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‖
⊢ (@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‖

Tactic:
simp_rw [norm_mul, norm_norm]

Premises used: norm_mul, norm_norm
-- 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : E) ↦ ‖f₁ (a - x)‖) * ‖f₂ x‖ =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : E) ↦ ‖f₁ y‖) * ‖f₂ x‖
⊢ (@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:
rw [integral_mul_const]

Premises used: MeasureTheory.integral_mul_const