case h
𝕜 : Type u_1
inst✝⁸ : CommRing 𝕜
V : Type u_2
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : MeasurableSpace V
W : Type u_3
inst✝⁴ : AddCommGroup W
inst✝³ : Module 𝕜 W
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ fourierIntegral e μ L (r • f) w = (r • fourierIntegral e μ L f) w
𝕜 : Type u_1
inst✝⁸ : CommRing 𝕜
V : Type u_2
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : MeasurableSpace V
W : Type u_3
inst✝⁴ : AddCommGroup W
inst✝³ : Module 𝕜 W
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
⊢ fourierIntegral e μ L (r • f) = r • fourierIntegral e μ L f
ext1 w
case h
𝕜 : Type u_1
inst✝⁸ : CommRing 𝕜
V : Type u_2
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : MeasurableSpace V
W : Type u_3
inst✝⁴ : AddCommGroup W
inst✝³ : Module 𝕜 W
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ (∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • r • f v ∂μ) =
    ∫ (a : V), r • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) w))) • f a ∂μ
case h
𝕜 : Type u_1
inst✝⁸ : CommRing 𝕜
V : Type u_2
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : MeasurableSpace V
W : Type u_3
inst✝⁴ : AddCommGroup W
inst✝³ : Module 𝕜 W
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ fourierIntegral e μ L (r • f) w = (r • fourierIntegral e μ L f) w
simp only [Pi.smul_apply, fourierIntegral, ← integral_smul]
case h.e_f
𝕜 : Type u_1
inst✝⁸ : CommRing 𝕜
V : Type u_2
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : MeasurableSpace V
W : Type u_3
inst✝⁴ : AddCommGroup W
inst✝³ : Module 𝕜 W
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ (fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • r • f v) = fun a =>
    r • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) w))) • f a
case h
𝕜 : Type u_1
inst✝⁸ : CommRing 𝕜
V : Type u_2
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : MeasurableSpace V
W : Type u_3
inst✝⁴ : AddCommGroup W
inst✝³ : Module 𝕜 W
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ (∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • r • f v ∂μ) =
    ∫ (a : V), r • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) w))) • f a ∂μ
congr
case h.e_f.h
𝕜 : Type u_1
inst✝⁸ : CommRing 𝕜
V : Type u_2
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : MeasurableSpace V
W : Type u_3
inst✝⁴ : AddCommGroup W
inst✝³ : Module 𝕜 W
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
x✝ : V
⊢ ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L x✝) w))) • r • f x✝ = r • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L x✝) w))) • f x✝
case h.e_f
𝕜 : Type u_1
inst✝⁸ : CommRing 𝕜
V : Type u_2
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : MeasurableSpace V
W : Type u_3
inst✝⁴ : AddCommGroup W
inst✝³ : Module 𝕜 W
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ (fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • r • f v) = fun a =>
    r • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) w))) • f a
funext
no goals
case h.e_f.h
𝕜 : Type u_1
inst✝⁸ : CommRing 𝕜
V : Type u_2
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : MeasurableSpace V
W : Type u_3
inst✝⁴ : AddCommGroup W
inst✝³ : Module 𝕜 W
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
x✝ : V
⊢ ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L x✝) w))) • r • f x✝ = r • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L x✝) w))) • f x✝
rw [smul_comm]