OAI/NumberTheory/Ostmann/Characters/QuartetOrientations.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The four quartet orientation formulas

A friendly side uses its own difference, and a bad side uses the reciprocal of the other difference. The twists below are exactly the four rows in tree-twisted-convolution.

  1. def OAI.Ostmann.quartetLeftRatio line 20
  2. def OAI.Ostmann.quartetRightRatio line 23
  3. def OAI.Ostmann.quartetLeftTwist line 26
  4. def OAI.Ostmann.quartetRightTwist line 30
  5. def OAI.Ostmann.quartetParameterValue line 34
  6. theorem OAI.Ostmann.quartetParameterValue_eq_synthesis line 42
  7. theorem OAI.Ostmann.quartetParameterValue_parseval line 73

    Source documentation

    All orientation choices have precisely the two-twist Fourier norm.

    theorem quartetParameterValue_parseval {p : ℕ} [Fact p.Prime]
    (g h : ZMod p → ℂ) (left right : Bool) (ν : MulChar (ZMod p) ℂ) :
    (p : ℝ)⁻¹ * (∑ y : ZMod p,
      (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * (∑ z : (ZMod p)ˣ,
        (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ *
          ∑ t : (ZMod p)ˣ, ‖quartetParameterValue g h left right ν y z t‖ ^ 2)) =
      ∑ χ : MulChar (ZMod p) ℂ, ∑ ψ : MulChar (ZMod p) ℂ, ∑ a : ZMod p,
        ‖additiveFourier (fun d => pairAutocorrelation g χ d *
          quartetLeftTwist left right ν χ ψ d) a‖ ^ 2 *
        ‖additiveFourier (fun e => pairAutocorrelation h ψ e *
          quartetRightTwist left right ν χ ψ e) (-a)‖ ^ 2 := by
…

    Mentions: OAI.Ostmann.quartetParameterValue, OAI.Ostmann.additiveFourier, OAI.Ostmann.pairAutocorrelation, OAI.Ostmann.quartetLeftTwist, OAI.Ostmann.quartetRightTwist