case hF_meas
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ (x : W), AEStronglyMeasurable (fun a => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a) μ

case h_bound
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ (x : W), ∀ᵐ (a : V) ∂μ, ‖↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a‖ ≤ ?bound a

case bound_integrable
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ Integrable ?bound

case h_cont
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ᵐ (a : V) ∂μ, Continuous fun x => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a

case bound
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ V → ℝ
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ Continuous (fourierIntegral e μ L f)
apply continuous_of_dominated
no goals
case hF_meas
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ (x : W), AEStronglyMeasurable (fun a => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a) μ
exact fun w => ((fourier_integral_convergent_iff he hL w).mp hf).1
case bound
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ V → ℝ

case h_bound
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
w : W
v : V
⊢ ‖↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v‖ ≤ ?bound v
case h_bound
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ (x : W), ∀ᵐ (a : V) ∂μ, ‖↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a‖ ≤ ?bound a
refine' fun w => ae_of_all _ fun v => _
no goals
case bound
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ V → ℝ
exact fun v => ‖f v‖
no goals
case h_bound
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
w : W
v : V
⊢ ‖↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v‖ ≤ ‖f v‖
rw [norm_smul, Complex.norm_eq_abs, abs_coe_circle, one_mul]
no goals
case bound_integrable
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ Integrable fun v => ‖f v‖
exact hf.norm
case h_cont
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous (Subtype.val ∘ ↑e)
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ᵐ (a : V) ∂μ, Continuous fun x => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a
case h_cont
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ᵐ (a : V) ∂μ, Continuous fun x => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a
rw [continuous_induced_rng] at he
case h_cont
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous (Subtype.val ∘ ↑e)
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
v : V
⊢ Continuous fun x => -↑(↑L v) x
case h_cont
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous (Subtype.val ∘ ↑e)
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ᵐ (a : V) ∂μ, Continuous fun x => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a
refine' ae_of_all _ fun v => (he.comp (continuous_ofAdd.comp _)).smul continuous_const
no goals
case h_cont
𝕜 : Type u_2
inst✝¹⁴ : CommRing 𝕜
V : Type u_3
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_1
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
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous (Subtype.val ∘ ↑e)
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
v : V
⊢ Continuous fun x => -↑(↑L v) x
refine' (hL.comp (continuous_prod_mk.mpr ⟨continuous_const, continuous_id⟩)).neg