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✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ (fourierIntegral e μ L f + fourierIntegral e μ L g) w = fourierIntegral e μ L (f + g) 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✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
⊢ fourierIntegral e μ L f + fourierIntegral e μ L g = fourierIntegral e μ L (f + g)
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✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ ((∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v ∂μ) +
      ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v ∂μ) =
    ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • (f v + g v) ∂μ
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✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ (fourierIntegral e μ L f + fourierIntegral e μ L g) w = fourierIntegral e μ L (f + g) w
dsimp only [Pi.add_apply, fourierIntegral]
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✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ ((∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v ∂μ) +
      ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v ∂μ) =
    ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v + ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v ∂μ
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✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ ((∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v ∂μ) +
      ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v ∂μ) =
    ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • (f v + g v) ∂μ
simp_rw [smul_add]
case h.hf
𝕜 : 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✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v

case h.hg
𝕜 : 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✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v
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✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ ((∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v ∂μ) +
      ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v ∂μ) =
    ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v + ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v ∂μ
rw [integral_add]
no goals
case h.hf
𝕜 : 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✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v
exact (fourier_integral_convergent_iff he hL w).mp hf
no goals
case h.hg
𝕜 : 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✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : MeasureTheory.Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v
exact (fourier_integral_convergent_iff he hL w).mp hg