OAI/NumberTheory/TwoPointCorrelations/HalaszTwistedMean.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Height translation for the ordinary mean estimate. This is the form applied to Dirichlet polynomials on a vertical line.

  1. lemma OAI.TwoPointCorrelations.halasz_twist_add line 13

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszTwistedMean.lean:13 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_twist_mul line 17

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszTwistedMean.lean:17 (same declaration text).

  3. def OAI.TwoPointCorrelations.halaszTwistedFunction line 24

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszTwistedMean.lean:24 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_twisted_one line 27

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszTwistedMean.lean:27 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_twisted_mul line 30

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszTwistedMean.lean:30 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.halasz_twisted_oneBounded line 37

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszTwistedMean.lean:37 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.halasz_twisted_distance line 43

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszTwistedMean.lean:43 (same declaration text).

  8. theorem OAI.TwoPointCorrelations.halasz_twisted_mean_value line 51

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszTwistedMean.lean:51 (same declaration text).