QuartetFriendlyCoordinates.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The two-friendly orientation of an actual rational quartet

theorem OAI.Ostmann.pair_ratio_friendly line 12
def OAI.Ostmann.quartetLeftHeld line 22
def OAI.Ostmann.quartetRightHeld line 26
def OAI.Ostmann.quartetMovingMultiplier line 30
theorem OAI.Ostmann.quartet_friendly_product line 35
Source documentation
Reciprocal coordinates on the two moving leaves preserve the quartet product.
```
theorem quartet_friendly_product {G : Type*} [CommGroup G] (P a b r : G) :
    (r⁻¹ * a) * (P * r / (a * b) * b) = P := by
…
```

theorem OAI.Ostmann.quartet_friendly_ratio line 44

Source documentation

The ratio at the quartet root is a fixed multiple of the moving square.

theorem quartet_friendly_ratio {p : ℕ} [Fact p.Prime]
    (Q : RationalQuartetData (ZMod p)ˣ) (XL XR P a b r : (ZMod p)ˣ) :
    (Q.sL / Q.sR) * ((XR * Q.CR * (P * r / (a * b) * b)) /
      (XL * Q.CL * (r⁻¹ * a))) = quartetMovingMultiplier Q XL XR P a * r ^ 2 := by
…

Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.quartetMovingMultiplier

theorem OAI.Ostmann.rationalQuartetValue_friendly line 56

Source documentation

The actual depth-two diagram, with residual entries held on both sides, is exactly the quartet ratio function used in the coefficient majorant.

theorem rationalQuartetValue_friendly {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
    (XL XR P a b r : (ZMod p)ˣ) :
    rationalQuartetValue g D Q XL XR r⁻¹ a (P * r / (a * b)) b =
      quartetRatioValue g g true true
        (rationalTreeArgument Q.s (Q.CL * Q.CR) D XL XR P)
        (quartetLeftHeld D Q XL * a ^ 2) (quartetRightHeld D Q XR * b ^ 2)
        (quartetMovingMultiplier Q XL XR P a * r ^ 2) := by
…

Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.rationalQuartetValue, OAI.Ostmann.quartetRatioValue, OAI.Ostmann.rationalTreeArgument, OAI.Ostmann.quartetLeftHeld, OAI.Ostmann.quartetRightHeld, OAI.Ostmann.quartetMovingMultiplier