OAI/NumberTheory/Ostmann/Tree/RationalPairValue.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact bottom-pair identification in a reconstructed rational tree

  1. theorem OAI.Ostmann.rationalTreeAmplitude_pair line 14

    Source documentation

    A bottom node with the usual alternating conjugation is exactly the pair function used in the Fourier and Mellin estimates, including invalid nodes.

    theorem rationalTreeAmplitude_pair {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (D s sL sR CL CR u XL XR mL mR : (ZMod p)ˣ) :
    rationalTreeAmplitude g D
      (.node s CL CR u (.leaf sL (u * CL)) (.leaf sR (u * CR)))
      XL XR (false, true) (mL, mR) =
      fieldBottomPairValue g
        (rationalTreeArgument s (CL * CR) D XL XR (mL * mR))
        (((sL / sR) * ((XR * CR * mR) / (XL * CL * mL)) : (ZMod p)ˣ) : ZMod p) := by
…

    Mentions: OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.fieldBottomPairValue, OAI.Ostmann.rationalTreeArgument