Phase Mixing and Recoverable Information

Exact root statement

∀ (epsilon : ℝ),
  0 < epsilon →
    ∃ turn,
      0 < turn ∧
        (∀ (elapsed position : ℝ), (reversedPair turn).NonvacuousVlasovPoissonAt elapsed position) ∧
          (∀ (position : ℝ), |(∫ (velocity : ℝ), afterVelocityReversal turn 0 position velocity) - 1| < epsilon) ∧
            (∀ (position velocity : ℝ),
                afterVelocityReversal turn turn position velocity =
                  PlasmaPhysics.phaseSpaceDensity 0 position velocity) ∧
              |(∫ (velocity : ℝ), afterVelocityReversal turn turn 0 velocity) - 1| = 1 / 2