OAI/NumberTheory/TwoPoint/Bounds/ComplexNumericalEdges.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transfer the existing positive deletion costs to arbitrary complex factors. Liouville's unit values serve only as an exact algebraic change of test functions.

  1. def OAI.TwoPointCorrelations.liouvilleUntwist line 14
  2. lemma OAI.TwoPointCorrelations.liouvilleUntwist_norm_le line 17
  3. lemma OAI.TwoPointCorrelations.liouvilleUntwist_cancel line 31
  4. lemma OAI.TwoPointCorrelations.retainedComplexPrimeEdge_eq_untwist line 44
  5. lemma OAI.TwoPointCorrelations.uncutNumericalEdge_untwist line 59
  6. lemma OAI.TwoPointCorrelations.complex_uncut_sub_retained_edge_le line 72