BottomPairMellin.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The bottom-pair Mellin coefficient is an autocorrelation

This is equation tree-P-definition. The difference parameter is a unit; the exceptional ratio t = 1 is assigned value zero. The function being correlated is twisted by the conjugate multiplicative character.

theorem OAI.Ostmann.sum_units_of_zero line 19
def OAI.Ostmann.ratioInvolution line 37
Source documentation
The fractional-linear involution exchanges the two exceptional points with themselves, making it a permutation of the entire finite field.
```
noncomputable def ratioInvolution {p : ℕ} [Fact p.Prime] (t : ZMod p) : ZMod p :=
…
```
theorem OAI.Ostmann.ratioInvolution_involutive line 40
def OAI.Ostmann.bottomPairValue line 56
Source documentation
Bottom-pair value with difference d and ratio t, zero at the singular ratio.
```
noncomputable def bottomPairValue {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (d t : (ZMod p)ˣ) : ℂ :=
…
```

def OAI.Ostmann.characterTwist line 63

Source documentation

The multiplicative twist appearing in the autocorrelation formula.

noncomputable def characterTwist {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (χ : MulChar (ZMod p) ℂ) (x : ZMod p) : ℂ :=
…

theorem OAI.Ostmann.twisted_pair_identity line 67

theorem OAI.Ostmann.bottomPair_mellin_sum line 95

Source documentation

Reindex the unnormalized bottom-pair Mellin sum as a full-field correlation.

theorem bottomPair_mellin_sum {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (d : (ZMod p)ˣ) (χ : MulChar (ZMod p) ℂ) :
    (∑ t : (ZMod p)ˣ, bottomPairValue g d t * conj (χ t)) =
      ∑ x : ZMod p, characterTwist g χ x * conj (characterTwist g χ (x - d)) := by
…

Mentions: OAI.Ostmann.bottomPairValue, OAI.Ostmann.characterTwist

theorem OAI.Ostmann.bottomPair_mellin_autocorrelation line 130

Source documentation

Equation tree-P-definition, with the paper's two probability normalizations.

theorem bottomPair_mellin_autocorrelation {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (d : (ZMod p)ˣ) (χ : MulChar (ZMod p) ℂ) :
    mellinCoefficient (bottomPairValue g d) χ =
      (p : ℂ) / (Fintype.card (ZMod p)ˣ : ℂ) *
        additiveAutocorrelation (characterTwist g χ) (d : ZMod p) := by
…

Mentions: OAI.Ostmann.mellinCoefficient, OAI.Ostmann.bottomPairValue, OAI.Ostmann.additiveAutocorrelation, OAI.Ostmann.characterTwist