OAI/NumberTheory/TwoPoint/Halasz/HalaszDenominatorCalculus.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Calculus for the variable denominator in the second prime convolution.

  1. def OAI.TwoPointCorrelations.halaszDenominatorWeight line 11

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszDenominatorCalculus.lean:11 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_log_gap_pos line 14

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

  3. lemma OAI.TwoPointCorrelations.halasz_denominator_hasDerivAt line 17

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

  4. lemma OAI.TwoPointCorrelations.halasz_denominator_primitive line 26

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszDenominatorCalculus.lean:26 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_denominator_deriv_continuous line 36

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszDenominatorCalculus.lean:36 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.halasz_denominator_integral line 49

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