awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
v : V
⊢ Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ)
    (∑ a ∈ Finsupp.support (M := ℂ) (AddMonoidAlgebra.single w 1),
        HMul.hMul (α := ℂ) (β := ℂ) ((AddMonoidAlgebra.single w 1 : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)
have h : Eq (α := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
  (∑ x ∈ Finsupp.support (M := ℂ) (Finsupp.single w 1),
    HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) x : ℂ)
      ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) x)) : ℂ) : ℂ))
Tactic: simp only [char_apply, AddMonoidAlgebra.single]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
v : V
⊢ Eq (α := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
    (∑ x ∈ Finsupp.support (M := ℂ) (Finsupp.single w 1),
      HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) x : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) x)) : ℂ) : ℂ))
have h : (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) w : ℂ)
    ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) : ℂ)
Tactic: rw [Finset.sum_eq_single w]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
v : V
h :
  (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) w : ℂ)
      ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) : ℂ)
⊢ Eq (α := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
    (∑ x ∈ Finsupp.support (M := ℂ) (Finsupp.single w 1),
      HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) x : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) x)) : ℂ) : ℂ))
have h₁ : ∀ b ∈ Finsupp.support (M := ℂ) (Finsupp.single w 1),
  b ≠ w →
    HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) b : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) b)) : ℂ) : ℂ) =
      0
Tactic: rw [Finset.sum_eq_single w]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
v : V
h :
  (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) w : ℂ)
      ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) : ℂ)
h₁ :
  ∀ b ∈ Finsupp.support (M := ℂ) (Finsupp.single w 1),
    b ≠ w →
      HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) b : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) b)) : ℂ) : ℂ) =
        0
⊢ Eq (α := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
    (∑ x ∈ Finsupp.support (M := ℂ) (Finsupp.single w 1),
      HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) x : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) x)) : ℂ) : ℂ))
have h₂ : w ∉ Finsupp.support (M := ℂ) (Finsupp.single w 1) →
  HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) w : ℂ)
      ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) : ℂ) =
    0
Tactic: rw [Finset.sum_eq_single w]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
have contrapose! : ∀ (hvv' : ∀ (w : W), Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)), v = v'
Tactic: contrapose! hvv'
Cleared hypotheses: hvv'
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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'
⊢ ∃ (f : V → ℂ),
    Membership.mem (γ := Set (V → ℂ))
        ((fun (f : C(V, ℂ)) ↦ (⇑f : (a : V) → ℂ)) ''
          (↑(StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL))) : Set C(V, ℂ)))
        f ∧
      f v ≠ f v'
have obtain : ∀ (w : W) (hw : Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)),
  ∃ (f : V → ℂ),
    Membership.mem (γ := Set (V → ℂ))
        ((fun (f : C(V, ℂ)) ↦ (⇑f : (a : V) → ℂ)) ''
          (↑(StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL))) : Set C(V, ℂ)))
        f ∧
      f v ≠ f v'
Tactic: obtain ⟨w, hw⟩ : ∃ w, char he hL w v ≠ char he hL w v' := by
    contrapose! hvv'
    exact ext_of_char_eq he he' hL hL' hvv'
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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' : ℂ)
⊢ ∃ (f : V → ℂ),
    Membership.mem (γ := Set (V → ℂ))
        ((fun (f : C(V, ℂ)) ↦ (⇑f : (a : V) → ℂ)) ''
          (↑(StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL))) : Set C(V, ℂ)))
        f ∧
      f v ≠ f v'
have h : 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: use char he hL w
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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' : ℂ)
⊢ 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' : ℂ)
have 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' : ℂ)
Tactic: simp only [StarSubalgebra.coe_toSubalgebra, StarSubalgebra.coe_map, Set.mem_image,
    SetLike.mem_coe, exists_exists_and_eq_and, ne_eq]
-- 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₂
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (p : E × E) ↦ ‖B‖ * (‖f₁ (p.1 - p.2)‖ * ‖f₂ p.2‖))
    (Measure.prod volume volume)
have h : @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (x : E × E) ↦ ‖f₁ (x.1 - x.2)‖ * ‖f₂ x.2‖)
  (Measure.prod volume volume)
Tactic: apply Integrable.const_mul
-- 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₂
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (x : E × E) ↦ ‖f₁ (x.1 - x.2)‖ * ‖f₂ x.2‖)
    (Measure.prod volume volume)
have 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
Tactic: rw [integrable_prod_iff' (by fun_prop)]
-- 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₂
⊢ (∀ᵐ (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
have h : ∀ᵐ (y : E),
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ ‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖) volume
Tactic: constructor
-- 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₂
h :
  ∀ᵐ (y : E),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (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
have 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
Tactic: constructor
-- 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₂
⊢ ∀ᵐ (y : E),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : E) ↦ ‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖) volume
have h : ∀ (x : E), @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x_1 : E) ↦ ‖f₁ (x_1 - x)‖ * ‖f₂ x‖) volume
Tactic: filter_upwards with 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₃
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
have 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‖)
Tactic: apply hf₂.norm.bdd_mul (by fun_prop) (c := ‖(∫ y, ‖f₁ y‖)‖)
-- 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₂
⊢ ∀ᵐ (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‖)
have 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‖)
Tactic: filter_upwards with
-- 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₃
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 (y : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        ‖‖f₁ ((x, y).1 - (x, y).2)‖ * ‖f₂ (x, y).2‖‖)
    volume
have this : @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
-- 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
⊢ @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
have 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‖
Tactic: convert! this using 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
⊢ 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‖
have 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‖
Tactic: ext x