import PhysicsLogic.Papers.KaplanSavageWise1998.PionAmplitudeJet

set_option autoImplicit false
open PhysicsLogic.Papers.KaplanSavageWise1998

example (M p : Real) (a : Complex × Complex) :
    PionAmplitudeJet.retainedScatteringReadout M p a =
      (1 + 2 * Complex.I * ((M / (4 * Real.pi) * p : Real) : Complex) * a.1,
       ((M / (4 * Real.pi) * p : Real) : Complex) * a.2 /
         (1 + 2 * Complex.I * ((M / (4 * Real.pi) * p : Real) : Complex) * a.1)) := rfl

-- The first component has the paper's i M p/(2 pi) normalization.
example (M p : Real) (a : Complex × Complex) :
    (PionAmplitudeJet.retainedScatteringReadout M p a).1 =
      1 + Complex.I * ((M * p / (2 * Real.pi) : Real) : Complex) * a.1 := by
  dsimp [PionAmplitudeJet.retainedScatteringReadout]
  push_cast
  ring

example (j : PionAmplitudeJet) (m p : Real) : j.graphII m p =
    ((j.couplings.axialCoupling ^ 2 / (2 * j.couplings.pionDecayConstant ^ 2) : Real) : Complex) *
      (-1 + ((m ^ 2 / (4 * p ^ 2) : Real) : Complex) *
        (Real.log (1 + 4 * p ^ 2 / m ^ 2) : Complex)) := rfl

example (j : PionAmplitudeJet) (m p mu : Real) : j.graphIII m p mu =
    ((j.couplings.axialCoupling ^ 2 / j.couplings.pionDecayConstant ^ 2 : Real) : Complex) *
      (((m * j.couplings.mass / (4 * Real.pi) : Real) : Complex) * j.leadingCoefficient p mu) *
      (-((mu : Complex) + Complex.I * (p : Complex)) / (m : Complex) +
        ((m / (2 * p) : Real) : Complex) *
          ((Real.arctan (2 * p / m) : Complex) +
            Complex.I / 2 * (Real.log (1 + 4 * p ^ 2 / m ^ 2) : Complex))) := rfl

example (j : PionAmplitudeJet) (m p mu : Real) : j.firstCoefficient m p mu =
    -(j.firstC0 mu : Complex) / j.couplings.pionDiagramDenominator mu p ^ 2 -
      ((j.couplings.c2 mu * p ^ 2 : Real) : Complex) / j.couplings.pionDiagramDenominator mu p ^ 2 +
      j.graphII m p + j.graphIII m p mu + j.couplings.twoLoopPionAmplitude m mu p +
      j.couplings.dressedMassInsertion m mu p (j.couplings.d2 mu) := rfl

example (j : PionAmplitudeJet) : j.withoutMassInsertion =
    ({ j with couplings := { j.couplings with d2 := fun _ => 0 } } : PionAmplitudeJet) := rfl

example (j : PionAmplitudeJet) (s d : Real) : j.withSubleadingContacts s d =
    ({ couplings := { j.couplings with d2 := fun _ => d }
       firstC0 := fun _ => s } : PionAmplitudeJet) := rfl

example (j : PionAmplitudeJet) (m p : Real) (scales : Set Real) :
    j.AdmissibleOn m p scales =
      (j.couplings.PhysicalAt ∧ 0 < m ∧ 0 < p ∧
        ∀ mu ∈ scales, 0 < mu) := rfl

example (j : PionAmplitudeJet) (mu : Real) : j.RunsAt mu =
    (HasDerivAt j.couplings.c0 (j.couplings.mass / (4 * Real.pi) * j.couplings.c0 mu ^ 2) mu ∧
    HasDerivAt j.firstC0
      (2 * (j.couplings.mass / (4 * Real.pi)) * j.couplings.c0 mu * j.firstC0 mu +
        (j.couplings.mass / (4 * Real.pi)) * j.couplings.c0 mu *
          (j.couplings.axialCoupling ^ 2 / j.couplings.pionDecayConstant ^ 2)) mu ∧
    HasDerivAt j.couplings.c2
      (2 * (j.couplings.mass / (4 * Real.pi)) * j.couplings.c0 mu * j.couplings.c2 mu) mu ∧
    HasDerivAt j.couplings.d2
      (2 * (j.couplings.mass / (4 * Real.pi)) * j.couplings.c0 mu * j.couplings.d2 mu +
        j.couplings.pionLogCountertermSlope mu / mu) mu) := rfl

example (j : PionAmplitudeJet) (m p mu : Real) : (j.firstPhaseIncrement m p mu) =
    ((j.couplings.mass / (4 * Real.pi) * p : Real) : Complex) * j.firstCoefficient m p mu /
      (1 + 2 * Complex.I * ((j.couplings.mass / (4 * Real.pi) * p : Real) : Complex) *
        j.leadingCoefficient p mu) := rfl