OAI/NumberTheory/TwoPoint/Halasz/HalaszPhaseIntegral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact primitive of the Archimedean phase, including the zero endpoint.

  1. lemma OAI.TwoPointCorrelations.halasz_power_phase_eq_cpow line 11

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

  2. lemma OAI.TwoPointCorrelations.halasz_power_phase_cpow_primitive line 20

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPhaseIntegral.lean:20 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_power_phase_integral line 33

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPhaseIntegral.lean:33 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_power_phase_intervalIntegrable line 47

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPhaseIntegral.lean:47 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_power_phase_integral_norm line 55

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