OAI/NumberTheory/TwoPointCorrelations/HalaszPhaseCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Unit cells for the elementary power-sum approximation. Centering the cells cancels the linear phase error, leaving a summable quadratic error.

  1. def OAI.TwoPointCorrelations.halaszPowerPhase line 14

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPhaseCells.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_power_phase_norm line 17

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

  3. lemma OAI.TwoPointCorrelations.halasz_power_phase_add line 20

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPhaseCells.lean:20 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_power_phase_cell_error line 29

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPhaseCells.lean:29 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_power_phase_continuousOn line 65

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPhaseCells.lean:65 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.halasz_power_phase_cell_integral line 74

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPhaseCells.lean:74 (same declaration text).