Physlib.QuantumMechanics.Operators.OneDimension.Momentum

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 Mathlib.Analysis.Calculus.FDeriv.Star
public import Physlib.QuantumMechanics.Operators.OneDimension.Unbounded
public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.SchwartzSubmodule
public import Physlib.QuantumMechanics.PlanckConstant
public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.PlaneWaves

Momentum operator

In this module we define:

The momentum operator on functions ℝ → ℂ

The momentum operator on Schwartz maps as an unbounded operator on the Hilbert space.

We show that plane waves are generalized eigenvectors of the momentum operator.

@[expose] public section

The momentum operator on functions `ℝ → ℂ`

The momentum operator is defined as the map from ℝ → ℂ to ℝ → ℂ taking ψ to - i ℏ ψ'.

def momentumOperator (ψ : ℝ → ℂ) : ℝ → ℂ := fun x ↦ - Complex.I * ℏ * deriv ψ x

              lemma momentumOperator_eq_smul (ψ : ℝ → ℂ) :
    momentumOperator ψ = fun x => (- Complex.I * ℏ) • deriv ψ x := byψ:ℝ → ℂ⊢ momentumOperator ψ = fun x => (-Complex.I * ↑↑ℏ) • deriv ψ x
  rflAll goals completed! 🐙

@[fun_prop]
lemma continuous_momentumOperator (ψ : ℝ → ℂ) (hψ : ContDiff ℝ 1 ψ) :
    Continuous (momentumOperator ψ) := byψ:ℝ → ℂhψ:ContDiff ℝ 1 ψ⊢ Continuous (momentumOperator ψ)
  rw [momentumOperator_eq_smulψ:ℝ → ℂhψ:ContDiff ℝ 1 ψ⊢ Continuous fun x => (-Complex.I * ↑↑ℏ) • deriv ψ xψ:ℝ → ℂhψ:ContDiff ℝ 1 ψ⊢ Continuous fun x => (-Complex.I * ↑↑ℏ) • deriv ψ x]ψ:ℝ → ℂhψ:ContDiff ℝ 1 ψ⊢ Continuous fun x => (-Complex.I * ↑↑ℏ) • deriv ψ x
  fun_propAll goals completed! 🐙

lemma momentumOperator_smul {ψ : ℝ → ℂ} (hψ : Differentiable ℝ ψ) (c : ℂ) :
    momentumOperator (c • ψ) = c • momentumOperator ψ := byψ:ℝ → ℂhψ:Differentiable ℝ ψc:ℂ⊢ momentumOperator (c • ψ) = c • momentumOperator ψ
  rw [momentumOperator_eq_smul,ψ:ℝ → ℂhψ:Differentiable ℝ ψc:ℂ⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (c • ψ) x) = c • momentumOperator ψψ:ℝ → ℂhψ:Differentiable ℝ ψc:ℂ⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (c • ψ) x) = c • fun x => (-Complex.I * ↑↑ℏ) • deriv ψ x momentumOperator_eq_smulψ:ℝ → ℂhψ:Differentiable ℝ ψc:ℂ⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (c • ψ) x) = c • fun x => (-Complex.I * ↑↑ℏ) • deriv ψ xψ:ℝ → ℂhψ:Differentiable ℝ ψc:ℂ⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (c • ψ) x) = c • fun x => (-Complex.I * ↑↑ℏ) • deriv ψ x]ψ:ℝ → ℂhψ:Differentiable ℝ ψc:ℂ⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (c • ψ) x) = c • fun x => (-Complex.I * ↑↑ℏ) • deriv ψ x
  funext xψ:ℝ → ℂhψ:Differentiable ℝ ψc:ℂx:ℝ⊢ (-Complex.I * ↑↑ℏ) • deriv (c • ψ) x = (c • fun x => (-Complex.I * ↑↑ℏ) • deriv ψ x) x
  simp only [Pi.smul_apply, deriv_const_smul _ (hψ x), smul_comm (-Complex.I * ℏ) c]All goals completed! 🐙

lemma momentumOperator_add {ψ1 ψ2 : ℝ → ℂ}
    (hψ1 : Differentiable ℝ ψ1) (hψ2 : Differentiable ℝ ψ2) :
    momentumOperator (ψ1 + ψ2) = momentumOperator ψ1 + momentumOperator ψ2 := byψ1:ℝ → ℂψ2:ℝ → ℂhψ1:Differentiable ℝ ψ1hψ2:Differentiable ℝ ψ2⊢ momentumOperator (ψ1 + ψ2) = momentumOperator ψ1 + momentumOperator ψ2
  rw [momentumOperator_eq_smul,ψ1:ℝ → ℂψ2:ℝ → ℂhψ1:Differentiable ℝ ψ1hψ2:Differentiable ℝ ψ2⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (ψ1 + ψ2) x) = momentumOperator ψ1 + momentumOperator ψ2ψ1:ℝ → ℂψ2:ℝ → ℂhψ1:Differentiable ℝ ψ1hψ2:Differentiable ℝ ψ2⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (ψ1 + ψ2) x) =
  (fun x => (-Complex.I * ↑↑ℏ) • deriv ψ1 x) + fun x => (-Complex.I * ↑↑ℏ) • deriv ψ2 x momentumOperator_eq_smul,ψ1:ℝ → ℂψ2:ℝ → ℂhψ1:Differentiable ℝ ψ1hψ2:Differentiable ℝ ψ2⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (ψ1 + ψ2) x) = (fun x => (-Complex.I * ↑↑ℏ) • deriv ψ1 x) + momentumOperator ψ2ψ1:ℝ → ℂψ2:ℝ → ℂhψ1:Differentiable ℝ ψ1hψ2:Differentiable ℝ ψ2⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (ψ1 + ψ2) x) =
  (fun x => (-Complex.I * ↑↑ℏ) • deriv ψ1 x) + fun x => (-Complex.I * ↑↑ℏ) • deriv ψ2 x momentumOperator_eq_smulψ1:ℝ → ℂψ2:ℝ → ℂhψ1:Differentiable ℝ ψ1hψ2:Differentiable ℝ ψ2⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (ψ1 + ψ2) x) =
  (fun x => (-Complex.I * ↑↑ℏ) • deriv ψ1 x) + fun x => (-Complex.I * ↑↑ℏ) • deriv ψ2 xψ1:ℝ → ℂψ2:ℝ → ℂhψ1:Differentiable ℝ ψ1hψ2:Differentiable ℝ ψ2⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (ψ1 + ψ2) x) =
  (fun x => (-Complex.I * ↑↑ℏ) • deriv ψ1 x) + fun x => (-Complex.I * ↑↑ℏ) • deriv ψ2 x]ψ1:ℝ → ℂψ2:ℝ → ℂhψ1:Differentiable ℝ ψ1hψ2:Differentiable ℝ ψ2⊢ (fun x => (-Complex.I * ↑↑ℏ) • deriv (ψ1 + ψ2) x) =
  (fun x => (-Complex.I * ↑↑ℏ) • deriv ψ1 x) + fun x => (-Complex.I * ↑↑ℏ) • deriv ψ2 x
  funext xψ1:ℝ → ℂψ2:ℝ → ℂhψ1:Differentiable ℝ ψ1hψ2:Differentiable ℝ ψ2x:ℝ⊢ (-Complex.I * ↑↑ℏ) • deriv (ψ1 + ψ2) x =
  ((fun x => (-Complex.I * ↑↑ℏ) • deriv ψ1 x) + fun x => (-Complex.I * ↑↑ℏ) • deriv ψ2 x) x
  simp only [Pi.add_apply, deriv_add (hψ1 x) (hψ2 x), smul_eq_mul]ψ1:ℝ → ℂψ2:ℝ → ℂhψ1:Differentiable ℝ ψ1hψ2:Differentiable ℝ ψ2x:ℝ⊢ -Complex.I * ↑↑ℏ * (deriv ψ1 x + deriv ψ2 x) = -Complex.I * ↑↑ℏ * deriv ψ1 x + -Complex.I * ↑↑ℏ * deriv ψ2 x
  ringAll goals completed! 🐙

The momentum 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 => - I ℏ * ψ' x.

def momentumOperatorSchwartz : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) where
  toFun ψ := (- Complex.I * ℏ) • SchwartzMap.derivCLM ℂ ℂ ψ
  map_add' ψ1 ψ2 := byψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)⊢ (-Complex.I * ↑↑ℏ) • (derivCLM ℂ ℂ) (ψ1 + ψ2) =
  (-Complex.I * ↑↑ℏ) • (derivCLM ℂ ℂ) ψ1 + (-Complex.I * ↑↑ℏ) • (derivCLM ℂ ℂ) ψ2
    simp only [neg_mul, map_add, smul_add, neg_smul]All goals completed! 🐙
  map_smul' a ψ := bya:ℂψ:𝓢(ℝ, ℂ)⊢ (-Complex.I * ↑↑ℏ) • (derivCLM ℂ ℂ) (a • ψ) = (RingHom.id ℂ) a • (-Complex.I * ↑↑ℏ) • (derivCLM ℂ ℂ) ψ
    simp only [map_smul, RingHom.id_apply, smul_comm (-Complex.I * ℏ) a]All goals completed! 🐙
  cont := by⊢ Continuous fun ψ => (-Complex.I * ↑↑ℏ) • (derivCLM ℂ ℂ) ψ fun_propAll goals completed! 🐙



lemma momentumOperatorSchwartz_apply (ψ : 𝓢(ℝ, ℂ))
    (x : ℝ) : (momentumOperatorSchwartz ψ) x = (- Complex.I * ℏ) * (deriv ψ x) := byψ:𝓢(ℝ, ℂ)x:ℝ⊢ (momentumOperatorSchwartz ψ) x = -Complex.I * ↑↑ℏ * deriv (⇑ψ) x
  rw [momentumOperatorSchwartzψ:𝓢(ℝ, ℂ)x:ℝ⊢ ({ toFun := fun ψ => (-Complex.I * ↑↑ℏ) • (derivCLM ℂ ℂ) ψ, map_add' := momentumOperatorSchwartz._proof_3,
        map_smul' := momentumOperatorSchwartz._proof_4, cont := momentumOperatorSchwartz._proof_5 }
      ψ)
    x =
  -Complex.I * ↑↑ℏ * deriv (⇑ψ) xψ:𝓢(ℝ, ℂ)x:ℝ⊢ ({ toFun := fun ψ => (-Complex.I * ↑↑ℏ) • (derivCLM ℂ ℂ) ψ, map_add' := momentumOperatorSchwartz._proof_3,
        map_smul' := momentumOperatorSchwartz._proof_4, cont := momentumOperatorSchwartz._proof_5 }
      ψ)
    x =
  -Complex.I * ↑↑ℏ * deriv (⇑ψ) x]ψ:𝓢(ℝ, ℂ)x:ℝ⊢ ({ toFun := fun ψ => (-Complex.I * ↑↑ℏ) • (derivCLM ℂ ℂ) ψ, map_add' := momentumOperatorSchwartz._proof_3,
        map_smul' := momentumOperatorSchwartz._proof_4, cont := momentumOperatorSchwartz._proof_5 }
      ψ)
    x =
  -Complex.I * ↑↑ℏ * deriv (⇑ψ) x
  rflAll goals completed! 🐙

The unbounded momentum operator, whose domain is Schwartz maps.

def momentumOperatorUnbounded : UnboundedOperator schwartzIncl schwartzIncl_injective :=
  UnboundedOperator.ofSelfCLM momentumOperatorSchwartz

Generalized eigenvectors of the momentum operator



lemma planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded (k : ℝ) :
    momentumOperatorUnbounded.IsGeneralizedEigenvector
      (planewaveFunctional k) (2 * Real.pi * ℏ * k) := byk:ℝ⊢ momentumOperatorUnbounded.IsGeneralizedEigenvector (planewaveFunctional k) (2 * ↑Real.pi * ↑↑ℏ * ↑k)
  dsimp [momentumOperatorUnbounded]k:ℝ⊢ (UnboundedOperator.ofSelfCLM momentumOperatorSchwartz).IsGeneralizedEigenvector (planewaveFunctional k)
  (2 * ↑Real.pi * ↑↑ℏ * ↑k)
  rw [UnboundedOperator.isGeneralizedEigenvector_ofSelfCLM_iffk:ℝ⊢ ∀ (ψ : 𝓢(ℝ, ℂ)),
  (planewaveFunctional k) (momentumOperatorSchwartz ψ) = (2 * ↑Real.pi * ↑↑ℏ * ↑k) • (planewaveFunctional k) ψk:ℝ⊢ ∀ (ψ : 𝓢(ℝ, ℂ)),
  (planewaveFunctional k) (momentumOperatorSchwartz ψ) = (2 * ↑Real.pi * ↑↑ℏ * ↑k) • (planewaveFunctional k) ψ]k:ℝ⊢ ∀ (ψ : 𝓢(ℝ, ℂ)),
  (planewaveFunctional k) (momentumOperatorSchwartz ψ) = (2 * ↑Real.pi * ↑↑ℏ * ↑k) • (planewaveFunctional k) ψ
  intro ψk:ℝψ:𝓢(ℝ, ℂ)⊢ (planewaveFunctional k) (momentumOperatorSchwartz ψ) = (2 * ↑Real.pi * ↑↑ℏ * ↑k) • (planewaveFunctional k) ψ
  trans (-((Complex.I * ↑↑ℏ) •
      (SchwartzMap.fourierTransformCLM ℂ) ((SchwartzMap.derivCLM ℂ ℂ) ψ) k))k:ℝψ:𝓢(ℝ, ℂ)⊢ (planewaveFunctional k) (momentumOperatorSchwartz ψ) =
  -((Complex.I * ↑↑ℏ) • ((fourierTransformCLM ℂ) ((derivCLM ℂ ℂ) ψ)) k)k:ℝψ:𝓢(ℝ, ℂ)⊢ -((Complex.I * ↑↑ℏ) • ((fourierTransformCLM ℂ) ((derivCLM ℂ ℂ) ψ)) k) =
  (2 * ↑Real.pi * ↑↑ℏ * ↑k) • (planewaveFunctional k) ψ
  ·k:ℝψ:𝓢(ℝ, ℂ)⊢ (planewaveFunctional k) (momentumOperatorSchwartz ψ) =
  -((Complex.I * ↑↑ℏ) • ((fourierTransformCLM ℂ) ((derivCLM ℂ ℂ) ψ)) k) simp [momentumOperatorSchwartz, planewaveFunctional_apply,
      SchwartzMap.fourierTransformCLM_apply]All goals completed! 🐙
  simp only [SchwartzMap.fourierTransformCLM_apply, smul_eq_mul]k:ℝψ:𝓢(ℝ, ℂ)⊢ -(Complex.I * ↑↑ℏ * (FourierTransform.fourier ((derivCLM ℂ ℂ) ψ)) k) =
  2 * ↑Real.pi * ↑↑ℏ * ↑k * (planewaveFunctional k) ψ
  change -(Complex.I * ↑↑ℏ * (FourierTransform.fourier ((deriv ψ)) k)) = _k:ℝψ:𝓢(ℝ, ℂ)⊢ -(Complex.I * ↑↑ℏ * FourierTransform.fourier (deriv ⇑ψ) k) = 2 * ↑Real.pi * ↑↑ℏ * ↑k * (planewaveFunctional k) ψ
  rw [Real.fourier_deriv (SchwartzMap.integrable ψ)
      (SchwartzMap.differentiable (ψ)) (SchwartzMap.integrable ((SchwartzMap.derivCLM ℂ ℂ) ψ))k:ℝψ:𝓢(ℝ, ℂ)⊢ -(Complex.I * ↑↑ℏ * (fun x => (2 * ↑Real.pi * Complex.I * ↑x) • FourierTransform.fourier (⇑ψ) x) k) =
  2 * ↑Real.pi * ↑↑ℏ * ↑k * (planewaveFunctional k) ψk:ℝψ:𝓢(ℝ, ℂ)⊢ -(Complex.I * ↑↑ℏ * (fun x => (2 * ↑Real.pi * Complex.I * ↑x) • FourierTransform.fourier (⇑ψ) x) k) =
  2 * ↑Real.pi * ↑↑ℏ * ↑k * (planewaveFunctional k) ψ]k:ℝψ:𝓢(ℝ, ℂ)⊢ -(Complex.I * ↑↑ℏ * (fun x => (2 * ↑Real.pi * Complex.I * ↑x) • FourierTransform.fourier (⇑ψ) x) k) =
  2 * ↑Real.pi * ↑↑ℏ * ↑k * (planewaveFunctional k) ψ
  simp only [planewaveFunctional_apply, smul_eq_mul]k:ℝψ:𝓢(ℝ, ℂ)⊢ -(Complex.I * ↑↑ℏ * (2 * ↑Real.pi * Complex.I * ↑k * FourierTransform.fourier (⇑ψ) k)) =
  2 * ↑Real.pi * ↑↑ℏ * ↑k * (FourierTransform.fourier ψ) k
  ring_nfk:ℝψ:𝓢(ℝ, ℂ)⊢ -(Complex.I ^ 2 * ↑↑ℏ * ↑Real.pi * ↑k * FourierTransform.fourier (⇑ψ) k * 2) =
  ↑↑ℏ * ↑Real.pi * ↑k * (FourierTransform.fourier ψ) k * 2
  simp [Complex.I_sq]k:ℝψ:𝓢(ℝ, ℂ)⊢ FourierTransform.fourier (⇑ψ) k = (FourierTransform.fourier ψ) k ∨ k = 0
  exact Or.inl rflAll goals completed! 🐙

The momentum operator is symmetric



lemma momentumOperatorUnbounded_isSymmetric : momentumOperatorUnbounded.IsSymmetric := by⊢ momentumOperatorUnbounded.IsSymmetric
  intro ψ1 ψ2ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)⊢ inner ℂ ((↑momentumOperatorUnbounded).toFun ψ1) (schwartzIncl ψ2) =
  inner ℂ (schwartzIncl ψ1) ((↑momentumOperatorUnbounded).toFun ψ2)
  have hint : ∀ f g : 𝓢(ℝ, ℂ),
      MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume :=
    fun f g => ((ContinuousLinearEquiv.integrable_comp_iff (starL' ℝ)).mpr
      (SchwartzMap.integrable f)).mul_of_top_left (SchwartzMap.memLp_top g)ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ inner ℂ ((↑momentumOperatorUnbounded).toFun ψ1) (schwartzIncl ψ2) =
  inner ℂ (schwartzIncl ψ1) ((↑momentumOperatorUnbounded).toFun ψ2)
  dsimp [momentumOperatorUnbounded]ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ inner ℂ (schwartzIncl (momentumOperatorSchwartz ψ1)) (schwartzIncl ψ2) =
  inner ℂ (schwartzIncl ψ1) (schwartzIncl (momentumOperatorSchwartz ψ2))
  rw [schwartzIncl_inner,ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  inner ℂ (schwartzIncl ψ1) (schwartzIncl (momentumOperatorSchwartz ψ2))ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (momentumOperatorSchwartz ψ2) x schwartzIncl_innerψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (momentumOperatorSchwartz ψ2) xψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (momentumOperatorSchwartz ψ2) x]ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (momentumOperatorSchwartz ψ2) x
  conv_rhs =>
    enter [2, x]ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volumex:ℝ| (starRingEnd ℂ) (ψ1 x) * (momentumOperatorSchwartz ψ2) x
    rw [momentumOperatorSchwartz_apply, ← fderiv_apply_one_eq_deriv, ← mul_assoc,
      mul_comm _ (-Complex.I * ↑↑ℏ), mul_assoc]ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volumex:ℝ| -Complex.I * ↑↑ℏ * ((starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1)
  rw [MeasureTheory.integral_const_mul,ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  -Complex.I * ↑↑ℏ * ∫ (a : ℝ), (starRingEnd ℂ) (ψ1 a) * (fderiv ℝ (⇑ψ2) a) 1ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (a : ℝ), -Complex.I * ↑↑ℏ * -((fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) a) 1 * ψ2 a)hf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 x) MeasureTheory.volumehfg'ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1) MeasureTheory.volumehfgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * ψ2 x) MeasureTheory.volumehfψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport ⇑ψ2, DifferentiableAt ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) xhgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport fun a => (starRingEnd ℂ) (ψ1 a), DifferentiableAt ℝ (⇑ψ2) x integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable,ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  -Complex.I * ↑↑ℏ * -∫ (x : ℝ), (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 xhf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 x) MeasureTheory.volumehfg'ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1) MeasureTheory.volumehfgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * ψ2 x) MeasureTheory.volumehfψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport ⇑ψ2, DifferentiableAt ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) xhgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport fun a => (starRingEnd ℂ) (ψ1 a), DifferentiableAt ℝ (⇑ψ2) xψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (a : ℝ), -Complex.I * ↑↑ℏ * -((fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) a) 1 * ψ2 a)hf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 x) MeasureTheory.volumehfg'ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1) MeasureTheory.volumehfgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * ψ2 x) MeasureTheory.volumehfψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport ⇑ψ2, DifferentiableAt ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) xhgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport fun a => (starRingEnd ℂ) (ψ1 a), DifferentiableAt ℝ (⇑ψ2) x
    ← MeasureTheory.integral_neg,ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  -Complex.I * ↑↑ℏ * ∫ (a : ℝ), -((fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) a) 1 * ψ2 a)hf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 x) MeasureTheory.volumehfg'ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1) MeasureTheory.volumehfgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * ψ2 x) MeasureTheory.volumehfψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport ⇑ψ2, DifferentiableAt ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) xhgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport fun a => (starRingEnd ℂ) (ψ1 a), DifferentiableAt ℝ (⇑ψ2) xψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (a : ℝ), -Complex.I * ↑↑ℏ * -((fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) a) 1 * ψ2 a)hf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 x) MeasureTheory.volumehfg'ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1) MeasureTheory.volumehfgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * ψ2 x) MeasureTheory.volumehfψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport ⇑ψ2, DifferentiableAt ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) xhgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport fun a => (starRingEnd ℂ) (ψ1 a), DifferentiableAt ℝ (⇑ψ2) x ← MeasureTheory.integral_const_mulψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (a : ℝ), -Complex.I * ↑↑ℏ * -((fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) a) 1 * ψ2 a)hf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 x) MeasureTheory.volumehfg'ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1) MeasureTheory.volumehfgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * ψ2 x) MeasureTheory.volumehfψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport ⇑ψ2, DifferentiableAt ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) xhgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport fun a => (starRingEnd ℂ) (ψ1 a), DifferentiableAt ℝ (⇑ψ2) xψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (a : ℝ), -Complex.I * ↑↑ℏ * -((fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) a) 1 * ψ2 a)hf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 x) MeasureTheory.volumehfg'ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1) MeasureTheory.volumehfgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * ψ2 x) MeasureTheory.volumehfψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport ⇑ψ2, DifferentiableAt ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) xhgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport fun a => (starRingEnd ℂ) (ψ1 a), DifferentiableAt ℝ (⇑ψ2) x]ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (a : ℝ), -Complex.I * ↑↑ℏ * -((fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) a) 1 * ψ2 a)hf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 x) MeasureTheory.volumehfg'ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1) MeasureTheory.volumehfgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * ψ2 x) MeasureTheory.volumehfψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport ⇑ψ2, DifferentiableAt ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) xhgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport fun a => (starRingEnd ℂ) (ψ1 a), DifferentiableAt ℝ (⇑ψ2) x
  simp only [starRingEnd_apply, fderiv_star]ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∫ (x : ℝ), star ((momentumOperatorSchwartz ψ1) x) * ψ2 x =
  ∫ (a : ℝ), -Complex.I * ↑↑ℏ * -((↑(starL' ℝ) ∘SL fderiv ℝ (⇑ψ1) a) 1 * ψ2 a)hf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 x) MeasureTheory.volumehfg'ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1) MeasureTheory.volumehfgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * ψ2 x) MeasureTheory.volumehfψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport ⇑ψ2, DifferentiableAt ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) xhgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport fun a => (starRingEnd ℂ) (ψ1 a), DifferentiableAt ℝ (⇑ψ2) x
  simp [momentumOperatorSchwartz_apply, mul_assoc]hf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 x) MeasureTheory.volumehfg'ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1) MeasureTheory.volumehfgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * ψ2 x) MeasureTheory.volumehfψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport ⇑ψ2, DifferentiableAt ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) xhgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport fun a => (starRingEnd ℂ) (ψ1 a), DifferentiableAt ℝ (⇑ψ2) x
  ·hf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (fderiv ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x) 1 * ψ2 x) MeasureTheory.volume simp only [starRingEnd_apply, fderiv_star]hf'gψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (↑(starL' ℝ) ∘SL fderiv ℝ (⇑ψ1) x) 1 * ψ2 x) MeasureTheory.volume
    exact hint (SchwartzMap.derivCLM ℂ ℂ ψ1) ψ2All goals completed! 🐙
  ·hfg'ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * (fderiv ℝ (⇑ψ2) x) 1) MeasureTheory.volume exact hint ψ1 (SchwartzMap.derivCLM ℂ ℂ ψ2)All goals completed! 🐙
  ·hfgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ MeasureTheory.Integrable (fun x => (starRingEnd ℂ) (ψ1 x) * ψ2 x) MeasureTheory.volume exact hint ψ1 ψ2All goals completed! 🐙
  ·hfψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport ⇑ψ2, DifferentiableAt ℝ (fun a => (starRingEnd ℂ) (ψ1 a)) x exact fun x _ => (SchwartzMap.differentiable ψ1).star xAll goals completed! 🐙
  ·hgψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)hint:∀ (f g : 𝓢(ℝ, ℂ)), MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume⊢ ∀ x ∈ tsupport fun a => (starRingEnd ℂ) (ψ1 a), DifferentiableAt ℝ (⇑ψ2) x fun_propAll goals completed! 🐙

Momentum operator

The momentum operator on functions ℝ → ℂ

The momentum operator on Schwartz maps

Generalized eigenvectors of the momentum operator

The momentum operator is symmetric

The momentum operator on functions `ℝ → ℂ`