OAI/NumberTheory/TwoPoint/Bounds/TraceErrorAbsorption.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The three exceptional trace classes are absorbed by an absolute change of the square-root harmonic-mass constant.

  1. lemma OAI.TwoPointCorrelations.eventually_trace_exceptional_cost line 12
  2. lemma OAI.TwoPointCorrelations.trace_base_double_absorbs_one line 46
  3. theorem OAI.TwoPointCorrelations.eventually_trace_absorption line 74