OAI/NumberTheory/TwoPoint/Bounds/FinitePrimePhases.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The Fourier twists used in qualitative analytic centering count distinct prime divisors, rather than their multiplicities. Their multiplicativity is therefore asserted only for coprime arguments.

  1. def OAI.TwoPointCorrelations.finitePrimeDivisorCount line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FinitePrimePhases.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.finitePrimeDivisorCount_mul line 17

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FinitePrimePhases.lean:17 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.finitePrimeDivisorCount_prime_outside line 32

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FinitePrimePhases.lean:32 (same declaration text).

  4. def OAI.TwoPointCorrelations.finitePrimePhase line 43

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FinitePrimePhases.lean:43 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.norm_finitePrimePhase line 46

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FinitePrimePhases.lean:46 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.finitePrimePhase_mul line 49

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FinitePrimePhases.lean:49 (same declaration text).

  7. def OAI.TwoPointCorrelations.twistByPrimePhase line 55

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FinitePrimePhases.lean:55 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.Multiplicative.twistByPrimePhase line 58

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FinitePrimePhases.lean:58 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.OneBounded.twistByPrimePhase line 66

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FinitePrimePhases.lean:66 (same declaration text).

  10. lemma OAI.TwoPointCorrelations.twistByPrimePhase_prime_outside line 72

    Also declared: OAI/NumberTheory/TwoPointCorrelations/FinitePrimePhases.lean:72 (same declaration text).