OAI/NumberTheory/TwoPoint/Bounds/PositiveNormalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Setting the unused value at zero to zero permits globally bounded graph test vectors without changing any of the theorem's positive correlations.

  1. def OAI.TwoPointCorrelations.positiveNormalization line 14
  2. lemma OAI.TwoPointCorrelations.positiveNormalization_eq line 17
  3. lemma OAI.TwoPointCorrelations.positiveNormalization_norm line 21
  4. lemma OAI.TwoPointCorrelations.Multiplicative.positiveNormalization line 28
  5. lemma OAI.TwoPointCorrelations.UniformlyNonpretentious.positiveNormalization line 35
  6. lemma OAI.TwoPointCorrelations.positiveNormalization_prefix line 42
  7. lemma OAI.TwoPointCorrelations.correlationSum_eq_positivePrefix line 51