awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (hypothesis)
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
⊢ Integrable.{u_4, u_2} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v))
      μ ↔
    Integrable f μ
have 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))
    μ
Tactic: have aux {g : V → E} (hg : Integrable g μ) (x : W) :
      Integrable (fun v : V ↦ e (-L v x) • g v) μ := by
    have c : Continuous fun v ↦ e (-L v x) := he.comp (hL.comp (.prodMk_left _)).neg
    simp_rw [← integrable_norm_iff (c.aestronglyMeasurable.smul hg.1), Circle.norm_smul]
    exact hg.norm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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))
      μ
⊢ Integrable.{u_4, u_2} (ε := E)
      (fun (v : V) ↦
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
          (f v))
      μ ↔
    Integrable f μ
have refine : ∀
  (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))
      μ),
  Integrable f μ
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ aux hf w⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (hypothesis)
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))
    μ
⊢ Integrable f μ
have this : Integrable.{u_4, u_2} (ε := E)
  (fun (v : V) ↦
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) (-w)) : 𝕊)
      (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
        (f v)))
  μ
Tactic: have := aux hf (-w)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 μ
⊢ fourierIntegral e μ L (f + g) = fourierIntegral e μ L f + fourierIntegral e μ L g
have h : ∀ (w : W), fourierIntegral e μ L (f + g) w = (fourierIntegral e μ L f + fourierIntegral e μ L g) w
Tactic: ext1 w
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ fourierIntegral e μ L (f + g) w = (fourierIntegral e μ L f + fourierIntegral e μ L g) w
have 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) ∂μ)
Tactic: dsimp only [Pi.add_apply, fourierIntegral]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ ∫ (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) ∂μ)
have 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) ∂μ)
Tactic: simp_rw [smul_add]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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
⊢ ∫ (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) ∂μ)
have 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))
  μ
Tactic: rw [integral_add]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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))
    μ
⊢ ∫ (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) ∂μ)
have 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))
  μ
Tactic: rw [integral_add]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 μ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (fourierIntegral e μ L f)
have 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))
    μ
Tactic: apply continuous_of_dominated
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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))
      μ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (fourierIntegral e μ L f)
have h_bound : ∀ (x : W),
  ∀ᵐ (a : V) ∂μ,
    ‖HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) a : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) x) : 𝕊)
          (f a)‖ ≤
      ‖f a‖
Tactic: apply continuous_of_dominated
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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‖
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (fourierIntegral e μ L f)
have bound_integrable : Integrable (ε := ℝ) (fun (v : V) ↦ ‖f v‖) μ
Tactic: apply continuous_of_dominated
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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‖) μ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (fourierIntegral e μ L f)
have 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)
Tactic: apply continuous_of_dominated
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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)
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (fourierIntegral e μ L f)
have bound : V → ℝ
Tactic: apply continuous_of_dominated
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 μ
⊢ ∀ᵐ (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)
have 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)
Tactic: filter_upwards with v
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
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 ν
⊢ 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)) ∂ν ∂μ)
have 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 μ)
Tactic: rw [integral_integral_swap]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (hypothesis)
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 ν
⊢ 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 μ)
have this : Integrable (ε := ℝ) (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ)
Tactic: have : Integrable (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ) :=
    (hg.norm.mul_prod hf.norm).const_mul _