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}