OAI/NumberTheory/JointDickman/Amplification/ConditionedRootTests.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Transferring bounded tests to independent auxiliary roots

  1. theorem OAI.JointDickman.finiteExpectation_abs_bound line 12
  2. theorem OAI.JointDickman.finiteExpectation_difference_l1 line 21
  3. theorem OAI.JointDickman.siteConditionedRoot_test line 35
  4. theorem OAI.JointDickman.averaged_siteConditionedRoot_test line 53