Physlib.QuantumMechanics.Operators.OneDimension.Parity

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.SchwartzSubmodule
public import Physlib.QuantumMechanics.Operators.OneDimension.Unbounded
public import Mathlib.MeasureTheory.Measure.Haar.Unique
public import Mathlib.Analysis.Calculus.ContDiff.Operations

Parity operator

@[expose] public section

The parity operator on functions

The parity operator is defined as linear map from ℝ → ℂ to itself, such that ψ is taken to fun x => ψ (-x).

def parityOperator : (ℝ → ℂ) →ₗ[ℂ] (ℝ → ℂ) where
  toFun ψ := fun x => ψ (-x)
  map_add' ψ1 ψ2 := byψ1:ℝ → ℂψ2:ℝ → ℂ⊢ (fun x => (ψ1 + ψ2) (-x)) = (fun x => ψ1 (-x)) + fun x => ψ2 (-x)
    funext xψ1:ℝ → ℂψ2:ℝ → ℂx:ℝ⊢ (ψ1 + ψ2) (-x) = ((fun x => ψ1 (-x)) + fun x => ψ2 (-x)) x
    simpAll goals completed! 🐙
  map_smul' a ψ1 := bya:ℂψ1:ℝ → ℂ⊢ (fun x => (a • ψ1) (-x)) = (RingHom.id ℂ) a • fun x => ψ1 (-x)
    funext xa:ℂψ1:ℝ → ℂx:ℝ⊢ (a • ψ1) (-x) = ((RingHom.id ℂ) a • fun x => ψ1 (-x)) x
    simpAll goals completed! 🐙

The parity operator on Schwartz maps

The parity operator on the Schwartz maps is defined as the linear map from 𝓢(ℝ, ℂ) to itself, such that ψ is taken to fun x => ψ (-x).


def parityOperatorSchwartz : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) := by⊢ 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ)
  refine (SchwartzMap.compCLM ℂ (g := (fun x => - x : ℝ → ℝ)) ⟨?_, ?_⟩ ?_)refine_1⊢ ContDiff ℝ ↑⊤ fun x => -xrefine_2⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => -x) x‖ ≤ C * (1 + ‖x‖) ^ krefine_3⊢ ∃ k C, ∀ (x : ℝ), ‖x‖ ≤ C * (1 + ‖-x‖) ^ k
  ·refine_1⊢ ContDiff ℝ ↑⊤ fun x => -x fun_propAll goals completed! 🐙
  ·refine_2⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => -x) x‖ ≤ C * (1 + ‖x‖) ^ k intro nrefine_2n:ℕ⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => -x) x‖ ≤ C * (1 + ‖x‖) ^ k
    simp only [Real.norm_eq_abs]refine_2n:ℕ⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => -x) x‖ ≤ C * (1 + |x|) ^ k
    use 1, 1hn:ℕ⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => -x) x‖ ≤ 1 * (1 + |x|) ^ 1
    intro xhn:ℕx:ℝ⊢ ‖iteratedFDeriv ℝ n (fun x => -x) x‖ ≤ 1 * (1 + |x|) ^ 1
    simp only [pow_one, one_mul]hn:ℕx:ℝ⊢ ‖iteratedFDeriv ℝ n (fun x => -x) x‖ ≤ 1 + |x|
    rw [show (fun x : ℝ => -x) = -(fun x : ℝ => x) from rflhn:ℕx:ℝ⊢ ‖iteratedFDeriv ℝ n (-fun x => x) x‖ ≤ 1 + |x|hn:ℕx:ℝ⊢ ‖iteratedFDeriv ℝ n (-fun x => x) x‖ ≤ 1 + |x|]hn:ℕx:ℝ⊢ ‖iteratedFDeriv ℝ n (-fun x => x) x‖ ≤ 1 + |x|
    rw [iteratedFDeriv_neg_applyhn:ℕx:ℝ⊢ ‖-iteratedFDeriv ℝ n (fun x => x) x‖ ≤ 1 + |x|hn:ℕx:ℝ⊢ ‖-iteratedFDeriv ℝ n (fun x => x) x‖ ≤ 1 + |x|]hn:ℕx:ℝ⊢ ‖-iteratedFDeriv ℝ n (fun x => x) x‖ ≤ 1 + |x|
    simp only [norm_neg]hn:ℕx:ℝ⊢ ‖iteratedFDeriv ℝ n (fun x => x) x‖ ≤ 1 + |x|
    match n with
    | 0 =>n:ℕx:ℝ⊢ ‖iteratedFDeriv ℝ 0 (fun x => x) x‖ ≤ 1 + |x| simpAll goals completed! 🐙
    | 1 =>n:ℕx:ℝ⊢ ‖iteratedFDeriv ℝ 1 (fun x => x) x‖ ≤ 1 + |x|
      rw [iteratedFDeriv_succ_eq_comp_rightn:ℕx:ℝ⊢ ‖(⇑(continuousMultilinearCurryRightEquiv' ℝ 0 ℝ ℝ).symm ∘ iteratedFDeriv ℝ 0 fun y => fderiv ℝ (fun x => x) y) x‖ ≤
  1 + |x|n:ℕx:ℝ⊢ ‖(⇑(continuousMultilinearCurryRightEquiv' ℝ 0 ℝ ℝ).symm ∘ iteratedFDeriv ℝ 0 fun y => fderiv ℝ (fun x => x) y) x‖ ≤
  1 + |x|]n:ℕx:ℝ⊢ ‖(⇑(continuousMultilinearCurryRightEquiv' ℝ 0 ℝ ℝ).symm ∘ iteratedFDeriv ℝ 0 fun y => fderiv ℝ (fun x => x) y) x‖ ≤
  1 + |x|
      simp [ContinuousLinearMap.norm_id]All goals completed! 🐙
    | .succ (.succ n) =>n✝:ℕx:ℝn:ℕ⊢ ‖iteratedFDeriv ℝ n.succ.succ (fun x => x) x‖ ≤ 1 + |x|
      rw [iteratedFDeriv_succ_eq_comp_rightn✝:ℕx:ℝn:ℕ⊢ ‖(⇑(continuousMultilinearCurryRightEquiv' ℝ (n + 1) ℝ ℝ).symm ∘
        iteratedFDeriv ℝ (n + 1) fun y => fderiv ℝ (fun x => x) y)
      x‖ ≤
  1 + |x|n✝:ℕx:ℝn:ℕ⊢ ‖(⇑(continuousMultilinearCurryRightEquiv' ℝ (n + 1) ℝ ℝ).symm ∘
        iteratedFDeriv ℝ (n + 1) fun y => fderiv ℝ (fun x => x) y)
      x‖ ≤
  1 + |x|]n✝:ℕx:ℝn:ℕ⊢ ‖(⇑(continuousMultilinearCurryRightEquiv' ℝ (n + 1) ℝ ℝ).symm ∘
        iteratedFDeriv ℝ (n + 1) fun y => fderiv ℝ (fun x => x) y)
      x‖ ≤
  1 + |x|
      simp only [Nat.succ_eq_add_one, fderiv_fun_id, Function.comp_apply,
        LinearIsometryEquiv.norm_map, ge_iff_le]n✝:ℕx:ℝn:ℕ⊢ ‖iteratedFDeriv ℝ (n + 1) (fun y => ContinuousLinearMap.id ℝ ℝ) x‖ ≤ 1 + |x|
      rw [iteratedFDeriv_const_of_nen✝:ℕx:ℝn:ℕ⊢ ‖0 x‖ ≤ 1 + |x|hnn✝:ℕx:ℝn:ℕ⊢ n + 1 ≠ 0n✝:ℕx:ℝn:ℕ⊢ ‖0 x‖ ≤ 1 + |x|hnn✝:ℕx:ℝn:ℕ⊢ n + 1 ≠ 0]n✝:ℕx:ℝn:ℕ⊢ ‖0 x‖ ≤ 1 + |x|hnn✝:ℕx:ℝn:ℕ⊢ n + 1 ≠ 0
      simp only [Pi.zero_apply, norm_zero]n✝:ℕx:ℝn:ℕ⊢ 0 ≤ 1 + |x|hnn✝:ℕx:ℝn:ℕ⊢ n + 1 ≠ 0
      apply add_nonneghan✝:ℕx:ℝn:ℕ⊢ 0 ≤ 1hbn✝:ℕx:ℝn:ℕ⊢ 0 ≤ |x|hnn✝:ℕx:ℝn:ℕ⊢ n + 1 ≠ 0
      ·han✝:ℕx:ℝn:ℕ⊢ 0 ≤ 1 exact zero_le_one' ℝAll goals completed! 🐙
      ·hbn✝:ℕx:ℝn:ℕ⊢ 0 ≤ |x| exact abs_nonneg xAll goals completed! 🐙
      simpAll goals completed! 🐙
  ·refine_3⊢ ∃ k C, ∀ (x : ℝ), ‖x‖ ≤ C * (1 + ‖-x‖) ^ k simprefine_3⊢ ∃ k C, ∀ (x : ℝ), |x| ≤ C * (1 + |x|) ^ k
    use 1, 1h⊢ ∀ (x : ℝ), |x| ≤ 1 * (1 + |x|) ^ 1
    intro xhx:ℝ⊢ |x| ≤ 1 * (1 + |x|) ^ 1
    simpAll goals completed! 🐙

The unbounded parity operator, whose domain is Schwartz maps.

def parityOperatorUnbounded : UnboundedOperator schwartzIncl schwartzIncl_injective :=
  UnboundedOperator.ofSelfCLM parityOperatorSchwartz

@[simp]
lemma parityOperatorSchwartz_parityOperatorSchwartz (ψ : 𝓢(ℝ, ℂ)) :
    parityOperatorSchwartz (parityOperatorSchwartz ψ) = ψ := byψ:𝓢(ℝ, ℂ)⊢ parityOperatorSchwartz (parityOperatorSchwartz ψ) = ψ
  ext xψ:𝓢(ℝ, ℂ)x:ℝ⊢ (parityOperatorSchwartz (parityOperatorSchwartz ψ)) x = ψ x
  simp [parityOperatorSchwartz]All goals completed! 🐙

Parity operator is symmetric



lemma parityOperatorUnbounded_isSymmetric :
    parityOperatorUnbounded.IsSymmetric := by⊢ parityOperatorUnbounded.IsSymmetric
  intro ψ1 ψ2ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)⊢ ⟪(↑parityOperatorUnbounded).toFun ψ1, schwartzIncl ψ2⟫_ℂ = ⟪schwartzIncl ψ1, (↑parityOperatorUnbounded).toFun ψ2⟫_ℂ
  dsimp [parityOperatorUnbounded]ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)⊢ ⟪schwartzIncl (parityOperatorSchwartz ψ1), schwartzIncl ψ2⟫_ℂ =
  ⟪schwartzIncl ψ1, schwartzIncl (parityOperatorSchwartz ψ2)⟫_ℂ
  rw [schwartzIncl_inner,ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((parityOperatorSchwartz ψ1) x) * ψ2 x =
  ⟪schwartzIncl ψ1, schwartzIncl (parityOperatorSchwartz ψ2)⟫_ℂψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((parityOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (parityOperatorSchwartz ψ2) x schwartzIncl_innerψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((parityOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (parityOperatorSchwartz ψ2) xψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((parityOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (parityOperatorSchwartz ψ2) x]ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((parityOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (parityOperatorSchwartz ψ2) x
  let f (x : ℝ) :=
    (starRingEnd ℂ) ((ψ1) (-x)) * (ψ2) xψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)f:ℝ → ℂ := fun x => (starRingEnd ℂ) (ψ1 (-x)) * ψ2 x⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((parityOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (parityOperatorSchwartz ψ2) x
  change ∫ (x : ℝ), f x = _ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)f:ℝ → ℂ := fun x => (starRingEnd ℂ) (ψ1 (-x)) * ψ2 x⊢ ∫ (x : ℝ), f x = ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (parityOperatorSchwartz ψ2) x
  trans ∫ (x : ℝ), f (- x)ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)f:ℝ → ℂ := fun x => (starRingEnd ℂ) (ψ1 (-x)) * ψ2 x⊢ ∫ (x : ℝ), f x = ∫ (x : ℝ), f (-x)ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)f:ℝ → ℂ := fun x => (starRingEnd ℂ) (ψ1 (-x)) * ψ2 x⊢ ∫ (x : ℝ), f (-x) = ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (parityOperatorSchwartz ψ2) x
  ·ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)f:ℝ → ℂ := fun x => (starRingEnd ℂ) (ψ1 (-x)) * ψ2 x⊢ ∫ (x : ℝ), f x = ∫ (x : ℝ), f (-x) exact Eq.symm (integral_neg_eq_self f volume)All goals completed! 🐙
  ·ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)f:ℝ → ℂ := fun x => (starRingEnd ℂ) (ψ1 (-x)) * ψ2 x⊢ ∫ (x : ℝ), f (-x) = ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (parityOperatorSchwartz ψ2) x simp only [neg_neg, f]ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)f:ℝ → ℂ := fun x => (starRingEnd ℂ) (ψ1 (-x)) * ψ2 x⊢ ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * ψ2 (-x) = ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (parityOperatorSchwartz ψ2) x
    rflAll goals completed! 🐙