import PhysicsLogic.Framework.LowEnergyEffectiveRangeReduction

open Filter PhysicsLogic.Framework.EffectiveRangeExpansion
open scoped Topology

example (phase : Real -> Real) (constant quadratic : Real) :
    HasFirstTwoCoefficients phase constant quadratic =
      Tendsto (fun momentum => (phase momentum - constant) / momentum ^ 2)
        (nhdsWithin 0 (Set.Ioi 0)) (𝓝 quadratic) := rfl

-- The whole reduced specification, without project-defined predicates on
-- the readable side. The radius and coefficient precede the momentum.
example (phase : Real -> Real) (inverseLength effectiveRange : Real) :
    NonvacuousEffectiveRangeExpansionAt phase inverseLength effectiveRange ↔
      ∃ radius coefficient : Real, 0 < radius ∧ 0 ≤ coefficient ∧
        ∀ momentum : Real, 0 < momentum -> momentum < radius ->
          |phase momentum - (-inverseLength + effectiveRange / 2 * momentum ^ 2)| ≤
            coefficient * momentum ^ 4 := Iff.rfl