OAI/NumberTheory/JointDickman/Amplification/ConditionedRootFluctuation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The site-conditioned auxiliary roots have vanishing fluctuations

  1. def OAI.JointDickman.averagedConditionedRootError line 13
  2. theorem OAI.JointDickman.averagedConditionedRootError_bound line 24