OAI/NumberTheory/TwoPoint/Bounds/BinCutoffGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal logarithmic bin places T/(dq) between X exp(-eta) and X. Floor normalization introduces a scalar of norm at most one.

  1. lemma OAI.TwoPointCorrelations.actualPaddingBin_cutoff line 11
  2. lemma OAI.TwoPointCorrelations.floor_cutoff_weight_norm_le line 44