import PhysicsLogicConsumer.PlasmaPhysics

open PhysicsLogicConsumer.PlasmaPhysics PhysicsLogicConsumer.PhaseMixingRecovery
open PhysicsLogic.Framework.ElectrostaticKinetic

example (v : Real) : velocityProfile v = Real.exp (-Real.pi * v ^ 2) := rfl
example (t v : Real) : mode t v =
    freeStreamingAmplitude (2 * Real.pi) (fun w => (velocityProfile w : Complex)) t v := rfl
example (t x v : Real) : phaseSpaceDensity t x v =
    velocityProfile v * (1 + (1 / 2 : Real) * Real.cos (2 * Real.pi * (x - v * t))) := rfl
example (species : Fin 2) : neutralPair.particle species =
    (⟨if species = 0 then -1 else 1, 1⟩ : Species) := rfl
example (species : Fin 2) : neutralPair.density species = phaseSpaceDensity := rfl
example (t x : Real) : neutralPair.potential t x = 0 := rfl
example (x : Real) : neutralPair.fixedChargeDensity x = 0 := rfl
example : fixedIonProbe.particle = (⟨-1, 1⟩ : Species) := rfl
example : fixedIonProbe.waveNumber = 2 * Real.pi := rfl
example : fixedIonProbe.equilibrium = velocityProfile := rfl
example : fixedIonProbe.distribution = mode := rfl
example (t : Real) : fixedIonProbe.potential t = 0 := rfl
example (turn elapsed x v : Real) : afterVelocityReversal turn elapsed x v =
    phaseSpaceDensity turn (x - v * elapsed) (-v) := rfl
example (turn : Real) : (reversedPair turn).particle = neutralPair.particle := rfl
example (turn : Real) (species : Fin 2) :
    (reversedPair turn).density species = afterVelocityReversal turn := rfl
example (turn elapsed x : Real) : (reversedPair turn).potential elapsed x = 0 := rfl
example (turn x : Real) : (reversedPair turn).fixedChargeDensity x = 0 := rfl