awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
w : W
aux :
  ∀ {g : V → E} (hg : Integrable g μ) (x : W),
    Integrable.{u_4, u_2} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
          (g v))
      μ
hf :
  Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊) (f v))
    μ
this : Integrable.{u_4, u_2} (ε := E) (fun (v : V) ↦ f v) μ
⊢ Integrable f μ

Tactic:
exact this
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
h : ∀ (w : W), fourierIntegral e μ L (f + g) w = (fourierIntegral e μ L f + fourierIntegral e μ L g) w
⊢ fourierIntegral e μ L (f + g) = fourierIntegral e μ L f + fourierIntegral e μ L g

Tactic:
ext1 w
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
h :
  ∫ (v : V),
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
        (f v + g v) ∂μ =
    HAdd.hAdd (α := E)
      (∫ (v : V),
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v) ∂μ)
      (∫ (v : V),
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (g v) ∂μ)
⊢ fourierIntegral e μ L (f + g) w = (fourierIntegral e μ L f + fourierIntegral e μ L g) w

Tactic:
dsimp only [Pi.add_apply, fourierIntegral]

Premises used: VectorFourier.fourierIntegral, Pi.add_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
h :
  ∫ (v : V),
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v) +
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (g v) ∂μ =
    HAdd.hAdd (α := E)
      (∫ (v : V),
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v) ∂μ)
      (∫ (v : V),
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (g v) ∂μ)
⊢ ∫ (v : V),
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
        (f v + g v) ∂μ =
    HAdd.hAdd (α := E)
      (∫ (v : V),
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v) ∂μ)
      (∫ (v : V),
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (g v) ∂μ)

Tactic:
simp_rw [smul_add]

Premises used: smul_add
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
h :
  Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊) (f v))
    μ
h₁ :
  Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊) (g v))
    μ
⊢ ∫ (v : V),
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v) +
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (g v) ∂μ =
    HAdd.hAdd (α := E)
      (∫ (v : V),
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v) ∂μ)
      (∫ (v : V),
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (g v) ∂μ)

Tactic:
rw [integral_add]

Premises used: MeasureTheory.integral_add
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊) (f v))
    μ

Tactic:
(fourierIntegral_convergent_iff he hL w).2 hf

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊) (f v))
    μ

Tactic:
exact (fourierIntegral_convergent_iff he hL w).2 hf

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊) (g v))
    μ

Tactic:
(fourierIntegral_convergent_iff he hL w).2 hg

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ Integrable.{u_4, u_2} (ε := E)
    (fun (v : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊) (g v))
    μ

Tactic:
exact (fourierIntegral_convergent_iff he hL w).2 hg

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst_13 : FirstCountableTopology W
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
hf : Integrable f μ
hF_meas :
  ∀ (x : W),
    AEStronglyMeasurable.{u_2, u_4} (β := E)
      (fun (a : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
          (f a))
      μ
h_bound :
  ∀ (x : W),
    ∀ᵐ (a : V) ∂μ,
      ‖HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
            (f a)‖ ≤
        ‖f a‖
bound_integrable : Integrable (ε := ℝ) (fun (v : V) ↦ ‖f v‖) μ
h_cont :
  ∀ᵐ (a : V) ∂μ,
    Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : W) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f a)
bound : V → ℝ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (fourierIntegral e μ L f)

Tactic:
apply continuous_of_dominated

Premises used: MeasureTheory.continuous_of_dominated
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst_13 : FirstCountableTopology W
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
hf : Integrable f μ
⊢ ∀ (x : W),
    AEStronglyMeasurable.{u_2, u_4} (β := E)
      (fun (a : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
          (f a))
      μ

Tactic:
fun w ↦ ((fourierIntegral_convergent_iff he hL w).2 hf).1

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff, And.left
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst_13 : FirstCountableTopology W
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
hf : Integrable f μ
⊢ ∀ (x : W),
    AEStronglyMeasurable.{u_2, u_4} (β := E)
      (fun (a : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
          (f a))
      μ

Tactic:
exact fun w ↦ ((fourierIntegral_convergent_iff he hL w).2 hf).1

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff, And.left
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst_13 : FirstCountableTopology W
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
hf : Integrable f μ
⊢ ∀ (x : W),
    ∀ᵐ (a : V) ∂μ,
      ‖HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
            (f a)‖ ≤
        ‖f a‖

Tactic:
fun w ↦ ae_of_all _ fun v ↦ le_of_eq (Circle.norm_smul _ _)

Premises used: MeasureTheory.ae_of_all, le_of_eq, DFunLike.coe, Neg.neg, Circle.norm_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst_13 : FirstCountableTopology W
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
hf : Integrable f μ
⊢ ∀ (x : W),
    ∀ᵐ (a : V) ∂μ,
      ‖HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
            (f a)‖ ≤
        ‖f a‖

Tactic:
exact fun w ↦ ae_of_all _ fun v ↦ le_of_eq (Circle.norm_smul _ _)

Premises used: MeasureTheory.ae_of_all, le_of_eq, Circle.norm_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst_13 : FirstCountableTopology W
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
hf : Integrable f μ
⊢ Integrable (ε := ℝ) (fun (v : V) ↦ ‖f v‖) μ

Tactic:
hf.norm

Premises used: MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst_13 : FirstCountableTopology W
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
hf : Integrable f μ
⊢ Integrable (ε := ℝ) (fun (v : V) ↦ ‖f v‖) μ

Tactic:
exact hf.norm

Premises used: MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst_13 : FirstCountableTopology W
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
hf : Integrable f μ
h_cont :
  ∀ (v : V),
    Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : W) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f v)
⊢ ∀ᵐ (a : V) ∂μ,
    Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : W) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f a)

Tactic:
filter_upwards with v
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst_13 : FirstCountableTopology W
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
f : V → E
hf : Integrable f μ
v : V
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : W) ↦
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊) (f v)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Fourier.FourierTransform
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
σ : ℂ →+* ℂ
inst_22 : RingHomIsometric σ
f : V → E
g : W → F
M : F →L[ℂ] E →SL[σ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hf₁ :
  Integrable (ε := G)
    (Function.uncurry fun (ξ : W) (x : V) ↦
      (((M : (a : F) → E →SL[σ] G) (g ξ) : E →SL[σ] G) : (a : E) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
          (f x)))
    (ν.prod μ)
⊢ Eq.{u_6 + 1} (α := G)
    (∫ (ξ : W),
      ∫ (x : V),
        (((M : (a : F) → E →SL[σ] G) (g ξ) : E →SL[σ] G) : (a : E) → G)
          (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
            (f x)) ∂μ ∂ν)
    (∫ (x : V),
      ∫ (ξ : W),
        (((M : (a : F) → E →SL[σ] G) (g ξ) : E →SL[σ] G) : (a : E) → G)
          (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
            (f x)) ∂ν ∂μ)

Tactic:
rw [integral_integral_swap]

Premises used: MeasureTheory.integral_integral_swap