OAI/NumberTheory/TwoPoint/Bounds/CoordinateFiberSum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Sum one coordinate first, retaining the weighted sum of all other coordinates.

  1. def OAI.TwoPointCorrelations.outsideCoordinate line 12
  2. lemma OAI.TwoPointCorrelations.update_eq_of_outside_eq line 15
  3. theorem OAI.TwoPointCorrelations.coordinate_fiber_sum_bound line 25