import BohmObservableChallenges

set_option autoImplicit false
open MeasureTheory
open PhysicsLogic.Papers.Bohm1952.StationaryGaussianOscillator
open PhysicsLogic.Framework
open PhysicsLogic.Philosophy.MathematicsAndNature
open BohmObservableChallenges

example (t x : Real) : momentumWave t x = -Complex.I * deriv (wave t) x := rfl

example (t : Real) : operatorKineticExpectation t =
    (1 / 2 : Real) * ∫ x : Real, Complex.normSq (momentumWave t x) := rfl

example (t : Real) : guidingKineticExpectation t =
    ∫ x : Real, guidanceVelocity t x ^ 2 / 2
      ∂GuidedDensityTransport.bornMeasure volume (wave t) := rfl

example : kineticInterpretation =
    ({ physicallyHasValueAt := fun _ t _ v _ => v = guidingKineticExpectation t
       mathematicalStateAdmissibleAt := fun _ _ => True
       mathematicalQuantityAdmissibleAt := fun _ _ => True
       representsStateAt := fun t s _ _ => t = s
       representsQuantityAt := fun _ _ _ _ => True
       assignsValueAt := fun _ t v _ => v = operatorKineticExpectation t
       representsValueAt := fun v w _ _ _ => v = w } :
      QuantityRepresentationContext Unit Real Real Unit Unit Real Real Unit) := rfl