OAI/NumberTheory/JointDickman/Amplification/FairAverageContraction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The conditional fair-split average contracts squared error

  1. theorem OAI.JointDickman.finite_probability_square_le line 9
  2. theorem OAI.JointDickman.fairSplitAverage_square_le line 18
  3. theorem OAI.JointDickman.fairSplitAverage_sub line 24
  4. theorem OAI.JointDickman.fairSplitAverage_square_error line 29