OAI/NumberTheory/Ostmann/Characters/QuartetOrientedValue.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.orientedPairBase line 11
2. def OAI.Ostmann.quartetLeftParameter line 14
3. def OAI.Ostmann.quartetRightParameter line 20
4. theorem OAI.Ostmann.quartet_left_oriented_value line 28

   Source documentation

   Both choices on the left use the same child difference and exactly the friendly/bad parameter table of the Fourier calculation.

   theorem quartet_left_oriented_value {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
       (V XL XR m₁ m₂ m₃ m₄ : (ZMod p)ˣ) (friendly : Bool) :
       fieldBottomPairValue g (rationalTreeArgument Q.sL (Q.u * Q.CL) D V XL (m₁ * m₂))
         (((Q.s₁ / Q.s₂) * ((XL * Q.C₂ * m₂) / (V * Q.C₁ * m₁)) : (ZMod p)ˣ) : ZMod p) =
       fieldBottomPairValue (orientedPairBase g friendly)
         (rationalTreeArgument Q.sL (Q.u * Q.CL) D V XL (m₁ * m₂))
         (quartetLeftRatio friendly
           (quartetLeftParameter D Q XL XR ((m₁ * m₂) * (m₃ * m₄)) friendly m₁ m₂)
           (rationalTreeArgument Q.sL (Q.u * Q.CL) D V XL (m₁ * m₂))
           (rationalTreeArgument Q.sR (Q.u * Q.CR) D V XR (m₃ * m₄))) := by
   …

   Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.fieldBottomPairValue, OAI.Ostmann.rationalTreeArgument, OAI.Ostmann.orientedPairBase, OAI.Ostmann.quartetLeftRatio, OAI.Ostmann.quartetLeftParameter

5. theorem OAI.Ostmann.quartet_right_oriented_value line 53
6. theorem OAI.Ostmann.rationalQuartetValue_oriented line 81

   Source documentation

   All four orientation rows identify the actual local diagram, including its zero at an invalid reconstruction, with the same ratio function whose coefficient bounds were proved above.

   theorem rationalQuartetValue_oriented {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
       (XL XR m₁ m₂ m₃ m₄ : (ZMod p)ˣ) (left right : Bool) :
       rationalQuartetValue g D Q XL XR m₁ m₂ m₃ m₄ =
         quartetRatioValue (orientedPairBase g left) (orientedPairBase g right) left right
           (rationalTreeArgument Q.s (Q.CL * Q.CR) D XL XR ((m₁ * m₂) * (m₃ * m₄)))
           (quartetLeftParameter D Q XL XR ((m₁ * m₂) * (m₃ * m₄)) left m₁ m₂)
           (quartetRightParameter D Q XL XR ((m₁ * m₂) * (m₃ * m₄)) right m₃ m₄)
           ((Q.sL / Q.sR) * ((XR * Q.CR * (m₃ * m₄)) / (XL * Q.CL * (m₁ * m₂)))) := by
   …

   Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.rationalQuartetValue, OAI.Ostmann.quartetRatioValue, OAI.Ostmann.orientedPairBase, OAI.Ostmann.rationalTreeArgument, OAI.Ostmann.quartetLeftParameter, OAI.Ostmann.quartetRightParameter