From ac837f98b1058e47d8b11bfc73669a5398673155 Mon Sep 17 00:00:00 2001
From: stefanalbrecht <147979832+sterecht@users.noreply.github.com>
Date: Wed, 14 Aug 2024 15:02:50 +0200
Subject: [PATCH] Plancharel (#47)

The proof of Plancharel's theorem is done, except for one theorem about
convolutions that is missing from mathlib (which I didn't notice
earlier) and a silly norm-cast lemma that I couldn't figure out.
Unfortunately, I couldn't prove that L^1 intersected L^2 is a normed
space. I don't understand why, but nothing I tried worked in instance :
NormedSpace. This also means that I couldn't even state the following
lemmas (The inclusion is DenseInducing, etc.) without throwing errors.
I also updated the .tex file, so that the online version should have all
the links and the dependency graph should display the progress
correctly. (I did not test this, apart from making sure the LaTeX
compiles.)
---
 BonnAnalysis/Plancherel.lean         | 591 +++++++++++++++++++++++++--
 blueprint/src/chapter/plancherel.tex |  99 +++--
 2 files changed, 628 insertions(+), 62 deletions(-)

diff --git a/BonnAnalysis/Plancherel.lean b/BonnAnalysis/Plancherel.lean
index 6484f46..1b8abe4 100644
--- a/BonnAnalysis/Plancherel.lean
+++ b/BonnAnalysis/Plancherel.lean
@@ -3,43 +3,542 @@ import Mathlib.Analysis.Fourier.Inversion
 import Mathlib.Analysis.Fourier.PoissonSummation
 import Mathlib.Analysis.Fourier.RiemannLebesgueLemma
 import BonnAnalysis.StrongType
+import Mathlib.Analysis.Convolution
 
 noncomputable section
 
-open FourierTransform MeasureTheory Real
+open FourierTransform MeasureTheory Real Lp Memℒp Filter Complex Topology ComplexInnerProductSpace ComplexConjugate
 
 namespace MeasureTheory
 
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
 variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V]
   [BorelSpace V] [FiniteDimensional ℝ V]
 
-/-- Part of **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its Fourier transform is also in
-`L²`. -/
-theorem memℒp_fourierIntegral {f : V → E} (hf : Integrable f) (h2f : Memℒp f 2) :
-    Memℒp (𝓕 f) 2 := sorry
 
-/-- Part of **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its inverse Fourier transform is
-also in `L²`. -/
-theorem memℒp_fourierIntegralInv {f : V → E} (hf : Integrable f) (h2f : Memℒp f 2) :
-    Memℒp (𝓕⁻ f) 2 := sorry
+-- The Fourier transform of conj f is the conjugate of the inverse Fourier transform
+lemma fourier_conj {f : V → ℂ} : 𝓕 (conj f) = conj (𝓕 (f ∘ (fun x ↦ -x))) := by
+  unfold fourierIntegral VectorFourier.fourierIntegral
+  ext w
+  simp
+  rw [← integral_conj, ← integral_neg_eq_self]
+  apply congrArg (integral volume)
+  ext v
+  have : 𝐞 (-⟪v, w⟫_ℝ) • f (-v) = 𝐞 (-⟪v, w⟫_ℝ) * f (-v) := rfl
+  rw [this, starRingEnd_apply, starRingEnd_apply, star_mul']
+  have : 𝐞 (-⟪-v, w⟫_ℝ) • star (f (-v)) = 𝐞 (-⟪-v, w⟫_ℝ) * star (f (-v)) := rfl
+  rw [this]
+  simp
+  left
+  unfold Real.fourierChar
+  simp [← Complex.exp_conj, Complex.exp_neg, inv_inv, conj_ofReal]
+
+-- The fourier transform of a convolution is the product of the individual Fourier transforms
+lemma fourier_convolution {f g : V → ℂ} (hf : Integrable f volume) (hg : Integrable g volume) :
+    𝓕 (convolution f g (ContinuousLinearMap.mul ℂ ℂ) volume) = (𝓕 f) * (𝓕 g) := by
+  unfold convolution fourierIntegral VectorFourier.fourierIntegral
+  simp
+  ext x
+  simp
+  symm
+  calc (∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • f v) * ∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • g v
+    _ = ∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • f v * ∫ (w : V), 𝐞 (-⟪w, x⟫_ℝ) • g w := Eq.symm (integral_mul_right _ _)
+    _ = ∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • f v * ∫ (w : V), 𝐞 (-⟪w - v,x⟫_ℝ) • g (w - v) := ?_
+    _ = ∫ (v : V) (w : V), 𝐞 (-⟪v, x⟫_ℝ) * 𝐞 (-⟪w - v,x⟫_ℝ) * (f v * g (w - v)) := ?_
+    _ = ∫ (v : V) (w : V), 𝐞 (-⟪w, x⟫_ℝ) * (f v * g (w - v)) := ?_
+    _ = ∫ (w : V) (v : V), 𝐞 (-⟪w, x⟫_ℝ) * (f v * g (w - v)) := ?_
+    _ = ∫ (w : V), 𝐞 (-⟪w, x⟫_ℝ) * ∫ (v : V), f v * g (w - v) :=
+        congrArg (integral volume) <| (Set.eqOn_univ _ _).1 fun _ _ ↦ integral_mul_left _ _
+    _ = ∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • ∫ (t : V), f t * g (v - t) := rfl
+  · apply congrArg (integral volume)
+    ext v
+    simp
+    left
+    exact (@integral_sub_right_eq_self V ℂ _ _ _ volume _ _ _ (fun w ↦ 𝐞 (-⟪w,x⟫_ℝ) • g w) v).symm
+  · apply congrArg (integral volume)
+    ext v
+    rw [← integral_mul_left]
+    apply congrArg (integral volume)
+    ext w
+    have h1 : 𝐞 (-⟪v, x⟫_ℝ) • f v = 𝐞 (-⟪v, x⟫_ℝ) * f v := rfl
+    have h2 : 𝐞 (-⟪w - v, x⟫_ℝ) • g (w - v) = 𝐞 (-⟪w - v, x⟫_ℝ) * g (w - v) := rfl
+    rw [h1, h2]
+    ring
+  · apply congrArg (integral volume)
+    ext v
+    apply congrArg (integral volume)
+    ext w
+    apply mul_eq_mul_right_iff.2
+    left
+    unfold Real.fourierChar
+    simp only [AddChar.coe_mk, mul_neg, coe_inv_unitSphere, expMapCircle_apply, ofReal_mul, ofReal_ofNat]
+    rw [← Complex.exp_add]
+    apply congrArg (cexp)
+    simp
+    have : ⟪w, x⟫_ℝ = ⟪v, x⟫_ℝ + ⟪w - v, x⟫_ℝ := by
+      rw [← InnerProductSpace.add_left, add_sub_cancel]
+    rw [this]
+    push_cast
+    ring
+  · apply integral_integral_swap
+    rw [integrable_prod_iff]
+    constructor
+    · simp
+      apply ae_of_all volume
+      intro v
+      have h : AEStronglyMeasurable (fun a ↦ f v * g (a - v)) volume := by
+        apply AEStronglyMeasurable.mul aestronglyMeasurable_const
+        apply AEStronglyMeasurable.comp_measurePreserving (Integrable.aestronglyMeasurable hg)
+        exact measurePreserving_sub_right volume v
+      apply (integrable_norm_iff ?_).1
+      have : (∀ b, (fun a ↦ ‖(𝐞 (-⟪a,x⟫_ℝ) : ℂ) * (f v * g (a - v))‖) b = (fun a ↦ ‖f v * g (a - v)‖) b) := by
+        simp
+      apply (integrable_congr (ae_of_all volume this)).2
+      apply (integrable_norm_iff h).2
+      apply Integrable.const_mul
+      exact Integrable.comp_sub_right hg v
+      apply AEStronglyMeasurable.mul; swap; exact h
+      have : (fun y ↦ ↑(𝐞 (-⟪y, x⟫_ℝ))) = (Complex.exp ∘ ((- 2 * (π : ℂ) * I) • (fun y ↦ (⟪y, x⟫_ℝ : ℂ)))) := by
+        ext y
+        unfold Real.fourierChar
+        simp[Complex.exp_neg]
+        exact congrArg cexp (by ring)
+      rw [this]
+      apply aestronglyMeasurable_iff_aemeasurable.2
+      apply Measurable.comp_aemeasurable Complex.measurable_exp
+      apply AEMeasurable.const_smul (Continuous.aemeasurable ?_)
+      have : (fun y ↦ (⟪y, x⟫_ℝ : ℂ)) = ((fun x ↦ (x : ℂ)) : ℝ → ℂ) ∘ ((fun y ↦ ⟪y, x⟫_ℝ) : V → ℝ) := by
+        ext y; simp
+      rw [this]
+      exact Continuous.comp continuous_ofReal (Continuous.inner continuous_id' continuous_const)
+    · simp
+      have : (fun x ↦ ∫ (y : V), Complex.abs (f x) * Complex.abs (g (y - x))) = (fun x ↦ ‖f x‖ * ∫ (y : V), Complex.abs (g y)) := by
+        ext x
+        rw [← integral_add_right_eq_self _ x]
+        simp
+        exact integral_mul_left (Complex.abs (f x)) fun a ↦ Complex.abs (g a)
+      rw [this]
+      apply Integrable.mul_const
+      apply (integrable_norm_iff ?_).2
+      exact hf
+      exact Integrable.aestronglyMeasurable hf
+    · apply AEStronglyMeasurable.mul
+      have : AEStronglyMeasurable (fun a ↦ (𝐞 (-⟪a, x⟫_ℝ) : ℂ)) volume := by
+        unfold Real.fourierChar
+        simp
+        apply aestronglyMeasurable_iff_aemeasurable.2
+        apply Measurable.comp_aemeasurable measurable_inv
+        apply Measurable.comp_aemeasurable Complex.measurable_exp
+        apply AEMeasurable.mul_const _ I
+        apply AEMeasurable.const_mul
+        apply Continuous.aemeasurable
+        have : (fun y ↦ (⟪y, x⟫_ℝ : ℂ)) = ((fun x ↦ (x : ℂ)) : ℝ → ℂ) ∘ ((fun y ↦ ⟪y, x⟫_ℝ) : V → ℝ) := by
+          ext y; simp
+        rw [this]
+        exact Continuous.comp continuous_ofReal (Continuous.inner continuous_id' continuous_const)
+      exact @AEStronglyMeasurable.snd V V _ _ volume volume _ _ _ _ this
+      apply AEStronglyMeasurable.mul
+      exact AEStronglyMeasurable.fst (Integrable.aestronglyMeasurable hf)
+      have : ((fun a : V × V ↦ g (a.2 - a.1)) = (fun a ↦ g (a.1 - a.2)) ∘ (fun a ↦ (a.2,a.1))) := by
+        ext a; simp
+      rw [this]
+      apply AEStronglyMeasurable.comp_measurePreserving _ (Measure.measurePreserving_swap)
+      apply AEStronglyMeasurable.comp_aemeasurable
+      apply AEStronglyMeasurable.mono_ac (quasiMeasurePreserving_sub_of_right_invariant volume volume).absolutelyContinuous
+      exact hg.1
+      exact Measurable.aemeasurable measurable_sub
+
+
+-- The function f ⋆ conj (f(-x)) which is used in Plancharel's theorem
+-- We prove that it is continuous and integrable and calculate its Fourier transform
+def selfConvolution (f : V → ℂ) := convolution f (conj (fun x ↦ f (-x))) (ContinuousLinearMap.mul ℂ ℂ)
+
+lemma integrable_selfConvolution {f : V → ℂ} (hf : Integrable f volume) : Integrable (selfConvolution f) volume := by
+  unfold selfConvolution
+  apply MeasureTheory.Integrable.integrable_convolution (ContinuousLinearMap.mul ℂ ℂ) hf
+  apply (integrable_norm_iff _).1
+  · have : (fun a ↦ ‖(starRingEnd (V → ℂ)) (fun x ↦ f (-x)) a‖) = (fun a ↦ ‖f (-a)‖) := by
+      ext a; simp
+    rw [this]
+    apply (integrable_norm_iff _).2
+    exact Integrable.comp_neg hf
+    rw [show (fun a ↦ f (-a)) = (f ∘ (fun a ↦ -a)) from by ext a; simp]
+    apply AEStronglyMeasurable.comp_aemeasurable
+    rw [Measure.map_neg_eq_self]
+    exact hf.aestronglyMeasurable
+    exact AEMeasurable.neg aemeasurable_id
+  · rw [show ((starRingEnd (V → ℂ)) fun x ↦ f (-x)) = ((starRingEnd ℂ) ∘ (fun x ↦ f (-x))) from ?_]
+    apply AEStronglyMeasurable.comp_aemeasurable
+    apply Continuous.aestronglyMeasurable
+    exact continuous_conj
+    rw [show (fun a ↦ f (-a)) = (f ∘ (fun a ↦ -a)) from by ext a; simp]
+    apply AEMeasurable.comp_aemeasurable
+    rw [Measure.map_neg_eq_self]
+    exact hf.aemeasurable
+    exact AEMeasurable.neg aemeasurable_id
+    ext x
+    simp
+
+/- This lemma follows easily from the following fact:
+   f ⋆ g is continuous if f ∈ L^p and g ∈ L^q with p,q conjugate.
+   This is listed as TODO in Mathlib.Analysis.Convolution -/
+lemma continuous_selfConvolution {f : V → ℂ} (hf : Memℒp f 2) : Continuous (selfConvolution f) := by
+  unfold selfConvolution
+  sorry
+
+
+lemma fourier_selfConvolution {f : V → ℂ}  (hf : Integrable f) :
+    𝓕 (selfConvolution f) = fun x ↦ (‖𝓕 f x‖ : ℂ) ^ 2 := by
+  unfold selfConvolution
+  rw [fourier_convolution, fourier_conj]
+  ext x; simp
+  have : ((fun x ↦ f (-x)) ∘ fun x ↦ -x) = f := by ext x; simp
+  rw [this, mul_conj']
+  simp
+  exact hf
+  apply (integrable_norm_iff ?_).1
+  · have : (fun a ↦ ‖conj (fun x ↦ f (-x)) a‖) = (fun a ↦ ‖f (-a)‖) := by
+      ext a
+      simp
+    rw [this]
+    exact Integrable.norm (Integrable.comp_neg hf)
+  · apply aestronglyMeasurable_iff_aemeasurable.2
+    apply Measurable.comp_aemeasurable (Continuous.measurable continuous_conj)
+    exact Integrable.aemeasurable (Integrable.comp_neg hf)
+
+
+-- In the proofs we sometimes have to convert between ∫ and ∫⁻. This is surprisingly tricky,
+-- the following two lemmas are helpful
+lemma l2norm_bochnerIntegral {f : V → ℂ} (h2f : Memℒp f 2) : snorm f 2 volume =
+    ENNReal.ofReal ((∫ v : V, ‖f v‖ ^ 2) ^ ((1 : ℝ) / 2)) := by
+  unfold snorm; simp; unfold snorm'; simp
+  rw [← ENNReal.ofReal_rpow_of_nonneg]
+  apply congrArg (fun x ↦ (x ^ (2 : ℝ)⁻¹))
+  rw [ofReal_integral_eq_lintegral_ofReal]
+  · apply congrArg (lintegral volume)
+    ext x
+    rw [ENNReal.ofReal_pow]
+    apply congrArg (fun x ↦ x ^ 2)
+    rw [← ofReal_norm_eq_coe_nnnorm]
+    simp
+    exact AbsoluteValue.nonneg Complex.abs (f x)
+  · rw [Integrable.eq_1]; constructor
+    · rw [show (fun v ↦ Complex.abs (f v) ^ 2) = (fun x ↦ x ^ 2) ∘ (fun v ↦ Complex.abs (f v)) from by ext v; simp]
+      apply aestronglyMeasurable_iff_aemeasurable.2
+      apply Measurable.comp_aemeasurable
+      exact Measurable.pow_const (fun ⦃t⦄ a ↦ a) 2
+      apply Measurable.comp_aemeasurable (Continuous.measurable Complex.continuous_abs)
+      exact aestronglyMeasurable_iff_aemeasurable.1 h2f.1
+    · rw [hasFiniteIntegral_def]
+      rw [show (fun a ↦ (‖Complex.abs (f a) ^ 2‖₊ : ENNReal)) = (fun a ↦ (‖f a‖₊ ^ 2 : ENNReal)) from ?_]
+      have : snorm f 2 volume < ⊤ := h2f.2
+      unfold snorm at this; simp at this; unfold snorm' at this; simp at this
+      have : ((∫⁻ (a : V), ↑‖f a‖₊ ^ 2) ^ (2 : ℝ)⁻¹) ^ (2 : ℝ) < ⊤ := by
+        rw [ENNReal.rpow_two]
+        exact ENNReal.pow_lt_top this 2
+      rw [← ENNReal.rpow_mul] at this
+      simp at this
+      exact this
+      ext v
+      rw [← ofReal_norm_eq_coe_nnnorm, ← ofReal_norm_eq_coe_nnnorm, ← ENNReal.ofReal_pow]
+      simp
+      exact norm_nonneg (f v)
+  · apply ae_of_all volume; simp
+  · apply integral_nonneg
+    intro v
+    simp
+  · simp
+
+
+lemma integrable_iff_memℒ2 {f : V → ℂ} : Memℒp f 2 ↔
+    AEStronglyMeasurable f volume ∧ Integrable (fun v ↦ ‖f v‖ ^ 2) := by
+  constructor
+  intro h
+  constructor
+  exact h.1
+  constructor
+  · apply aestronglyMeasurable_iff_aemeasurable.2
+    rw [show (fun v ↦ ‖f v‖ ^ 2) = (fun v ↦ ‖v‖ ^ 2) ∘ f from by ext v; rfl]
+    apply Measurable.comp_aemeasurable _ (aestronglyMeasurable_iff_aemeasurable.1 h.1)
+    exact Continuous.measurable <| Continuous.comp (continuous_pow 2) (continuous_norm)
+  unfold HasFiniteIntegral
+  simp
+  rw [show ∫⁻ (a : V), ↑‖Complex.abs (f a)‖₊ ^ 2 = ∫⁻ (a : V), ↑‖f a‖₊ ^ (2 : ℝ) from ?_]
+  exact (snorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top (p := 2) (by simp) (by simp)).1 h.2
+  apply congrArg (lintegral volume)
+  ext a
+  simp [← ofReal_norm_eq_coe_nnnorm]
+  intro h
+  constructor
+  exact h.1
+  unfold Integrable HasFiniteIntegral at h
+  unfold snorm snorm'; simp
+  rw [show ∫⁻ (a : V), ↑‖(fun v ↦ ‖f v‖ ^ 2) a‖₊ = ∫⁻ (a : V), ↑‖f a‖₊ ^ 2 from ?_] at h
+  apply (ENNReal.rpow_lt_top_iff_of_pos (by simp)).2 h.2.2
+  apply congrArg (lintegral volume)
+  ext a
+  simp [← ofReal_norm_eq_coe_nnnorm]
+
+
+
+lemma Complex.ofReal_integrable (f : V → ℝ) : Integrable (fun x ↦ f x) ↔ Integrable (fun x ↦ (f x : ℂ)) := by
+  constructor
+  exact Integrable.ofReal
+  intro h
+  have : Integrable (fun x ↦ (f x : ℂ).re) volume := MeasureTheory.Integrable.re h
+  simp at this
+  exact this
+
+
+-- I really don't know why I can't show this, it should be easy.
+lemma Complex.ofReal_integral (f : V → ℝ) : ∫ (v : V), f v = ∫ (v : V), (f v : ℂ) := by
+  by_cases h : Integrable (fun v ↦ f v)
+  · sorry
+  · simp [integral_undef h, integral_undef (fun k ↦ h ((ofReal_integrable f).2 k))]
+
+
 
 /-- **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its Fourier transform has the same
 `L²` norm as that of `f`. -/
-theorem snorm_fourierIntegral {f : V → E} (hf : Integrable f) (h2f : Memℒp f 2) :
-    snorm (𝓕 f) 2 volume = snorm f 2 volume := sorry
+theorem snorm_fourierIntegral {f : V → ℂ} (hf : Integrable f) (h2f : Memℒp f 2) :
+    snorm (𝓕 f) 2 volume = snorm f 2 volume := by
+  have hpos : {c : ℝ | c > 0} ∈ atTop := by
+      simp only [gt_iff_lt, mem_atTop_sets, ge_iff_le, Set.mem_setOf_eq]
+      use 1; intro b h; linarith
+  have lim1 : Tendsto (fun (c : ℝ) ↦ ∫ v : V, cexp (-c⁻¹ * ‖v‖ ^ 2) * 𝓕 (selfConvolution f) v) atTop
+      (𝓝 (∫ v : V, ‖f v‖ ^ 2)) := by
+    have : (fun (c : ℝ) ↦ (∫ v : V, 𝓕 (fun w ↦ cexp (-c⁻¹ * ‖w‖ ^ 2)) v * (selfConvolution f v))) =ᶠ[atTop] (fun c ↦ ∫ v : V, cexp (-c⁻¹ * ‖v‖ ^ 2) * 𝓕 (selfConvolution f) v) := by
+      apply Filter.eventuallyEq_of_mem hpos
+      intro c hc
+      dsimp
+      unfold fourierIntegral
+      rw [show ∫ (v : V), VectorFourier.fourierIntegral 𝐞 volume (innerₗ V) (fun w ↦ cexp (-c⁻¹ * ↑‖w‖ ^ 2)) v * selfConvolution f v =
+          ∫ (v : V), (ContinuousLinearMap.mul ℂ ℂ) (VectorFourier.fourierIntegral 𝐞 volume (innerₗ V) (fun w ↦ cexp (-c⁻¹ * ↑‖w‖ ^ 2)) v) (selfConvolution f v) from ?_]; swap
+      · apply congrArg (integral volume)
+        simp
+      rw [VectorFourier.integral_bilin_fourierIntegral_eq_flip]
+      simp
+      · exact continuous_fourierChar
+      · simp
+        exact continuous_inner
+      · simpa using GaussianFourier.integrable_cexp_neg_mul_sq_norm_add (by simpa) 0 (0 : V)
+      · exact integrable_selfConvolution hf
+    apply Tendsto.congr' this
+    apply Tendsto.congr' (show ((fun (c : ℝ) ↦ ∫ v : V, ((π * c) ^ (FiniteDimensional.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * c * ‖0 - v‖^2)) * (selfConvolution f v)) =ᶠ[atTop]
+        (fun c ↦ ∫ v : V, 𝓕 (fun w ↦ cexp (-c⁻¹ * ‖w‖ ^ 2)) v * (selfConvolution f v))) from ?_); swap
+    · apply Filter.eventuallyEq_of_mem hpos
+      intro c hc
+      simp at hc
+      dsimp
+      apply congrArg (integral volume)
+      ext v
+      simp only [mul_eq_mul_right_iff]
+      left
+      rw [fourierIntegral_gaussian_innerProductSpace]
+      simp
+      constructor
+      ring_nf
+      simpa
+    have : ∫ v : V, (‖f v‖ : ℂ) ^ 2 = selfConvolution f 0 := by
+      unfold selfConvolution convolution
+      simp
+      apply congrArg (integral volume)
+      ext v
+      rw [mul_comm, ← Complex.normSq_eq_conj_mul_self, ← Complex.sq_abs]
+      simp
+    rw [this]
+    apply tendsto_integral_gaussian_smul' (integrable_selfConvolution hf)
+    exact Continuous.continuousAt (continuous_selfConvolution h2f)
+  have lim2 : Tendsto (fun (c : ℝ) ↦ ∫ v : V, cexp (- c⁻¹ * ‖v‖ ^ 2) * 𝓕 (selfConvolution f) v) atTop
+      (𝓝 (∫ v : V, ‖𝓕 f v‖ ^ 2)) := by
+    rw [fourier_selfConvolution hf]
+    by_cases hF : Integrable (fun x ↦ (‖𝓕 f x‖ ^ 2)) volume
+    · apply tendsto_integral_filter_of_dominated_convergence _ _ _ hF
+      apply ae_of_all volume
+      intro v
+      rw [show (‖𝓕 f v‖ ^ 2) = cexp (- (0 : ℝ) * ‖v‖ ^ 2) * (‖𝓕 f v‖ ^ 2) by simp]
+      apply (Tendsto.cexp _).smul_const
+      exact tendsto_inv_atTop_zero.ofReal.neg.mul_const _
+      simp
+      use (1 : ℝ)
+      intro b hb
+      apply AEStronglyMeasurable.mul
+      apply Integrable.aestronglyMeasurable
+      have hb : 0 < (b : ℂ)⁻¹.re := by simpa using by linarith
+      simpa using GaussianFourier.integrable_cexp_neg_mul_sq_norm_add hb 0 (0 : V)
+      apply Integrable.aestronglyMeasurable
+      simp at hF
+      norm_cast
+      exact Integrable.ofReal hF
+      simp
+      use 1
+      intro b hb
+      apply ae_of_all volume
+      intro v
+      rw [← one_mul (Complex.abs (𝓕 f v)), mul_pow, ← mul_assoc, show ((1 : ℝ) ^ 2 = 1) from by simp, mul_one]
+      apply mul_le_mul_of_nonneg_right
+      rw [Complex.abs_exp]
+      simp
+      apply Left.mul_nonneg
+      simpa using by linarith
+      rw [show ((‖v‖ : ℂ) ^ 2).re = ‖v‖ ^ 2 from by norm_cast]
+      exact sq_nonneg ‖v‖
+      exact sq_nonneg (Complex.abs (𝓕 f v))
+    · have : ¬Integrable (fun v ↦ (‖𝓕 f v‖ : ℂ) ^ 2) := by
+        norm_cast
+        intro h
+        rw [← Complex.ofReal_integrable] at h
+        exact hF h
+      rw [integral_undef this]
+      have : ∀ᶠ (c : ℝ) in atTop, ¬Integrable (fun v ↦ cexp (-↑c⁻¹ * (‖v‖ : ℂ) ^ 2) * (fun x ↦ (‖𝓕 f x‖ : ℂ) ^ 2) v) := by
+        by_contra h
+        simp at h
+        absurd this
+        sorry
+      have : ∀ᶠ (c : ℝ) in atTop, 0 = ∫ (v : V), cexp (-↑c⁻¹ * (‖v‖ : ℂ) ^ 2) * (fun x ↦ (‖𝓕 f x‖ : ℂ) ^ 2) v := by
+        simp
+        simp at this
+        obtain ⟨a, ha⟩ := this
+        use a
+        intro b hb
+        rw [integral_undef (ha b hb)]
+      apply Tendsto.congr' this
+      rw [tendsto_def]
+      intro s hs
+      simp
+      use 0
+      intro _ _
+      exact mem_of_mem_nhds hs
+  have hm : AEStronglyMeasurable (𝓕 f) := by
+    apply Continuous.aestronglyMeasurable
+    apply VectorFourier.fourierIntegral_continuous continuous_fourierChar
+        (by simp only [innerₗ_apply]; exact continuous_inner) hf
+  have : ∫ (v : V), (‖𝓕 f v‖ : ℂ) ^ 2 = ∫ (v : V), (‖f v‖ : ℂ) ^ 2 := tendsto_nhds_unique lim2 lim1
+  have : ∫ (v : V), ‖𝓕 f v‖ ^ 2 = ∫ (v : V), ‖f v‖ ^ 2 := by
+    norm_cast at this
+    apply ofReal_inj.1
+    rw [Complex.ofReal_integral, Complex.ofReal_integral, this]
+  rw [l2norm_bochnerIntegral h2f, l2norm_bochnerIntegral, this]
+  constructor; exact hm
+  by_cases H : snorm f 2 volume = 0
+  · rw [snorm_eq_zero_iff] at H
+    have : ∀ w, (fun v ↦ 𝐞 (-⟪v, w⟫_ℝ) • f v) =ᶠ[ae volume] 0 := by
+      intro w
+      rw [eventuallyEq_iff_exists_mem]
+      rw [eventuallyEq_iff_exists_mem] at H
+      obtain ⟨s,hs,h⟩ := H
+      use s
+      constructor
+      exact hs
+      intro x hx
+      simp
+      rw [h hx]
+      simp
+    have : 𝓕 f = 0 := by
+      unfold fourierIntegral VectorFourier.fourierIntegral
+      ext w
+      simp
+      exact integral_eq_zero_of_ae (this w)
+    rw [this]
+    simp
+    exact hf.1
+    simp
+  have : Memℒp (𝓕 f) 2 := by
+    apply integrable_iff_memℒ2.2
+    constructor
+    exact hm
+    apply MeasureTheory.Integrable.of_integral_ne_zero
+    rw [this]
+    unfold snorm snorm' at H; simp at H
+    have : 0 < ∫⁻ (v : V), ‖f v‖₊ ^ 2 := by
+      apply lt_of_le_of_ne (zero_le _) (fun a ↦ H (id (Eq.symm a)))
+    have : 0 < ENNReal.ofReal (∫ (v : V), ‖f v‖ ^ 2) := by
+      rw [ofReal_integral_eq_lintegral_ofReal]
+      norm_cast at this
+      apply lt_of_lt_of_le this (le_of_eq _)
+      apply congrArg (lintegral volume)
+      ext v
+      simp [← ofReal_norm_eq_coe_nnnorm]
+      rw [ENNReal.ofReal_pow (AbsoluteValue.nonneg Complex.abs (f v))]
+      exact (integrable_iff_memℒ2.1 h2f).2
+      apply ae_of_all
+      intro a
+      simp
+    rw [ENNReal.ofReal_pos] at this
+    exact Ne.symm (ne_of_lt this)
+  exact this.2
+
+
+/-- Part of **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its Fourier transform is
+also in `L²`. -/
+theorem memℒp_fourierIntegral {f : V → ℂ} (hf : Integrable f) (h2f : Memℒp f 2) :
+    Memℒp (𝓕 f) 2 := by
+  unfold Memℒp; constructor
+  · apply Continuous.aestronglyMeasurable
+    exact VectorFourier.fourierIntegral_continuous continuous_fourierChar
+        (by simp only [innerₗ_apply]; exact continuous_inner) hf
+  · rw [snorm_fourierIntegral hf h2f]
+    exact h2f.2
+
+/-- Part of **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its inverse Fourier transform is
+also in `L²`. -/
+theorem memℒp_fourierIntegralInv {f : V → ℂ} (hf : Integrable f) (h2f : Memℒp f 2) :
+    Memℒp (𝓕⁻ f) 2 := by
+  rw [fourierIntegralInv_eq_fourierIntegral_comp_neg]
+  apply memℒp_fourierIntegral (Integrable.comp_neg hf)
+  apply Memℒp.comp_of_map
+  simpa
+  exact AEMeasurable.neg aemeasurable_id
 
 /-- **Plancherel theorem**: if `f` is in `L¹ ∩ L²` then its inverse Fourier transform has the same
 `L²` norm as that of `f`. -/
-theorem snorm_fourierIntegralInv {f : V → E} (hf : Integrable f) (h2f : Memℒp f 2) :
-    snorm (𝓕⁻ f) 2 volume = snorm f 2 volume := sorry
+theorem snorm_fourierIntegralInv {f : V → ℂ} (hf : Integrable f) (h2f : Memℒp f 2) :
+    snorm (𝓕⁻ f) 2 volume = snorm f 2 volume := by
+  trans snorm (𝓕 f) 2 volume
+  · unfold snorm; simp; unfold snorm'
+    apply congrArg (fun x ↦ x ^ (1 / 2))
+    trans ∫⁻ (a : V), ‖𝓕 f (-a)‖₊ ^ (2 : ℝ)
+    · apply lintegral_rw₁ _ id
+      apply Germ.coe_eq.1 (congrArg Germ.ofFun _)
+      ext a
+      rw [fourierIntegralInv_eq_fourierIntegral_neg]
+    · rw [← @lintegral_map' _ _ _ _ _ (fun x ↦ (‖𝓕 f x‖₊ : ENNReal) ^ 2) (fun x ↦ -x) _ (AEMeasurable.neg aemeasurable_id)]
+      simp; simp
+      have : (fun x ↦ (‖𝓕 f x‖₊ : ENNReal) ^ 2) = (fun x ↦ x ^ 2) ∘ (fun x ↦ (‖𝓕 f x‖₊ : ENNReal)) := by
+        ext x; simp
+      rw [this]
+      apply Measurable.comp_aemeasurable (Measurable.pow_const (fun ⦃t⦄ a ↦ a) 2)
+      have : (fun x ↦ (‖𝓕 f x‖₊ : ENNReal)) = (fun x ↦ (‖x‖₊ : ENNReal)) ∘ (fun x ↦ 𝓕 f x) := by
+        ext x; simp
+      rw [this]
+      exact Measurable.comp_aemeasurable (Continuous.measurable <| ENNReal.continuous_coe_iff.2 continuous_nnnorm) <|
+        AEStronglyMeasurable.aemeasurable (memℒp_fourierIntegral hf h2f).1
+  · exact snorm_fourierIntegral hf h2f
+
+
+
+def L12 (V : Type*) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V]
+  [BorelSpace V] [FiniteDimensional ℝ V] : AddSubgroup (V →₂[volume] ℂ) where
+  carrier := {f | snorm f 1 volume < ⊤}
+  add_mem' := by
+    simp
+    intro a _ b _ h2a h2b
+    have h1a : Memℒp a 1 volume := mem_Lp_iff_memℒp.1 (mem_Lp_iff_snorm_lt_top.2 h2a)
+    have h1b : Memℒp b 1 volume := mem_Lp_iff_memℒp.1 (mem_Lp_iff_snorm_lt_top.2 h2b)
+    simp [snorm_congr_ae (AEEqFun.coeFn_add a b)]
+    apply lt_of_le_of_lt (snorm_add_le h1a.1 h1b.1 _)
+    exact ENNReal.add_lt_top.2 ⟨h2a, h2b⟩
+    rfl
+  zero_mem' := by simp [snorm_congr_ae AEEqFun.coeFn_zero, snorm_zero]
+  neg_mem' := by simp[snorm_congr_ae (AEEqFun.coeFn_neg _)]
+
+instance : NormedAddCommGroup (L12 V) := AddSubgroup.normedAddCommGroup
 
 
 scoped[MeasureTheory] notation:25 α " →₁₂[" μ "] " E =>
     ((α →₁[μ] E) ⊓ (α →₂[μ] E) : AddSubgroup (α →ₘ[μ] E))
-
+/-
 /- Note: `AddSubgroup.normedAddCommGroup` is almost this, but not quite. -/
-instance : NormedAddCommGroup (V →₁₂[volume] E) :=
+instance : NormedAddCommGroup (V →₁₂[volume] ℂ) :=
   AddGroupNorm.toNormedAddCommGroup {
     toFun := fun ⟨f,_⟩ ↦ ENNReal.toReal <| snorm f 2 volume
     map_zero' := by simp [snorm_congr_ae AEEqFun.coeFn_zero, snorm_zero]
@@ -56,19 +555,63 @@ instance : NormedAddCommGroup (V →₁₂[volume] E) :=
       ext
       apply ae_eq_trans <| (snorm_eq_zero_iff ((Lp.mem_Lp_iff_memℒp.1 hf).1) (by simp)).1 h
       apply ae_eq_trans (Lp.coeFn_zero E 2 volume).symm; rfl
-  }
+  }-/
+lemma memℒ12_iff {f : V → ℂ} (hf : Memℒp f 2 volume) :
+    (hf.toLp) ∈ L12 V ↔ Integrable f := by
+  constructor
+  · intro h
+    unfold L12 at h
+    simp at h
+    unfold Integrable
+    constructor
+    exact hf.1
+    unfold HasFiniteIntegral
+    unfold snorm snorm' at h
+    simp at h
+    have : ∫⁻ (a : V), ‖f a‖₊ = ∫⁻ (a : V), ‖toLp f hf a‖₊ := by
+      sorry
+    rw [this]
+    exact h
+  · sorry
+
+lemma memL12_iff {f : V →₂[volume] ℂ} : f ∈ L12 V ↔ Integrable (↑f) := by
+  constructor
+  · intro h
+    apply (memℒ12_iff _).1
+    rw [toLp_coeFn]
+    exact h
+    rw [← mem_Lp_iff_memℒp]
+    simp
+  · intro h
+    rw [← toLp_coeFn f, memℒ12_iff]
+    exact h
+    rw [← mem_Lp_iff_memℒp]
+    simp
 
-instance : NormedSpace ℝ (V →₁₂[volume] E) := sorry
+instance : NormedSpace ℝ (L12 V) where
+  smul := fun a f ↦ by
+    use a • f
+    sorry
+  one_smul := by
+    intro ⟨f, hf⟩
+    sorry
+  mul_smul := sorry
+  smul_zero := sorry
+  smul_add := sorry
+  add_smul := sorry
+  zero_smul := sorry
+  norm_smul_le := sorry
 
 
 /- The Fourier integral as a continuous linear map `L^1(V, E) ∩ L^2(V, E) → L^2(V, E)`. -/
-def fourierIntegralL2OfL12Fun : (V →₁₂[volume] E) → (V →₂[volume] E) :=
-  fun ⟨f,hf,hf2⟩ ↦ (memℒp_fourierIntegral (memℒp_one_iff_integrable.1 <|
-      Lp.mem_Lp_iff_memℒp.1 hf) (Lp.mem_Lp_iff_memℒp.1 hf2)).toLp <| 𝓕 f
+def fourierIntegralL2OfL12Fun : (V →₁₂[volume] ℂ) → (V →₂[volume] ℂ) := sorry
+  --fun ⟨f,hf,hf2⟩ ↦ (memℒp_fourierIntegral (memℒp_one_iff_integrable.1 <|
+  --    Lp.mem_Lp_iff_memℒp.1 (by sorry)) (Lp.mem_Lp_iff_memℒp.1 hf2)).toLp <| 𝓕 f
 
-def fourierIntegralL2OfL12 : (V →₁₂[volume] E) →L[ℝ] (V →₂[volume] E) := sorry
+--def fourierIntegralL2OfL12 : (V →₁₂[volume] ℂ) →L[ℝ] (V →₂[volume] ℂ) := sorry
   /-have : IsBoundedLinearMap ℝ fourierIntegralL2OfL12Fun := {
-    map_add := sorry
+    map_add := by
+      intro f g
     map_smul := sorry
     bound := sorry
   }
@@ -77,7 +620,7 @@ def fourierIntegralL2OfL12 : (V →₁₂[volume] E) →L[ℝ] (V →₂[volume]
 
 
 /- The Fourier integral as a continuous linear map `L^2(V, E) → L^2(V, E)`. -/
-def fourierIntegralL2 : (V →₂[volume] E) →L[ℝ] (V →₂[volume] E) :=
+def fourierIntegralL2 : (V →₂[volume] ℂ) →L[ℝ] (V →₂[volume] ℂ) :=
   sorry
 
 end MeasureTheory
diff --git a/blueprint/src/chapter/plancherel.tex b/blueprint/src/chapter/plancherel.tex
index 34a7f68..a8b9acd 100644
--- a/blueprint/src/chapter/plancherel.tex
+++ b/blueprint/src/chapter/plancherel.tex
@@ -29,6 +29,10 @@ \section{Basic Properties of the Fourier Transform}
   Let $f\in L^1(V,E)$. Then its Fourier transform $\widehat f$ is well-defined and bounded.
   In particular, the Fourier transform defines a map $\mathcal F:L^1(V,E)\to L^\infty(V,E)$.
 \end{lemma}
+\begin{proof}
+  \leanok
+  Omitted.
+\end{proof}
 
 From now on assume that $V$ and $W$ are equipped with second-countable topologies such that
 $L$ is continuous.
@@ -39,6 +43,10 @@ \section{Basic Properties of the Fourier Transform}
   \leanok
   Let $f\in L^1(V,E)$. Then $\widehat f$ is continuous.
 \end{lemma}
+\begin{proof}
+  \leanok
+  Omitted.
+\end{proof}
 
 \begin{lemma}[Multiplication formula]
 \label{lem:fourier-multiplication}
@@ -48,38 +56,51 @@ \section{Basic Properties of the Fourier Transform}
 Let $f,g\in L^1(V,E)$. Then
 $$\int_WM(\widehat f(w),g(w))\,d\nu(w)=\int_VM(f(v),\widehat g(v))\,d\mu(v).$$
 \end{lemma}
+\begin{proof}
+  \leanok
+  Omitted.
+\end{proof}
 
 \begin{lemma}
   \label{lem:fourier-prop}
   \uses{def:fourier-transform}
-  \lean{}
-  % \leanok
-Let $f,g\in L^1(V,E)$, $t\in\R$ and $a,b\in\C$. The Fourier transform satisfies the following elementary properties:
+  \lean{VectorFourier.fourierIntegral_add,
+        Fourier.fourierIntegral_comp_add_right,
+        Fourier.fourierIntegral_smul_const,
+        MeasureTheory.fourier_conj,
+        MeasureTheory.fourier_convolution}
+  \leanok
+Lef $f,g\in L^1(V,E)$, $t\in\R$ and $a,b\in\C$. The Fourier transform satisfies the following elementary properties:
 \begin{enumerate}
   \item[(i)] $\mathcal F(af+bg)=a\mathcal Ff+b\mathcal Fg$\hfill(Linearity)
   \item[(ii)] $\mathcal F(f(x-t)) = e^{-2\pi i ty}\mathcal F f(y)$\hfill (Shifting)
   \item[(iii)] $\mathcal F(f(tx)) = \frac1{|t|}\mathcal F f(\frac yt)$\hfill (Scaling)
-  \item[(iv)] $\mathcal F(\overline{f(x)}) = \overline{\mathcal Ff(-y)}$\hfill (Conjugation)
+  \item[(iv)] If $E$ admits a conjugation, then $\mathcal F(\overline{f(x)}) = \overline{\mathcal Ff(-y)}$\hfill (Conjugation)
   \item[(v)] Define the convolution of $f$ and $g$ w.r.t. a bilinear map $M:E\times E\to F$ as
              $$(f\ast_Mg)(w):=\int_VM(f(v),g(w-v))\,d\mu(v).$$ Then
              $\mathcal F(f\ast_M g) =M(\mathcal Ff,\mathcal Fg)$ \hfill (Convolution)
 \end{enumerate}
 \end{lemma}
+\begin{proof}
+  \leanok
+  Omitted.
+\end{proof}
 From now on, let $V$ be a finite-dimensional inner product space.
 We denote this product as ordinary multiplication, and the induced norm as $|\cdot|.$
 
 We now study a family of functions which is useful for later proofs.
 \begin{lemma}
 \label{lem:fourier-gaussian}
-\uses{def:fourier-transform, lem:fourier-prop}
+\uses{def:fourier-transform}
 \lean{fourierIntegral_gaussian_innerProductSpace'}
 \leanok
 Let $x\in V$ and $\delta>0$. Define the \emph{modulated Gaussian}
-$$u_{x,\delta}(y):V\to\C,\quad y\mapsto e^{-\pi|y|^2}e^{2\pi i x y}.$$
+$$u_{x,\delta}(y):V\to\C,\quad y\mapsto e^{-\delta\pi|y|^2}e^{2\pi i x y}.$$
 Its Fourier transform (w.r.t. the inner product) is given by
 $$\widehat{u_{x,\delta}}(z)=\delta^{-n/2}e^{-\pi|x-y|^2/\delta}=:K_\delta(x-z).$$
 \end{lemma}
 \begin{proof}
+  \uses{lem:fourier-prop}
   \leanok
   By choosing an orthonormal basis, wlog we may assume $V=\R^n$.
   First note $\widehat{u_{x,\delta}}(z-x)=\widehat{u_{0,\delta}}(z)$, so it is enough to consider $x=0$.
@@ -100,9 +121,8 @@ \section{Basic Properties of the Fourier Transform}
 
 \begin{lemma}
 \label{lem:weierstrass-kernel}
-% \uses{}
 % \lean{}
-% \leanok
+\leanok
 Let $K_\delta(v)=\delta^{-n/2}e^{-\pi|v|^2/\delta}$
 as in \Cref{lem:fourier-gaussian}. This is a
 \emph{good kernel}, called the \emph{Weierstrass kernel}, satisfying
@@ -113,7 +133,7 @@ \section{Basic Properties of the Fourier Transform}
 some constant $B$ independent of $\delta$.
 \end{lemma}
 \begin{proof}
-  % \leanok
+  \leanok
   By choosing an orthonormal basis, wlog we may assume $V=\R^n$. Then these are all straight-forward calculations:
   $$\int_{\R^n}e^{-\pi|x|^2/\delta}\,dx=\delta^{n/2}\int_{\R^n}e^{-\pi|x|^2}\,dx=\delta^{n/2}.$$
   $$\int_{|x|>\eta}\delta^{-n/2}e^{-\pi|x|^2/\delta}\,dx=\int_{|x|>\eta/\delta^{1/2}}e^{-\pi|x|^2}\xrightarrow{\delta\to0}0.$$
@@ -129,15 +149,15 @@ \section{Basic Properties of the Fourier Transform}
 \begin{theorem}
 \label{thm:kernel-approximation}
 \uses{lem:weierstrass-kernel}
-\lean{}
-% \leanok
+\lean{Real.tendsto_integral_gaussian_smul'}
+\leanok
 Let $f:V\to E$ be integrable. Let $K_\delta$ be the Weierstrass kernel from \Cref{lem:weierstrass-kernel},
 or indeed any family of functions satisfying the conditions of \Cref{lem:weierstrass-kernel}. Then
 $$(K_\delta\ast f)(x):=\int_V K_\delta(y)f(x-y)\,d\mu(y)\xrightarrow{\delta\to0}f(x)$$ in the $L^1$-norm.
 If $f$ is continuous, the convergence also holds pointwise.
 \end{theorem}
 \begin{proof}
-% \leanok
+\leanok
 Again we may assume $V=\R^n$. Consider the difference $$\Delta_\delta(x):=(K_\delta\ast f)(x)-f(x)=
 \int_{\R^n}(f(x-y)-f(x))K_\delta(y)\,dy.$$ We prove $L^1$-convergence first:
 Take $L^1$-norms and use Fubini's theorem to conclude
@@ -172,16 +192,16 @@ \section{Basic Properties of the Fourier Transform}
 
 \begin{theorem}[Inversion formula]
   \label{thm:fourier-inversion}
-  \uses{thm:kernel-approximation, lem:fourier-multiplication}
   \lean{MeasureTheory.Integrable.fourier_inversion, Continuous.fourier_inversion}
   Let $f:V\to E$ be integrable and continuous. Assume $\widehat f$ is integrable as well. Then
   $$\mathcal F^{-1}\mathcal F f=f.$$
   \leanok
 \end{theorem}
 \begin{proof}
-\leanok
-Apply the multiplication formula \Cref{lem:fourier-multiplication} to $u_{x,\delta}$ and $f$, and conclude with
-\Cref{thm:kernel-approximation}.
+  \uses{thm:kernel-approximation, lem:fourier-multiplication}
+  \leanok
+  Apply the multiplication formula \Cref{lem:fourier-multiplication} to $u_{x,\delta}$ and $f$, and conclude with
+  \Cref{thm:kernel-approximation}.
 \end{proof}
 
 \begin{remark}
@@ -191,33 +211,33 @@ \section{Basic Properties of the Fourier Transform}
 
 \begin{theorem}[Inversion formula, $L^1$-version]
   \label{thm:fourier-inversion-L1}
-  \uses{thm:kernel-approximation, lem:fourier-multiplication}
   \leanok
   Let $f\in L^1(V,E)$. If $\widehat f\in L^1(V,E)$, then $\mathcal F^{-1}\mathcal Ff=f$.
 \end{theorem}
+\begin{proof}
+  \leanok
+  \uses{thm:kernel-approximation, lem:fourier-multiplication}
+  Similar to \Cref{thm:fourier-inversion}.
+\end{proof}
 
 \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$}
                         {Plancherel's Theorem and the Fourier Transform on L2}}
-Again let $V$ be a finite-dimensional inner product space over $\R$ and let $E$ be a normed space over $\C$.
-%TODO: The proof needs convolutions of functions into E. Is there another proof? Or assume E has products?
+Let $(V,\cdot)$ be a finite-dimensional inner product space over $\R$ and let $(E,\langle\cdot,\cdot\rangle)$ be an inner product space over $\C$.
+
 \begin{theorem}[Plancherel's Theorem]
   \label{thm:plancherel}
-  \uses{thm:kernel-approximation, lem:fourier-multiplication, lem:fourier-gaussian, lem:fourier-prop}
-  \lean{MeasureTheory.memℒp_fourierIntegral, MeasureTheory.snorm_fourierIntegral} % the full Lean name this corresponds to (can be a comma-separated list)
-  \leanok % the *statement* of the lemma is formalized
+  \lean{MeasureTheory.memℒp_fourierIntegral, MeasureTheory.snorm_fourierIntegral}
+  \leanok
    Suppose that $f : V \to E$ is in $L^1(V,E)\cap L^2(V,E)$ and let $\widehat{f}$ be the Fourier transform of $f$. Then $\widehat{f},\check{f}\in L^2(V,E)$ and
   \[\|\widehat{f}\|_{L^2} = \|f\|_{L^2}=\|\check f\|_{L^2}.\]
    Suppose that $f : V \to E$ is in $L^1(V,E)\cap L^2(V,E)$ and let $\widehat{f}$ be the Fourier transform of $f$. Then $\widehat{f},\check{f}\in L^2(V,E)$ and
   \[\|\widehat{f}\|_{L^2} = \|f\|_{L^2}=\|\check f\|_{L^2}.\]
   \end{theorem}
     \begin{proof}
-    % \leanok % uncomment if the lemma has been proven
-    %Let $(e_i)_{i\in I}$ be a normalized basis of E. This choice defines a conjugation on $E$: Let $E_\R$ be
-    %the $\R$-span of the $e_i$, then $E\cong E_\R\otimes_\R\C$ and we can conjugate on the second factor.
-    %We denote this conjugation by $e\mapsto\overline e$.
-    Let $g(x)=\overline{f(-x)}$ and apply the multiplication formula \Cref{lem:fourier-multiplication}
+    \uses{thm:kernel-approximation, lem:fourier-multiplication, lem:fourier-gaussian, lem:fourier-prop}
+    Let $g(x)=f(-x)$ and apply the multiplication formula \Cref{lem:fourier-multiplication}
     to $f\ast g$ and $u_{0,\delta}$: $$\int_V\widehat{f\ast g}\cdot u_{0,\delta}(x)\,dx=\int_V(f\ast g)(x)K_\delta(-x)\,dx
-    \overset{\delta\to0}\to(f\ast g)(0)=\int_Vf(x)\overline{f(x)}\,dx=\| f\|_2^2$$ by \Cref{thm:kernel-approximation}.
+    \overset{\delta\to0}\to(f\ast g)(0)=\int_V \langle f(x),f(x)\rangle\,dx=\| f\|_2^2$$ by \Cref{thm:kernel-approximation}.
     On the other hand, by \Cref{lem:fourier-prop} the left hand side simplifies to
     $$\int_V|\widehat f(x)|^2e^{-\delta\pi|x|^2}\,dx\xrightarrow{\delta\to0}\|\widehat f\|_2^2$$ by dominated convergence.
 
@@ -228,9 +248,9 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$
 such that $f_n\xrightarrow[L^2]{}f$. Such sequences exist:
 \begin{lemma}
   \label{lem:L12-dense}
-  %\uses{MeasureTheory.Memℒp.exists_hasCompactSupport_snorm_sub_le}
+  %\uses{MeasureTheory.Memℒp.exists_hasCompactSupport_snorm_sub_le, Mathlib.MeasureTheory.Function.SimpleFuncDenseLp}
   \lean{}
-  % \leanok
+  %\leanok
   $L^1(V,E)\cap L^2(V,E)$ is dense in $L^2(V,E)$.
 \end{lemma}
 \begin{proof}
@@ -242,7 +262,7 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$
 Let $f\in L^2(V,E)$. Plancherel's theorem lets us now approximate a potential $\widehat f$:
 \begin{lemma}
   \label{lem:fourier12-cauchy}
-  \uses{lem:L12-dense, thm:plancherel, lem:fourier-prop}
+  \uses{lem:L12-dense,}
   \lean{}
   % \leanok
   Let $f\in L^2(V,E)$ and $(f_n)_n\subset L^1(V,E)\cap L^2(V,E)$ a sequence with $f_n\xrightarrow[L^2]{}f$. Then $(\widehat f_n)_n$ is a Cauchy sequence,
@@ -250,6 +270,7 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$
 \end{lemma}
 \begin{proof}
   % \leanok
+  \uses{thm:plancherel, lem:fourier-prop}
   $$\|\widehat f_n-\widehat f_m\|_2=\|\widehat{f_n-f_m}\|_2\overset{\text{Plancherel}}=\|f_n-f_m\|_2$$ goes to $0$ for $n,m$ large, as $(f_n)_n$ is
   convergent, hence Cauchy. Since $L^2(V,E)$ is complete, $(\widehat f_n)_n$ converges.
 \end{proof}
@@ -263,7 +284,7 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$
 \end{definition}
 \begin{lemma}
   \label{lem:fourier2-welldef}
-  \uses{def:fourier-L2, lem:fourier12-cauchy, thm:plancherel}
+  \uses{def:fourier-L2, lem:fourier12-cauchy}
   \lean{}
   % \leanok
   This is well-defined: By \Cref{lem:fourier12-cauchy}, the limit exists. Further it does not depend
@@ -272,6 +293,7 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$
 \end{lemma}
 \begin{proof}
   % \leanok
+  \uses{thm:plancherel}
   Let $(g_n)_n$ be another sequence approximating $f$. Then
   $$\|\widehat f_n-\widehat g_n\|_2=\|f_n-g_n\|\leq\|f_n-f\|+\|g_n-g\|\to0.$$
   If $f\in L^1(V,E)\cap L^2(V,E)$, we can choose the constant sequence $(f_n)_n=(f)_n$.
@@ -288,13 +310,14 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$
 
 \begin{corollary}
   \label{thm:fourier2-properties}
-  \uses{def:fourier-L2, def:invFourier-L2, thm:plancherel, thm:fourier-inversion, lem:fourier-prop}
+  \uses{def:fourier-L2, def:invFourier-L2, lem:fourier2-welldef}
   \lean{}
   % \leanok
   Plancherel's Theorem, the inversion formula, and the properties of \Cref{lem:fourier-prop} hold
   for the Fourier transform on $L^2(V,E)$ as well.
 \end{corollary}
 \begin{proof}
+  \uses{thm:plancherel, thm:fourier-inversion, lem:fourier-prop}
   % \leanok
   All of these follow immediately from the definition and the observation, that all operations (norms, sums, conjugation, $\ldots$) are continuous.
   For example, let $f\in L^2(V,E)$ and take an approximating sequence $(f_n)_n$ as before. Then
@@ -304,14 +327,14 @@ \section{\texorpdfstring{Plancherel's Theorem and the Fourier Transform on $L^2$
 
 \begin{corollary}
   \label{thm:fourier-is-l2-linear}
-  \uses{thm:fourier2-properties} % the (list of) LaTeX labels of the lemmas that are used for this result
-  \lean{MeasureTheory.fourierIntegralL2} % the full Lean name this corresponds to (can be a comma-separated list)
-  \leanok % the *statement* of the lemma is formalized
+  \uses{def:fourier-L2, lem:fourier2-welldef}
+  \lean{MeasureTheory.fourierIntegralL2}
+  \leanok
   The Fourier transform induces a continuous linear map $L^2(V,E) \to L^2(V,E)$.
   \end{corollary}
   \begin{proof}
-    % \uses{} % Put any results used in the proof but not in the statement here
+    \uses{thm:fourier2-properties}
     % \leanok % uncomment if the lemma has been proven
     This follows immediately from \Cref{thm:fourier2-properties}: Linearity from the $L^2$-version of
     \Cref{lem:fourier-prop}, and continuity and well-definedness from the $L^2$-version of Plancherel's theorem.
-\end{proof}
\ No newline at end of file
+\end{proof}