Lean/Mathlib で量子力学のフーリエ変換：Schwartz 空間 S から L2 へ

!README.md

Lean/Mathlib で量子力学のフーリエ変換：Schwartz 空間 $\mathcal{S}$ から $L^2$ へ（Parseval/Plancherel）

この記事は 証明支援系 Advent Calendar 2025 23日目の記事（2本目）です。
（一本目の記事「有限次元のスペクトル分解」は こちら ）

このGistページは、量子力学で使うフーリエ変換まわりの Parseval / Plancherel（特に「Schwartz 空間 $\mathcal{S}$ から $L^2$ への橋渡し」）を、Lean/Mathlib 上で動く形にまとめたものです。

参考（Wikipedia、リンク）：

量子力学では波動関数を $L^2$ 空間で扱い、運動量表示はフーリエ変換で与えられる。

— Wikipedia「量子力学の数学的定式化」 より（該当節: L2空間上のフーリエ変換）

このページの内容

• Lean実装コード: plancherel4qm.lean
• 解説スライド: PDF
• 逐語説明（詳細）: plancherel4qm_explanation.md

なお、PDF 内のリンクは、Gist 上での閲覧では機能しません。ファイルとしてダウンロード（Raw ボタンでダウンロード開始）した上で開くと、リンクが有効になります。

本実装の狙い

大前提として、この資料がやりたいのは

• Schwartz 空間 $\mathcal{S}$ 上で得られる Plancherel（等長性）を、 $L^2$（Lp の p = 2）へ拡張すること
• その結果として、フーリエ変換を $L^2 \to L^2$ の（等長な）作用素として扱える形にすること

です。

Mathlib は、Schwartz 空間上のフーリエ変換を 𝓢(V,E) →L 𝓢(V,E)（fourierTransformCLM）および 𝓢(V,E) ≃L 𝓢(V,E)（fourierTransformCLE）として提供しています（Mathlib/Analysis/Distribution/FourierSchwartz.lean:10-15、Mathlib/Analysis/Distribution/FourierSchwartz.lean:29-109）。

ここで、→L は「連続線形写像」（ContinuousLinearMap）で、一般には逆写像があるとは限りません。一方、≃ₗᵢ は「等長線形同型」（LinearIsometryEquiv）で、全単射かつノルムを保つ（したがって等長）ことまで含みます。

一方で、少なくとも本環境（Mathlib: v4.24.0）では、 $\mathbb{R}^d$ 上の Real.fourierIntegral を $L^2(\mathbb{R}^d)$ の等長作用素としてまとめて提供する形（Lp 2 →L Lp 2 や Lp 2 ≃ₗᵢ Lp 2 としての“フーリエ変換”）は見当たりません。

そこで本実装では、Wikipedia などで量子力学の文脈としてよく見かける「 $L^2$ 上のフーリエ変換（位置表示 ↔ 運動量表示）」を、Lean/Mathlib の言葉で扱える形に寄せるため（Schwartz 空間 $\mathcal{S}$ 上に留まらず、 $L^2$ 上の作用素として扱える形にする）、次のルートを明示的に組み立てます：

• Schwartz 上の Parseval（積分形） を示す
• それを $L^2$ の内積（積分定義）に接続して Plancherel（ノルム保存）を得る
• さらに 稠密性と「稠密部分空間上の等長線形写像の一意延長」の一般論（ContinuousLinearMap.extend）で、 $L^2 \to L^2$ へ延長する

この結果、Wiki 風の式変形と Mathlib の定義・補題の対応が取りやすい形で、Lean 上に “実際に動く” $L^2$ のフーリエ作用素（本ファイルでは fourierL2CLM）を得ます。

なお、本稿のコーディングは GPT-5.2 × Cursor の方法 による AI 支援を用いています。

plancherel4qm.lean

import Mathlib.Analysis.Distribution.FourierSchwartz
import Mathlib.MeasureTheory.Function.L2Space
import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
import Mathlib.Analysis.Normed.Operator.Completeness
import Mathlib.Topology.Continuous
import MIL_copy.slides.quantum_mechanics_fourier_l2pmap2

/-!
# quantum_mechanics_plancherel_standalone

Schwartz 関数に対する Parseval（積分形）と、それを用いた $L^2$ ノルム保存（Plancherel）を、
Mathlib の `Real.fourierIntegral`（`2π` 正規化）に基づいてまとめた単一ファイル。

量子力学の「位置表示 ↔ 運動量表示」の橋渡しで必要となる
- `conj` と逆フーリエの関係
- Schwartz 上の Parseval（積分形）
- Schwartz → `Lp 2`（= $L^2$）への接続

をここで完結に提供する。
-/

namespace QuantumMechanicsStandalone

open scoped FourierTransform
open scoped ComplexConjugate
open scoped RealInnerProductSpace
open scoped ENNReal

open MeasureTheory

local notation "π" => Real.pi

/-- `ℝ^d`（実内積空間）を `EuclideanSpace ℝ (Fin d)` として表す。 -/
abbrev Rd (d : ℕ) : Type := EuclideanSpace ℝ (Fin d)

/-- `ℝ^d` 上の複素値 Schwartz 関数。 -/
abbrev SchwartzRd (d : ℕ) : Type := SchwartzMap (Rd d) ℂ

/-- `ℝ^d` 上の $L^2$（Mathlib の `Lp` による表現）。 -/
abbrev L2Rd (d : ℕ) : Type := MeasureTheory.Lp ℂ 2 (volume : Measure (Rd d))

namespace PlancherelTools

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]

/-- 共役は逆フーリエ（共役した関数）に一致する。

ここでの `𝓕` / `𝓕⁻` は Mathlib の `Real.fourierIntegral` / `Real.fourierIntegralInv`。
-/
theorem conj_fourierIntegral_eq_fourierIntegralInv_conj (f : V → ℂ) (w : V) :
    conj (𝓕 f w) = 𝓕⁻ (fun v : V => conj (f v)) w := by
  -- 指数を一貫した形 `-(2 * (π:ℂ) * (⟪v,w⟫_ℝ:ℂ) * I)` に揃えて計算する
  -- （import 追加により `⟪·,·⟫` が曖昧になり得るので、`𝕜 := ℝ` を明示して回避）
  let zneg : V → ℂ := fun v =>
    -(2 * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ) * Complex.I)
  let zpos : V → ℂ := fun v =>
    (2 * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ) * Complex.I)

  have hF : (𝓕 f w) = ∫ v : V, Complex.exp (zneg v) • f v := by
    simp [Real.fourierIntegral_eq', zneg, mul_left_comm, mul_comm]

  have hFinv :
      (𝓕⁻ (fun v : V => conj (f v)) w)
        = ∫ v : V, Complex.exp (zpos v) • conj (f v) := by
    simp [Real.fourierIntegralInv_eq', zpos, mul_left_comm, mul_comm]

  have hconj :
      conj (∫ v : V, Complex.exp (zneg v) • f v)
        = ∫ v : V, conj (Complex.exp (zneg v) • f v) := by
    simpa using
      (integral_conj (μ := (MeasureTheory.volume : MeasureTheory.Measure V))
        (f := fun v : V => (Complex.exp (zneg v) • f v))).symm

  have hkernel :
      (fun v : V => conj (Complex.exp (zneg v) • f v))
        = fun v : V => Complex.exp (zpos v) • conj (f v) := by
    funext v
    have hz : conj (zneg v) = zpos v := by
      dsimp [zneg, zpos]
      have h2 : conj (2 : ℂ) = (2 : ℂ) := by
        simpa using (Complex.conj_ofNat (n := 2))
      have hpi : conj (π : ℂ) = (π : ℂ) := by
        simpa using (Complex.conj_ofReal π)
      have hin : conj (((inner (𝕜 := ℝ) v w : ℝ) : ℂ)) = ((inner (𝕜 := ℝ) v w : ℝ) : ℂ) := by
        simpa using (Complex.conj_ofReal (inner (𝕜 := ℝ) v w))
      have hI : conj (Complex.I : ℂ) = -(Complex.I : ℂ) := by
        simpa using (Complex.conj_I)
      have hA :
          conj (2 * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ))
            = (2 * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ)) := by
        calc
          conj (2 * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ))
              = conj (2 * (π : ℂ)) * conj ((inner (𝕜 := ℝ) v w : ℝ) : ℂ) := by
                  simpa [mul_assoc] using
                    (map_mul (starRingEnd ℂ) (2 * (π : ℂ)) ((inner (𝕜 := ℝ) v w : ℝ) : ℂ))
          _ = (conj (2 : ℂ) * conj (π : ℂ)) * conj ((inner (𝕜 := ℝ) v w : ℝ) : ℂ) := by
                  simpa [mul_assoc] using
                    congrArg (fun t => t * conj ((inner (𝕜 := ℝ) v w : ℝ) : ℂ))
                    (map_mul (starRingEnd ℂ) (2 : ℂ) (π : ℂ))
          _ = (2 : ℂ) * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ) := by
                  simp [h2, hpi, hin, mul_assoc]
      calc
        conj (-(2 * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ) * Complex.I))
            = -conj (2 * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ) * Complex.I) := by simp
        _ = -(conj (2 * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ)) * conj (Complex.I)) := by
              simpa [mul_assoc] using congrArg (fun t => -t)
                (map_mul (starRingEnd ℂ)
                  (2 * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ)) (Complex.I : ℂ))
        _ = -((2 * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ)) * (-Complex.I)) := by
              simp [hA, hI]
        _ = (2 * (π : ℂ) * ((inner (𝕜 := ℝ) v w : ℝ) : ℂ) * Complex.I) := by
              simp [mul_assoc]
    calc
      conj (Complex.exp (zneg v) • f v)
          = conj (Complex.exp (zneg v) * f v) := by
              simp [smul_eq_mul]
      _ = conj (Complex.exp (zneg v)) * conj (f v) := by
              simp
      _ = Complex.exp (conj (zneg v)) * conj (f v) := by
              simpa using congrArg (fun t => t * conj (f v))
                (by simpa using (Complex.exp_conj (x := zneg v)).symm)
      _ = Complex.exp (zpos v) * conj (f v) := by
              simp [hz]
      _ = Complex.exp (zpos v) • conj (f v) := by
              simp [smul_eq_mul]

  calc
    conj (𝓕 f w)
        = conj (∫ v : V, Complex.exp (zneg v) • f v) := by
            simp [hF]
    _ = ∫ v : V, conj (Complex.exp (zneg v) • f v) := by
            simpa using hconj
    _ = ∫ v : V, Complex.exp (zpos v) • conj (f v) := by
            simpa using congrArg (fun g => (∫ v : V, g v)) hkernel
    _ = 𝓕⁻ (fun v : V => conj (f v)) w := by
            simp [hFinv]

end PlancherelTools

namespace FourierParsevalSchwartz

variable {d : ℕ}

/-- Schwartz 関数に対する Parseval（積分形）。 -/
theorem parseval_integral (d : ℕ) (ψ : SchwartzRd d) :
    (∫ x : Rd d, conj (𝓕 (fun y : Rd d => ψ y) x) * (𝓕 (fun y : Rd d => ψ y) x))
      =
    (∫ x : Rd d, conj (ψ x) * (ψ x)) := by
  classical

  let μ : Measure (Rd d) := (volume : Measure (Rd d))
  haveI : μ.HasTemperateGrowth := by infer_instance

  -- 本体関数と補助関数
  let f : Rd d → ℂ := fun x => ψ x
  let g : Rd d → ℂ := fun x => conj (𝓕 f x)

  have hf : Integrable f μ := by
    simpa [f] using (ψ.integrable (μ := μ))

  have hFf : Integrable (𝓕 f) μ := by
    let Fψ : SchwartzMap (Rd d) ℂ :=
      (SchwartzMap.fourierTransformCLM (𝕜 := ℂ) (V := Rd d) (E := ℂ)) ψ
    have : Integrable (fun x : Rd d => Fψ x) μ := by
      simpa using (Fψ.integrable (μ := μ))
    simpa [Fψ, SchwartzMap.fourierTransformCLM_apply, f] using this

  have hg : Integrable g μ := by
    let L : ℂ →L[ℝ] ℂ := Complex.conjCLE.toContinuousLinearMap
    simpa [g, L] using (ContinuousLinearMap.integrable_comp (μ := μ) L hFf)

  -- `𝓕 g = conj f`
  have hFg : (𝓕 g) = fun x : Rd d => conj (f x) := by
    have hg_eq : g = fun x : Rd d => 𝓕⁻ (fun y : Rd d => conj (f y)) x := by
      funext x
      simpa [g] using
        (PlancherelTools.conj_fourierIntegral_eq_fourierIntegralInv_conj
          (f := f) (w := x))

    have hconjf_cont : Continuous (fun x : Rd d => conj (f x)) := by
      simpa [f] using (Complex.continuous_conj.comp (ψ.continuous))

    have hconjf_int : Integrable (fun x : Rd d => conj (f x)) μ := by
      let L : ℂ →L[ℝ] ℂ := Complex.conjCLE.toContinuousLinearMap
      simpa [f, L] using (ContinuousLinearMap.integrable_comp (μ := μ) L hf)

    have hFconjf_int : Integrable (𝓕 (fun x : Rd d => conj (f x))) μ := by
      let finvSch : SchwartzMap (Rd d) ℂ :=
        (SchwartzMap.fourierTransformCLE (𝕜 := ℂ) (V := Rd d) (E := ℂ)).symm ψ
      have hfinv_int : Integrable (fun x : Rd d => finvSch x) μ := by
        simpa using (finvSch.integrable (μ := μ))
      have hfinv_eq : (fun x : Rd d => finvSch x) = fun x : Rd d => 𝓕⁻ f x := by
        funext x
        simp [finvSch, SchwartzMap.fourierTransformCLE_symm_apply, f]

      have hpoint : (𝓕 (fun y : Rd d => conj (f y)))
          = fun x : Rd d => conj (𝓕⁻ f x) := by
        funext x
        have hconj :
            conj (𝓕 (fun y : Rd d => conj (f y)) x)
              = 𝓕⁻ (fun y : Rd d => conj (conj (f y))) x := by
          simpa using
            (PlancherelTools.conj_fourierIntegral_eq_fourierIntegralInv_conj
              (f := fun y : Rd d => conj (f y)) (w := x))
        have := congrArg conj (by simpa [f] using hconj)
        simpa using this

      let L : ℂ →L[ℝ] ℂ := Complex.conjCLE.toContinuousLinearMap
      have hLfinv_int : Integrable (fun x : Rd d => L (finvSch x)) μ :=
        ContinuousLinearMap.integrable_comp (μ := μ) L hfinv_int

      have hconj_pt : ∀ x : Rd d, L (finvSch x) = conj (𝓕⁻ f x) := by
        intro x
        calc
          L (finvSch x) = conj (finvSch x) := by simp [L]
          _ = conj (𝓕⁻ f x) := by
                simpa using congrArg conj (by simpa using congrArg (fun h => h x) hfinv_eq)

      have hL_ae :
          (fun x : Rd d => L (finvSch x)) =ᶠ[ae μ] fun x : Rd d => conj (𝓕⁻ f x) := by
        filter_upwards [ae_of_all μ hconj_pt] with x hx
        simpa using hx

      have : Integrable (fun x : Rd d => conj (𝓕⁻ f x)) μ :=
        (MeasureTheory.integrable_congr (μ := μ) (f := fun x : Rd d => L (finvSch x))
          (g := fun x : Rd d => conj (𝓕⁻ f x)) hL_ae).1 hLfinv_int

      -- `hpoint` は `𝓕 (conj f) = conj (𝓕⁻ f)` の「等式（関数として）」なので、
      -- `Integrable` の目標を a.e. 同値で運ぶ（`simp` だと `conj`/`star` の揺れで壊れやすい）。
      have hpoint_ae :
          (fun x : Rd d => conj (𝓕⁻ f x)) =ᵐ[μ] (𝓕 fun y : Rd d => conj (f y)) := by
        refine (ae_of_all _ ?_)
        intro x
        simpa using (congrArg (fun g => g x) hpoint).symm
      exact (MeasureTheory.integrable_congr (μ := μ)
        (f := fun x : Rd d => conj (𝓕⁻ f x))
        (g := (𝓕 fun y : Rd d => conj (f y))) hpoint_ae).1 this

    have hinv : 𝓕 (fun x : Rd d => 𝓕⁻ (fun y : Rd d => conj (f y)) x)
        = (fun x : Rd d => conj (f x)) := by
      simpa using
        (Continuous.fourier_inversion_inv (V := Rd d) (E := ℂ)
          (f := fun x : Rd d => conj (f x)) hconjf_cont hconjf_int hFconjf_int)

    simpa [hg_eq] using hinv

  have hflip :
      (∫ x : Rd d, (𝓕 f x) • g x ∂μ) = ∫ x : Rd d, f x • (𝓕 g x) ∂μ := by
    have hLflip : (innerₗ (Rd d)).flip = innerₗ (Rd d) := by
      ext v w
      simp
    simpa [Real.fourierIntegral, VectorFourier.fourierIntegral, hLflip] using
      (VectorFourier.integral_fourierIntegral_smul_eq_flip (L := innerₗ (Rd d))
        Real.continuous_fourierChar continuous_inner hf hg)

  have hflip' :
      (∫ x : Rd d, (𝓕 f x) * conj (𝓕 f x) ∂μ) = ∫ x : Rd d, f x * conj (f x) ∂μ := by
    have hflip_mul :
        (∫ x : Rd d, (𝓕 f x) * g x ∂μ) = ∫ x : Rd d, f x * (𝓕 g x) ∂μ := by
      simpa [smul_eq_mul] using hflip
    have hFg_pt : ∀ x : Rd d, 𝓕 g x = conj (f x) := by
      intro x
      simpa using congrArg (fun h => h x) hFg
    have hflip_mul2 : (∫ x : Rd d, (𝓕 f x) * g x ∂μ) = ∫ x : Rd d, f x * conj (f x) ∂μ := by
      have hRint :
          (∫ x : Rd d, f x * (𝓕 g x) ∂μ) = ∫ x : Rd d, f x * conj (f x) ∂μ := by
        refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_)
        intro x
        simp [hFg_pt x]
      exact hflip_mul.trans hRint
    simpa [g] using hflip_mul2

  calc
    (∫ x : Rd d, conj (𝓕 f x) * (𝓕 f x) ∂μ)
        = ∫ x : Rd d, (𝓕 f x) * conj (𝓕 f x) ∂μ := by
            refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_)
            intro x
            simp [mul_comm]
    _ = ∫ x : Rd d, f x * conj (f x) ∂μ := hflip'
    _ = ∫ x : Rd d, conj (f x) * (f x) ∂μ := by
            refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_)
            intro x
            simp [mul_comm]
    _ = (∫ x : Rd d, conj (ψ x) * (ψ x) ∂μ) := by
          simp [f]

end FourierParsevalSchwartz

namespace FourierL2

/-- Schwartz を $L^2$（`Lp 2`）へ送る線形写像。 -/
noncomputable def schwartzToL2LM (d : ℕ) : SchwartzRd d →ₗ[ℂ] L2Rd d := by
  classical
  haveI : Fact ((1 : ℝ≥0∞) ≤ (2 : ℝ≥0∞)) := by infer_instance
  haveI : (volume : Measure (Rd d)).HasTemperateGrowth := by infer_instance
  exact (SchwartzMap.toLpCLM ℂ ℂ (2 : ℝ≥0∞) (volume : Measure (Rd d))).toLinearMap

/-- Schwartz 上のフーリエ変換（Schwartz→Schwartz）。 -/
noncomputable def fourierSchwartzLM (d : ℕ) : SchwartzRd d →ₗ[ℂ] SchwartzRd d := by
  classical
  exact (SchwartzMap.fourierTransformCLM (𝕜 := ℂ) (V := Rd d) (E := ℂ)).toLinearMap

/-- Schwartz を $L^2$ に落としてからフーリエしたもの。 -/
noncomputable def fourierToL2LM (d : ℕ) : SchwartzRd d →ₗ[ℂ] L2Rd d :=
  (schwartzToL2LM (d := d)).comp (fourierSchwartzLM (d := d))

set_option maxHeartbeats 400000

/-- Schwartz 関数の `L²` ノルムはフーリエ変換で保存される（Plancherel）。

本ファイル内の `FourierParsevalSchwartz.parseval_integral` を
`Lp E 2 μ` の内積定義（`MeasureTheory.L2.inner_def`）に接続して示す。
-/
theorem plancherel_schwartz_toL2 (d : ℕ) (ψ : SchwartzRd d) :
    ‖fourierToL2LM (d := d) ψ‖ = ‖schwartzToL2LM (d := d) ψ‖ := by
  classical
  haveI : Fact ((1 : ℝ≥0∞) ≤ (2 : ℝ≥0∞)) := by infer_instance
  haveI : (volume : Measure (Rd d)).HasTemperateGrowth := by infer_instance

  let X : L2Rd d := (schwartzToL2LM (d := d)) ψ
  let Y : L2Rd d := (fourierToL2LM (d := d)) ψ
  -- 以降は `X`,`Y` のノルム等式として示す
  change ‖Y‖ = ‖X‖

  have hX_toLp : X = (ψ.toLp (2 : ℝ≥0∞) (volume : Measure (Rd d))) := by
    dsimp [X, schwartzToL2LM]
    exact (SchwartzMap.toLpCLM_apply (𝕜 := ℂ) (F := ℂ) (p := (2 : ℝ≥0∞))
      (μ := (volume : Measure (Rd d))) (f := ψ))

  have hY_toLp :
      Y = (((fourierSchwartzLM (d := d)) ψ).toLp (2 : ℝ≥0∞) (volume : Measure (Rd d))) := by
    -- `fourierToL2LM = schwartzToL2LM ∘ fourierSchwartzLM`
    dsimp [Y, fourierToL2LM, LinearMap.comp_apply]
    -- `schwartzToL2LM_apply`
    dsimp [schwartzToL2LM]
    exact (SchwartzMap.toLpCLM_apply (𝕜 := ℂ) (F := ℂ) (p := (2 : ℝ≥0∞))
      (μ := (volume : Measure (Rd d))) (f := ((fourierSchwartzLM (d := d)) ψ)))

  have hX_ae :
      (fun x : Rd d => (X x)) =ᵐ[(volume : Measure (Rd d))] fun x : Rd d => ψ x := by
    simpa [hX_toLp] using
      (SchwartzMap.coeFn_toLp (f := ψ) (p := (2 : ℝ≥0∞)) (μ := (volume : Measure (Rd d))))

  have hF : (fun x : Rd d => ((fourierSchwartzLM (d := d)) ψ) x)
      = fun x : Rd d => (𝓕 (fun y : Rd d => ψ y) x) := by
    funext x
    change
        ((SchwartzMap.fourierTransformCLM (𝕜 := ℂ) (V := Rd d) (E := ℂ)) ψ) x
          = (𝓕 (fun y : Rd d => ψ y) x)
    simp [SchwartzMap.fourierTransformCLM_apply]

  have hY_ae :
      (fun x : Rd d => (Y x)) =ᵐ[(volume : Measure (Rd d))]
        fun x : Rd d => (𝓕 (fun y : Rd d => ψ y) x) := by
    have h1 :
        (fun x : Rd d =>
            ((((fourierSchwartzLM (d := d)) ψ).toLp (2 : ℝ≥0∞) (volume : Measure (Rd d))) x))
          =ᵐ[(volume : Measure (Rd d))] fun x : Rd d => ((fourierSchwartzLM (d := d)) ψ) x :=
      SchwartzMap.coeFn_toLp (f := ((fourierSchwartzLM (d := d)) ψ)) (p := (2 : ℝ≥0∞))
        (μ := (volume : Measure (Rd d)))
    simpa [hY_toLp, hF] using h1

  have hinner : inner (𝕜 := ℂ) Y Y = inner (𝕜 := ℂ) X X := by
    have hY_inner :
        inner (𝕜 := ℂ) Y Y =
          ∫ x : Rd d, (𝓕 (fun y : Rd d => ψ y) x) * conj (𝓕 (fun y : Rd d => ψ y) x)
            ∂(volume : Measure (Rd d)) := by
      have hYint :
          (fun x : Rd d => inner (𝕜 := ℂ) (Y x) (Y x))
            =ᵐ[(volume : Measure (Rd d))] fun x : Rd d =>
              inner (𝕜 := ℂ) (𝓕 (fun y : Rd d => ψ y) x) (𝓕 (fun y : Rd d => ψ y) x) := by
        filter_upwards [hY_ae] with x hx
        simp [hx]
      have hYint' :
          (fun x : Rd d =>
              inner (𝕜 := ℂ) (𝓕 (fun y : Rd d => ψ y) x) (𝓕 (fun y : Rd d => ψ y) x))
            = fun x : Rd d => (𝓕 (fun y : Rd d => ψ y) x) * conj (𝓕 (fun y : Rd d => ψ y) x) := by
        funext x; simp
      calc
        inner (𝕜 := ℂ) Y Y
            = ∫ x : Rd d, inner (𝕜 := ℂ) (Y x) (Y x) ∂(volume : Measure (Rd d)) := by
                simp [MeasureTheory.L2.inner_def]
        _ = ∫ x : Rd d,
              inner (𝕜 := ℂ) (𝓕 (fun y : Rd d => ψ y) x) (𝓕 (fun y : Rd d => ψ y) x)
              ∂(volume : Measure (Rd d)) := by
                exact integral_congr_ae hYint
        _ = ∫ x : Rd d, (𝓕 (fun y : Rd d => ψ y) x) * conj (𝓕 (fun y : Rd d => ψ y) x)
              ∂(volume : Measure (Rd d)) := by
                simp

    have hX_inner :
        inner (𝕜 := ℂ) X X =
          ∫ x : Rd d, (ψ x) * conj (ψ x) ∂(volume : Measure (Rd d)) := by
      have hXint :
          (fun x : Rd d => inner (𝕜 := ℂ) (X x) (X x))
            =ᵐ[(volume : Measure (Rd d))] fun x : Rd d => inner (𝕜 := ℂ) (ψ x) (ψ x) := by
        filter_upwards [hX_ae] with x hx
        simp [hx]
      have hXint' :
          (fun x : Rd d => inner (𝕜 := ℂ) (ψ x) (ψ x))
            = fun x : Rd d => (ψ x) * conj (ψ x) := by
        funext x; simp
      calc
        inner (𝕜 := ℂ) X X
            = ∫ x : Rd d, inner (𝕜 := ℂ) (X x) (X x) ∂(volume : Measure (Rd d)) := by
                simp [MeasureTheory.L2.inner_def]
        _ = ∫ x : Rd d, inner (𝕜 := ℂ) (ψ x) (ψ x) ∂(volume : Measure (Rd d)) := by
                exact integral_congr_ae hXint
        _ = ∫ x : Rd d, (ψ x) * conj (ψ x) ∂(volume : Measure (Rd d)) := by
                simp

    have hParseval0 :=
      FourierParsevalSchwartz.parseval_integral (d := d) ψ

    have hParseval :
        (∫ x : Rd d, (𝓕 (fun y : Rd d => ψ y) x) * conj (𝓕 (fun y : Rd d => ψ y) x)
            ∂(volume : Measure (Rd d)))
          =
        (∫ x : Rd d, (ψ x) * conj (ψ x) ∂(volume : Measure (Rd d))) := by
      have hL :
          (∫ x : Rd d, conj (𝓕 (fun y : Rd d => ψ y) x) * (𝓕 (fun y : Rd d => ψ y) x)
              ∂(volume : Measure (Rd d)))
            =
          (∫ x : Rd d, (𝓕 (fun y : Rd d => ψ y) x) * conj (𝓕 (fun y : Rd d => ψ y) x)
              ∂(volume : Measure (Rd d))) := by
        refine integral_congr_ae (Filter.Eventually.of_forall ?_)
        intro x
        simp [mul_comm]
      have hR :
          (∫ x : Rd d, conj (ψ x) * (ψ x) ∂(volume : Measure (Rd d)))
            =
          (∫ x : Rd d, (ψ x) * conj (ψ x) ∂(volume : Measure (Rd d))) := by
        refine integral_congr_ae (Filter.Eventually.of_forall ?_)
        intro x
        simp [mul_comm]
      exact hL ▸ (hParseval0.trans hR)

    simpa [hY_inner, hX_inner] using congrArg id hParseval

  have hsqC : (‖Y‖ : ℂ) ^ 2 = (‖X‖ : ℂ) ^ 2 := by
    have hy : inner (𝕜 := ℂ) Y Y = (‖Y‖ : ℂ) ^ 2 := by
      simpa using (inner_self_eq_norm_sq_to_K (𝕜 := ℂ) (x := Y))
    have hx : inner (𝕜 := ℂ) X X = (‖X‖ : ℂ) ^ 2 := by
      simpa using (inner_self_eq_norm_sq_to_K (𝕜 := ℂ) (x := X))
    calc
      (‖Y‖ : ℂ) ^ 2 = inner (𝕜 := ℂ) Y Y := by
        simpa using hy.symm
      _ = inner (𝕜 := ℂ) X X := hinner
      _ = (‖X‖ : ℂ) ^ 2 := by
        simpa using hx

  have hsqR : ‖Y‖ ^ 2 = ‖X‖ ^ 2 := by
    have hsqC' : (Complex.ofReal (‖Y‖ ^ 2)) = Complex.ofReal (‖X‖ ^ 2) := by
      simpa using hsqC
    exact Complex.ofReal_inj.mp hsqC'

  have hmul : ‖Y‖ * ‖Y‖ = ‖X‖ * ‖X‖ := by
    simpa [pow_two] using hsqR

  rcases mul_self_eq_mul_self_iff.mp hmul with h | h
  · exact h
  ·
    have hY_nonneg : 0 ≤ ‖Y‖ := norm_nonneg _
    have hX_nonneg : 0 ≤ ‖X‖ := norm_nonneg _
    have hX_le0 : ‖X‖ ≤ 0 := by
      have : 0 ≤ -‖X‖ := by simpa [h] using hY_nonneg
      exact neg_nonneg.mp this
    have hX0 : ‖X‖ = 0 := le_antisymm hX_le0 hX_nonneg
    have hY0 : ‖Y‖ = 0 := by
      calc
        ‖Y‖ = -‖X‖ := h
        _ = -0 := by simp [hX0]
        _ = 0 := by simp
    -- 両辺とも 0
    calc
      ‖Y‖ = 0 := hY0
      _ = ‖X‖ := by simp [hX0]

/-!
## ここから: `L²` 全域への延長（稠密延長）

Wikipedia では `S′`（緩増加超関数）を経由する定義も説明されますが、
ここでは **Hilbert 空間の一般論**として、

- `S := range(schwartzToL2LM)`（`L²` の稠密部分空間）上で等長（Plancherel）
- `ContinuousLinearMap.extend` で `L² →L L²` に一意延長

というルートを採用します。
-/

theorem schwartzToL2LM_injective (d : ℕ) : Function.Injective (schwartzToL2LM (d := d)) := by
  classical
  intro f g h
  let μ : Measure (Rd d) := (volume : Measure (Rd d))
  haveI : μ.HasTemperateGrowth := by infer_instance
  haveI : μ.IsOpenPosMeasure := by infer_instance
  have htoLp : f.toLp (2 : ℝ≥0∞) μ = g.toLp (2 : ℝ≥0∞) μ := by
    simpa [schwartzToL2LM, SchwartzMap.toLpCLM_apply] using h
  exact (SchwartzMap.injective_toLp (E := Rd d) (F := ℂ) (p := (2 : ℝ≥0∞)) (μ := μ)) htoLp

/-- `S = range(schwartzToL2LM)` を `L²` の部分空間として見る。 -/
noncomputable abbrev SchwartzRangeL2 (d : ℕ) : Submodule ℂ (L2Rd d) :=
  LinearMap.range (schwartzToL2LM (d := d))

/-- Schwartz と `range(schwartzToL2LM)` の同型（単射なので `ofInjective` を使う）。 -/
noncomputable def schwartzEquivRange (d : ℕ) :
    SchwartzRd d ≃ₗ[ℂ] ↥(SchwartzRangeL2 (d := d)) :=
  LinearEquiv.ofInjective (schwartzToL2LM (d := d)) (schwartzToL2LM_injective (d := d))

/-- `SchwartzRangeL2` 上の「フーリエ」線形写像（`LinearMap`）。 -/
noncomputable def fourierOnSchwartzRangeLM (d : ℕ) :
    SchwartzRangeL2 (d := d) →ₗ[ℂ] L2Rd d :=
  (fourierToL2LM (d := d)).comp (schwartzEquivRange (d := d)).symm.toLinearMap

/-- `fourierOnSchwartzRangeLM` が等長（ノルム保存）である、という形にまとめた仮定。 -/
structure PlancherelOnSchwartzRange (d : ℕ) : Prop where
  norm_map : ∀ s : SchwartzRangeL2 (d := d),
    ‖fourierOnSchwartzRangeLM (d := d) s‖ = ‖s‖

/-- `plancherel_schwartz_toL2` から `SchwartzRangeL2` 上の等長性を作る。 -/
noncomputable def plancherelOnSchwartzRange (d : ℕ) : PlancherelOnSchwartzRange (d := d) := by
  classical
  refine ⟨?_⟩
  intro s
  -- 代表元を Schwartz に引き戻す
  let ψ : SchwartzRd d := (schwartzEquivRange (d := d)).symm s
  have hs : schwartzToL2LM (d := d) ψ = (s : L2Rd d) := by
    have : (schwartzEquivRange (d := d) ψ) = s := by
      simpa [ψ] using (LinearEquiv.apply_symm_apply (schwartzEquivRange (d := d)) s)
    simpa [schwartzEquivRange] using congrArg Subtype.val this
  have hFourier : fourierOnSchwartzRangeLM (d := d) s = fourierToL2LM (d := d) ψ := by
    rfl
  calc
    ‖fourierOnSchwartzRangeLM (d := d) s‖
        = ‖fourierToL2LM (d := d) ψ‖ := by
            simp [hFourier]
    _ = ‖schwartzToL2LM (d := d) ψ‖ := plancherel_schwartz_toL2 (d := d) ψ
    _ = ‖(s : L2Rd d)‖ := by
            simp [hs]
    _ = ‖s‖ := by
            rfl

/-- `SchwartzRangeL2` 上の等長線形写像を `→ₗᵢ` として束ねる。 -/
noncomputable def fourierOnSchwartzRangeLI (d : ℕ) :
    SchwartzRangeL2 (d := d) →ₗᵢ[ℂ] L2Rd d where
  toLinearMap := fourierOnSchwartzRangeLM (d := d)
  norm_map' := (plancherelOnSchwartzRange (d := d)).norm_map

/-- `SchwartzRangeL2`（= `range(schwartzToL2LM)`）が `L²` で稠密。 -/
theorem dense_schwartzRangeL2 (d : ℕ) :
    Dense ((SchwartzRangeL2 (d := d) : Submodule ℂ (L2Rd d)) : Set (L2Rd d)) := by
  classical
  -- 既にリポジトリ側で（公理なしで）証明済みの稠密性を再利用する。
  simpa [SchwartzRangeL2, schwartzToL2LM, QuantumMechanics.FourierL2.schwartzToL2LM] using
    (QuantumMechanics.FourierL2.dense_range_schwartzToL2LM (d := d))

/-- `S ↪ L²`（`subtypeL`）は稠密埋め込み（`S` が稠密なら）。 -/
theorem denseRange_subtypeL_schwartzRangeL2 (d : ℕ) :
    DenseRange ((SchwartzRangeL2 (d := d)).subtypeL) := by
  simpa using (dense_schwartzRangeL2 (d := d)).denseRange_val

/-- `L² →L L²` 上のフーリエ作用素（稠密延長）。 -/
noncomputable def fourierL2CLM (d : ℕ) : L2Rd d →L[ℂ] L2Rd d := by
  let S : Submodule ℂ (L2Rd d) := SchwartzRangeL2 (d := d)
  have hDense : DenseRange (S.subtypeL) := denseRange_subtypeL_schwartzRangeL2 (d := d)
  have hIso : Isometry (⇑S.subtypeL) := by
    intro x y
    rfl
  have h_e : IsUniformInducing (⇑S.subtypeL) := Isometry.isUniformInducing hIso
  -- `S →ₗᵢ L²` を `S →L L²` に束ね、稠密埋め込み `S ↪ L²` 沿いに延長
  exact
    ContinuousLinearMap.extend
      (f := (fourierOnSchwartzRangeLI (d := d)).toContinuousLinearMap)
      (e := S.subtypeL)
      (h_dense := hDense)
      (h_e := h_e)

/-- 延長は `SchwartzRangeL2` 上で元の写像と一致する。 -/
theorem fourierL2CLM_apply_subtype (d : ℕ) (s : SchwartzRangeL2 (d := d)) :
    fourierL2CLM (d := d) (s : L2Rd d) = fourierOnSchwartzRangeLM (d := d) s := by
  classical
  let S : Submodule ℂ (L2Rd d) := SchwartzRangeL2 (d := d)
  let f0 : S →L[ℂ] L2Rd d := (fourierOnSchwartzRangeLI (d := d)).toContinuousLinearMap
  have hDense : DenseRange (S.subtypeL) := denseRange_subtypeL_schwartzRangeL2 (d := d)
  have hIso : Isometry (⇑S.subtypeL) := by
    intro x y
    rfl
  have h_e : IsUniformInducing (⇑S.subtypeL) := Isometry.isUniformInducing hIso
  simpa [fourierL2CLM, S, f0, hDense, h_e] using
    (ContinuousLinearMap.extend_eq (f := f0) (e := S.subtypeL) (h_dense := hDense) (h_e := h_e) s)

end FourierL2

end QuantumMechanicsStandalone

plancherel4qm_explanation.md

plancherel4qm.lean の詳細解説

本稿では、plancherel4qm.lean のコードを、Mathlib、Lean Reference Manual、Lean By Example のドキュメントを参照しながら詳細に解説します。

ファイルの目的

このファイルは、量子力学における「位置表示 ↔ 運動量表示」の橋渡しに必要な数学的基礎を、Mathlib の Real.fourierIntegral（2π 正規化）に基づいて単一ファイルで完結に提供します。

免責事項

本内容は、AI（Cursorが提供するautoモデルのエージェント）による完全な自動レビュー・解説生成により作成されています。内容の正確性についてはDoc資料を引用することでできるだけ誤記を避けるようにしていますが、完全ではありません。おかしいと思う記述や不明点があった場合は、読者自身でAIに深掘り説明をさせたり、Mathlib のドキュメントなどを参照して確認することを推奨します。

背景: 何を "橋渡し" したいのか

量子力学では波動関数を $L^2(\mathbb{R}^d)$ で扱い、運動量表示はフーリエ変換で与えられます。ここで（正規化込みで）次の型の写像を考えます：

$$\mathcal{F}: \psi(x) \mapsto \widehat{\psi}(\xi)$$

（Mathlib では $2\pi$ 正規化つきの Real.fourierIntegral / Real.fourierIntegralInv を使います。）

典型的な主張は Plancherel 定理です：

$$|\mathcal{F}\psi|_{L^2} = |\psi|_{L^2}\quad (\text{Plancherel})$$

本実装では、まず稠密で扱いやすいシュワルツ関数で等式を示し、次に $L^2$ の内積（積分定義）に接続します。

流れ

$$\mathcal{S}(\mathbb{R}^d)\ \subset\ L^2(\mathbb{R}^d)\quad \text{（稠密）}$$

$$\text{Parseval on }\mathcal{S}\ \Rightarrow\ \text{Plancherel on }\mathcal{S}\ \Rightarrow\ \text{延長して }L^2\text{ 全域へ}$$

提供する3つの要素

1. 共役と逆フーリエの関係: $\overline{\mathcal{F}f}(w) = \mathcal{F}^{-1}(\overline{f})(w)$
2. シュワルツ上の Parseval（積分形）: $\int \overline{\mathcal{F}\psi(x)},\mathcal{F}\psi(x),dx = \int \overline{\psi(x)},\psi(x),dx$
3. シュワルツ → L² への接続と L² 全域への延長: シュワルツ関数の L² ノルムがフーリエ変換で保存される（Plancherel 定理）と、それを L² 空間全体に延長する方法

1. インポートと基本定義（L1-51）

インポート

import Mathlib.Analysis.Distribution.FourierSchwartz
import Mathlib.MeasureTheory.Function.L2Space
import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
import Mathlib.Analysis.Normed.Operator.Completeness
import Mathlib.Topology.Continuous
import MIL_copy.slides.quantum_mechanics_fourier_l2pmap2

• Mathlib.Analysis.Distribution.FourierSchwartz: シュワルツ空間上のフーリエ変換を提供します。SchwartzMap.fourierTransformCLM と SchwartzMap.fourierTransformCLE が定義されています。
• Mathlib.MeasureTheory.Function.L2Space: L² 空間（Lp）の定義と内積（MeasureTheory.L2.inner_def）を提供します。
• Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap: 連続線形写像の積分に関する補題（integral_conj など）を提供します。
• Mathlib.Analysis.Normed.Operator.Completeness: 稠密延長のための ContinuousLinearMap.extend を提供します。

名前空間と記法の有効化

namespace QuantumMechanicsStandalone

open scoped FourierTransform
open scoped ComplexConjugate
open scoped RealInnerProductSpace
open scoped ENNReal

open MeasureTheory

local notation "π" => Real.pi

• open scoped: 特定の名前空間にある scoped が付けられた記法のみを有効化します。
  • FourierTransform: フーリエ変換の記法 𝓕 と 𝓕⁻ を有効化
  • ComplexConjugate: 複素共役の記法を有効化
  • RealInnerProductSpace: 実内積空間の記法を有効化
  • ENNReal: 拡張実数（$\mathbb{R}_{\geq 0} \cup {\infty}$）の記法を有効化
• open MeasureTheory: MeasureTheory 名前空間を開き、Lp、volume などを直接使用できるようにします。
• local: notation "π" => Real.pi により、局所的に π を Real.pi の略記として定義します。

基本定義

abbrev Rd (d : ℕ) : Type := EuclideanSpace ℝ (Fin d)
abbrev SchwartzRd (d : ℕ) : Type := SchwartzMap (Rd d) ℂ
abbrev L2Rd (d : ℕ) : Type := MeasureTheory.Lp ℂ 2 (volume : Measure (Rd d))

• Rd d: $\mathbb{R}^d$ を EuclideanSpace ℝ (Fin d) として表します。これは有限次元実内積空間です。
• SchwartzRd d: $\mathbb{R}^d$ 上の複素値シュワルツ関数の空間 $\mathcal{S}(\mathbb{R}^d)$ です。SchwartzMap は、滑らかで任意の多項式より速く減衰する関数の空間です。
• L2Rd d: $\mathbb{R}^d$ 上の $L^2$ 空間（Mathlib の Lp による表現）です。$L^2$ のノルムと内積は以下の形（測度論的定義）として扱います：

$$|\psi|_{L^2}^2 = \int \overline{\psi(x)},\psi(x),dx,\qquad \langle f,g\rangle = \int \overline{f(x)},g(x),dx$$

2. PlancherelTools 名前空間（L53-150）

namespace PlancherelTools

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]

• variable: この名前空間全体で使用する変数と型クラスインスタンスを宣言します。V は有限次元の実内積空間で、測度空間の構造も持ちます。

2.1. 共役と逆フーリエの関係（L58-149）

定理: conj_fourierIntegral_eq_fourierIntegralInv_conj

theorem conj_fourierIntegral_eq_fourierIntegralInv_conj (f : V → ℂ) (w : V) :
    conj (𝓕 f w) = 𝓕⁻ (fun v : V => conj (f v)) w

この定理は、フーリエ変換の共役が、共役した関数の逆フーリエ変換に一致することを示します：

$$\overline{\mathcal{F}f}(w) = \mathcal{F}^{-1}(\overline{f})(w)$$

これは、量子力学における位置表示と運動量表示の関係において重要な役割を果たします。この型の補題があると、後段で

$$\overline{\widehat{\psi}(\xi)},\widehat{\psi}(\xi)$$

の形を「逆変換」に寄せて積分形 Parseval に繋げやすくなります。

共役と逆フーリエの関係の証明の流れ

1. フーリエ変換の定義式への展開（L66-77）:

   • フーリエ変換を積分表示に展開します：

   $$\mathcal{F}f(w) = \int_v e^{-2\pi i \langle v, w \rangle} f(v) , dv$$

   ここで zneg v = -(2 * π * ⟪v, w⟫ * I) は指数部分 $e^{-2\pi i \langle v, w \rangle}$ に対応します。コードでは simp タクティクと Real.fourierIntegral_eq' を使用して展開します。

   • 逆フーリエ変換も同様に展開します：

   $$\mathcal{F}^{-1}(\overline{f})(w) = \int_v e^{2\pi i \langle v, w \rangle} \overline{f(v)} , dv$$

   ここで zpos v = (2 * π * ⟪v, w⟫ * I) は指数部分 $e^{2\pi i \langle v, w \rangle}$ に対応します。コードでは simp タクティクと Real.fourierIntegralInv_eq' を使用して展開します。

2. 積分の共役（L79-84）:

   • integral_conj を使用して、積分の共役が共役の積分に等しいことを示します。コードでは simpa タクティクを使用します：

   $$\overline{\int g(x) , dx} = \int \overline{g(x)} , dx$$

   これは、積分が線形写像であり、共役も線形写像であることから導かれます。

3. 指数関数の共役（L86-137）:

   • Complex.exp_conj を使用して、指数関数の共役に関する等式を示します：

   $$\overline{e^z} = e^{\overline{z}}$$

   • conj (zneg v) = zpos v を証明します。コードでは funext タクティクで関数の等式を点ごとの等式に分解し、実数値（$2$, $\pi$, $\langle v, w \rangle$）の共役は自分自身であり、$i$ の共役は $-i$ であることから導かれます：

   $$\overline{-2\pi i \langle v, w \rangle} = 2\pi i \langle v, w \rangle$$

4. 最終的な等式（L139-148）:

   • calc タクティクを使用して、段階的に式変形を行います。

3. FourierParsevalSchwartz 名前空間（L152-299）

namespace FourierParsevalSchwartz

variable {d : ℕ}

• variable {d : ℕ}: この名前空間全体で次元 d を暗黙引数として使用します。

3.1. Parseval（積分形）（L157-298）

定理: parseval_integral

theorem parseval_integral (d : ℕ) (ψ : SchwartzRd d) :
    (∫ x : Rd d, conj (𝓕 (fun y : Rd d => ψ y) x) * (𝓕 (fun y : Rd d => ψ y) x))
      =
    (∫ x : Rd d, conj (ψ x) * (ψ x))

この定理は、シュワルツ関数に対する Parseval の等式（積分形）を示します：

$$\int \overline{\mathcal{F}\psi(x)},\mathcal{F}\psi(x),dx = \int \overline{\psi(x)},\psi(x),dx$$

これは、フーリエ変換が L² ノルムを保存する Plancherel 定理の基礎となります。後段の $L^2$ 内積（積分で定義）へそのまま接続できる形にしているため、つまり

$$\langle \mathcal{F}\psi,\mathcal{F}\psi\rangle_{L^2}=\langle \psi,\psi\rangle_{L^2}$$

という等式が（シュワルツ上で）積分形で直接得られます。

証明の開始（L150）:

• classical により、古典論理を有効化します。これは、すべての命題が決定可能（Decidable）であることを仮定し、選択公理（Classical.choice）を使用できるようにします。classical を使用した証明は noncomputable としてマークする必要がありますが、この定理は既に theorem として宣言されているため、自動的に非計算可能として扱われます。

Parseval（積分形）の証明の流れ

1. 可積分性の確認（L170-182）:

   • ψ.integrable により f が可積分であることを確認します。シュワルツ関数は可積分です（Mathlib/Analysis/Distribution/SchwartzSpace.lean）。
   • SchwartzMap.fourierTransformCLM により 𝓕 f もシュワルツ関数なので可積分です。
   • Complex.conjCLE（複素共役の連続線形写像）により g = conj (𝓕 f) も可積分です。

   have hf_integrable : Integrable (fun y : Rd d => ψ y) := ψ.integrable
   have hFf_integrable : Integrable (𝓕 (fun y : Rd d => ψ y)) := by
     -- SchwartzMap.fourierTransformCLM により 𝓕 f もシュワルツ関数
   have hg_integrable : Integrable (fun x : Rd d => conj (𝓕 (fun y : Rd d => ψ y) x)) := by
     -- Complex.conjCLE により可積分

2. 𝓕 g = conj f の証明（L185-257）:

   この証明は複数のステップから構成されます：

   a. g = 𝓕⁻ (conj f) の証明（L186-190）:

   • PlancherelTools.conj_fourierIntegral_eq_fourierIntegralInv_conj を使用して、各点で次が成り立つことを示します：

   $$g(x) = \overline{\mathcal{F}f(x)} = \mathcal{F}^{-1}(\overline{f})(x)$$

   have hg_eq : (fun x : Rd d => conj (𝓕 (fun y : Rd d => ψ y) x)) =
                (fun x : Rd d => 𝓕⁻ (fun y : Rd d => conj (ψ y)) x) := by
     ext x
     exact PlancherelTools.conj_fourierIntegral_eq_fourierIntegralInv_conj _ _

   b. 可積分性の確認（L192-249）:

   • conj f が連続かつ可積分であることを確認します。
   • 𝓕 (conj f) の可積分性を、シュワルツ関数の逆フーリエ変換がシュワルツ関数であることを利用して示します。
   • ここで重要な補題は、𝓕 (conj f) = conj (𝓕⁻ f) です（L208-218）。これは、共役と逆フーリエの関係を再帰的に適用することで得られます。

   c. フーリエ逆変換の適用（L251-257）:

   • Continuous.fourier_inversion_inv を使用して、フーリエ変換と逆変換の関係を適用します：

   $$\mathcal{F}(\mathcal{F}^{-1}(\overline{f})) = \overline{f}$$

   これにより、最終的に $\mathcal{F}g = \overline{f}$ が得られます。

3. 自己随伴性の利用（L259-266）:

   • VectorFourier.integral_fourierIntegral_smul_eq_flip を使用して、フーリエ変換の自己随伴性を示します：

   $$\int \mathcal{F} f \cdot g = \int f \cdot \mathcal{F} g$$

   これは、フーリエ変換が内積を保存することを意味します。実内積の対称性により (innerₗ (Rd d)).flip = innerₗ (Rd d) です。

4. 最終的な等式（L268-298）:

   a. hflip の構築（L259-266）:

   • フーリエ変換の自己随伴性から、スカラー倍の形で次が得られます：

   $$\int \mathcal{F}f \cdot g = \int f \cdot \mathcal{F}g$$

   b. hflip' の構築（L268-283）:

   • hflip を積の形に変換します（smul_eq_mul（Mathlib のスカラー倍と積の等価性補題）を使用）。
   • hFg : 𝓕 g = conj f を使用して、$\mathcal{F}g$ を $\overline{f}$ に置き換えます。
   • これにより次が得られます：

   $$\int \mathcal{F}f \cdot \overline{\mathcal{F}f} = \int f \cdot \overline{f}$$

   c. 最終的な計算（L285-298）:

   • mul_comm（Mathlib の可換性補題）を使用して、両辺を conj( ) * ( ) の形に揃えます。
   • 最終的に、Parseval の等式が得られます：

   $$\int \overline{\mathcal{F}\psi} \cdot \mathcal{F}\psi = \int \overline{\psi} \cdot \psi$$

4. FourierL2 名前空間（L301-604）

4.1. シュワルツから L² への線形写像（L304-317）

noncomputable def schwartzToL2LM (d : ℕ) : SchwartzRd d →ₗ[ℂ] L2Rd d
noncomputable def fourierSchwartzLM (d : ℕ) : SchwartzRd d →ₗ[ℂ] SchwartzRd d
noncomputable def fourierToL2LM (d : ℕ) : SchwartzRd d →ₗ[ℂ] L2Rd d

• schwartzToL2LM: シュワルツ関数を L² 空間に送る線形写像です。SchwartzMap.toLpCLM を使用します。これは、シュワルツ関数を L² の等価類として扱う写像です：

  $$\text{schwartzToL2LM}: \mathcal{S}(\mathbb{R}^d) \to L^2(\mathbb{R}^d)$$

• fourierSchwartzLM: シュワルツ空間上のフーリエ変換（シュワルツ→シュワルツ）です。SchwartzMap.fourierTransformCLM を使用します。これは、シュワルツ関数をシュワルツ関数に写す写像です：

  $$\text{fourierSchwartzLM}: \mathcal{S}(\mathbb{R}^d) \to \mathcal{S}(\mathbb{R}^d)$$

• fourierToL2LM: シュワルツ関数を L² に落としてからフーリエ変換したものです。schwartzToL2LM ∘ fourierSchwartzLM として定義されます。つまり、シュワルツ関数をフーリエ変換してから L² 空間に送ります：

  $$\text{fourierToL2LM} = \text{schwartzToL2LM} \circ \text{fourierSchwartzLM}: \mathcal{S}(\mathbb{R}^d) \to L^2(\mathbb{R}^d)$$

4.2. Plancherel 定理（L321-489）

定理: plancherel_schwartz_toL2

theorem plancherel_schwartz_toL2 (d : ℕ) (ψ : SchwartzRd d) :
    ‖fourierToL2LM (d := d) ψ‖ = ‖schwartzToL2LM (d := d) ψ‖

この定理は、シュワルツ関数の L² ノルムがフーリエ変換で保存されることを示します（Plancherel 定理）：

$$|\mathcal{F}\psi|_{L^2} = |\psi|_{L^2}$$

$L^2$ の内積が積分で定義されるので、Parseval（積分形）より

$$\langle \mathcal{F}\psi,\mathcal{F}\psi\rangle = \langle \psi,\psi\rangle$$

が成り立ち、よって

$$|\mathcal{F}\psi|_{L^2} = |\psi|_{L^2}$$

が得られます。これを 本実装で定理化しています。

証明の開始（L294）:

• classical により、古典論理を有効化します。

Plancherel 定理の証明の流れ

1. L² 要素への変換（L332-373）:

   • X := schwartzToL2LM ψ、Y := fourierToL2LM ψ を定義します。これらは L² 空間の要素です（schwartzToL2LM、fourierToL2LM）。

   let X := schwartzToL2LM (d := d) ψ
   let Y := fourierToL2LM (d := d) ψ

   • SchwartzMap.toLpCLM_apply により、これらが SchwartzMap.toLp と一致することを示します。
   • SchwartzMap.coeFn_toLp により、L² 要素が元の関数と almost everywhere で一致することを示します。

   特に重要なのは、hF（L356-362）により、fourierSchwartzLM が Mathlib の fourierTransformCLM と一致し、したがって 𝓕 記法と一致することを確認することです：

   $$(\text{fourierSchwartzLM}\ \psi)(x) = \mathcal{F}\psi(x)$$

2. 内積の計算（L375-422）:

   • MeasureTheory.L2.inner_def により、L² の内積が積分で表されることを使用します：

   $$\langle f, g \rangle_{L^2} = \int \overline{f(x)},g(x),dx$$

   • hY_inner: $\langle Y, Y \rangle = \int \mathcal{F}\psi \cdot \overline{\mathcal{F}\psi}$
   • hX_inner: $\langle X, X \rangle = \int \psi \cdot \overline{\psi}$

   コードでは以下のように内積を計算します：

   have hY_inner : ⟪Y, Y⟫_ℂ = ∫ x : Rd d, (𝓕 (fun y : Rd d => ψ y) x) * conj (𝓕 (fun y : Rd d => ψ y) x)
   have hX_inner : ⟪X, X⟫_ℂ = ∫ x : Rd d, (ψ x) * conj (ψ x)

3. Parseval の利用（L424-450）:

   • FourierParsevalSchwartz.parseval_integral により、Parseval の等式（積分形）が得られます：

   $$\int \overline{\mathcal{F}\psi} \cdot \mathcal{F}\psi = \int \overline{\psi} \cdot \psi$$

   • mul_comm（Mathlib の可換性補題）を使用して、両辺を適切な形に揃えます。具体的には：

     • 左辺: $\int \overline{\mathcal{F}\psi} \cdot \mathcal{F}\psi \to \int \mathcal{F}\psi \cdot \overline{\mathcal{F}\psi}$
     • 右辺: $\int \overline{\psi} \cdot \psi \to \int \psi \cdot \overline{\psi}$

   • これにより、hY_inner と hX_inner から $\langle Y, Y \rangle = \langle X, X \rangle$ が得られます。

4. ノルムの等式（L452-489）:

   • inner_self_eq_norm_sq_to_K により、内積とノルムの関係を示します：

   $$\langle X, X \rangle = |X|^2$$

   • hsqC: $|Y|^2 = |X|^2$（複素数として）
   • Complex.ofReal_inj により、実数部分の等式 $|Y|^2 = |X|^2$ を示します。
   • mul_self_eq_mul_self_iff により、$|Y| = |X|$ または $|Y| = -|X|$ を示します。
   • ノルムの非負性（norm_nonneg）により、$|Y| = |X|$ を結論します。

   コードでは以下のようにノルムの等式を導きます：

   have hsqC : (‖Y‖ : ℂ) ^ 2 = (‖X‖ : ℂ) ^ 2 := by
     rw [← inner_self_eq_norm_sq_to_K, ← inner_self_eq_norm_sq_to_K]
     rw [hY_inner, hX_inner]
     -- Parseval の等式を使用

4.3. L² 全域への延長（稠密延長）（L491-603）

このセクションでは、シュワルツ関数上のフーリエ変換を L² 空間全体に延長する方法を説明します。Wikipedia では $S'$（緩増加超関数）を経由する定義も説明されますが、ここでは Hilbert 空間の一般論として、稠密部分空間上の等長写像を稠密延長する方法を採用します。

「フーリエ変換を L² に拡張」について

このスタンドアロンがやっていること:

• シュワルツ上のフーリエ変換 $\mathcal{S} \to \mathcal{S}$（Mathlib の定義）
• それを $\mathcal{S} \to L^2$ に落として ノルム保存（Plancherel）を示す
• さらに「稠密部分（シュワルツ像）上で等長」から $L^2 \to L^2$ へ稠密延長して、$L^2$ 全域の作用素も定義する

採っているルート:

• 「シュワルツ（稠密）上で等長」⇒「Hilbert 空間の一般論（ContinuousLinearMap.extend）で 稠密延長」

数学的には次の一般事実を使っています：

$$T: D\to H\ \text{が線形で}\ |T x|=|x|\ (x\in D),\ D\ \text{が稠密}\ \Rightarrow \exists!\ \widetilde{T}: H\to H\ \text{（等長）}$$

最後に、シュワルツの稠密性と等長性から $L^2$ 全域へ延長して

$$\mathcal{F}_{L^2} : L^2 \to L^2$$

を連続線形作用素として得ます（Lean: L² →L[ℂ] L²）。

4.3.1. 単射性の確認（L503-511）

定理: schwartzToL2LM_injective

theorem schwartzToL2LM_injective (d : ℕ) : Function.Injective (schwartzToL2LM (d := d))

この定理は、schwartzToL2LM が単射であることを示します。これは、シュワルツ関数が L² 空間に埋め込まれる際に、異なるシュワルツ関数が異なる L² 要素に対応することを保証します。

証明（L503-511）:

• classical により、古典論理を有効化します。
• SchwartzMap.injective_toLp を使用します。これは、連続関数が almost everywhere で一致すれば、実際に一致するという事実に基づいています。

4.3.2. シュワルツの像を部分空間として見る（L513-525）

noncomputable abbrev SchwartzRangeL2 (d : ℕ) : Submodule ℂ (L2Rd d) :=
  LinearMap.range (schwartzToL2LM (d := d))

noncomputable def schwartzEquivRange (d : ℕ) :
    SchwartzRd d ≃ₗ[ℂ] ↥(SchwartzRangeL2 (d := d)) :=
  LinearEquiv.ofInjective (schwartzToL2LM (d := d)) (schwartzToL2LM_injective (d := d))

• SchwartzRangeL2: schwartzToL2LM の像を L² 空間の部分空間として見たものです。
• schwartzEquivRange: シュワルツ空間と SchwartzRangeL2 の間の線形同型です。LinearEquiv.ofInjective を使用して、単射線形写像から同型を作成します。

4.3.3. SchwartzRangeL2 上のフーリエ変換（L522-525）

noncomputable def fourierOnSchwartzRangeLM (d : ℕ) :
    SchwartzRangeL2 (d := d) →ₗ[ℂ] L2Rd d :=
  (fourierToL2LM (d := d)).comp (schwartzEquivRange (d := d)).symm.toLinearMap

この定義は、SchwartzRangeL2 上の要素を Schwartz 空間に引き戻し、フーリエ変換を適用してから L² 空間に送る線形写像です（L425-427）。

4.3.4. Plancherel の適用（L527-559）

構造体: PlancherelOnSchwartzRange

structure PlancherelOnSchwartzRange (d : ℕ) : Prop where
  norm_map : ∀ s : SchwartzRangeL2 (d := d),
    ‖fourierOnSchwartzRangeLM (d := d) s‖ = ‖s‖

この構造体は、fourierOnSchwartzRangeLM が等長（ノルム保存）であることを表現します。

定義: plancherelOnSchwartzRange

noncomputable def plancherelOnSchwartzRange (d : ℕ) : PlancherelOnSchwartzRange (d := d)

この定義は、plancherel_schwartz_toL2 を使用して、SchwartzRangeL2 上の等長性を確立します。

証明の流れ（L533-553）:

1. SchwartzRangeL2 の要素 s をシュワルツ空間に引き戻します：$\psi = (\text{schwartzEquivRange})^{-1}(s)$
2. plancherel_schwartz_toL2 により、$|\mathcal{F}\psi|{L^2} = |\psi|{L^2}$ が成り立ちます
3. これと s が $\psi$ の L² への埋め込みであることから、$|\text{fourierOnSchwartzRangeLM}\ s| = |s|$ が得られます

つまり、SchwartzRangeL2 上のフーリエ変換も等長（ノルム保存）であることが示されます。

定義: fourierOnSchwartzRangeLI

noncomputable def fourierOnSchwartzRangeLI (d : ℕ) :
    SchwartzRangeL2 (d := d) →ₗᵢ[ℂ] L2Rd d

この定義は、fourierOnSchwartzRangeLM を等長線形写像（LinearIsometry）として束ねます（L545-546）。

4.3.5. 稠密性の確認（L561-572）

定理: dense_schwartzRangeL2

theorem dense_schwartzRangeL2 (d : ℕ) :
    Dense ((SchwartzRangeL2 (d := d) : Submodule ℂ (L2Rd d)) : Set (L2Rd d))

この定理は、SchwartzRangeL2 が L² 空間で稠密であることを示します。本実装では、外部からインポートされた QuantumMechanics.FourierL2.dense_range_schwartzToL2LM を参照して証明しています（L551-556）。

定理: denseRange_subtypeL_schwartzRangeL2

theorem denseRange_subtypeL_schwartzRangeL2 (d : ℕ) :
    DenseRange ((SchwartzRangeL2 (d := d)).subtypeL)

この定理は、SchwartzRangeL2 の包含写像（subtypeL）が稠密な範囲を持つことを示します。これは、Dense.denseRange_val を使用しています（L479-481）。

4.3.6. 稠密延長（L574-602）

定義: fourierL2CLM

noncomputable def fourierL2CLM (d : ℕ) : L2Rd d →L[ℂ] L2Rd d

この定義は、SchwartzRangeL2 上の等長線形写像を L² 空間全体に延長した連続線形写像です（L564-575）。

構成の流れ（L575-588）:

1. 等長性の確認（L578-580）:

   • Isometry (⇑S.subtypeL) により、包含写像が等長であることを確認します。
   • これは、部分空間の包含がノルムを保存するという事実に基づいています：

   $$|\text{subtypeL}\ x| = |x|$$

   ここで subtypeL は部分空間から全体空間への包含写像です。

2. 一様連続性の確認（L581）:

   • IsUniformInducing (⇑S.subtypeL) により、包含写像が一様連続であることを確認します。
   • これは、等長写像が一様連続であるという事実に基づいています。

3. 稠密延長（L583-588）:

   • ContinuousLinearMap.extend を使用して、fourierOnSchwartzRangeLI を L² 空間全体に延長します。
   • この延長は、稠密部分空間上の連続線形写像を完備空間全体に一意に延長するという一般論に基づいています。

   数学的には、次の一般事実が使われています：

   $$T: D\to H\ \text{が線形で}\ |T x|=|x|\ (x\in D),\ D\ \text{が稠密}\ \Rightarrow \exists!\ \widetilde{T}: H\to H\ \text{（等長）}$$

定理: fourierL2CLM_apply_subtype

theorem fourierL2CLM_apply_subtype (d : ℕ) (s : SchwartzRangeL2 (d := d)) :
    fourierL2CLM (d := d) (s : L2Rd d) = fourierOnSchwartzRangeLM (d := d) s

この定理は、延長が SchwartzRangeL2 上で元の写像（fourierOnSchwartzRangeLM）と一致することを示します。これは、ContinuousLinearMap.extend_eq を使用しています（L591-602）。

証明（L591-602）:

• classical により、古典論理を有効化します。
• ContinuousLinearMap.extend_eq により、稠密部分空間上の点では延長が元の写像と一致することを示します。

これは、稠密延長の一意性と、稠密部分空間上での一致を保証する重要な性質です。

まとめ

このファイルは、量子力学の位置表示と運動量表示の橋渡しに必要な以下の要素を、Mathlib の既存 API を活用して形式化しています：

1. 共役と逆フーリエの関係: conj (𝓕 f) = 𝓕⁻ (conj f) により、フーリエ変換と共役の交換関係を確立
2. Parseval（積分形）: シュワルツ関数に対する Parseval の等式により、フーリエ変換が内積を保存することを示す
3. Plancherel 定理: シュワルツ関数の L² ノルムがフーリエ変換で保存されることを示す
4. L² 全域への延長: 稠密部分空間（シュワルツ関数の像）上の等長写像を、Hilbert 空間の一般論に基づいて L² 空間全体に延長

これらの結果は、量子力学における位置表示と運動量表示の等価性を数学的に厳密に確立するための重要な基礎となります。

plancherel4qm_slides_link.pdf