OAI/NumberTheory/JointDickman/Probability/SignedSplitProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The signed fair-split product law used by the kernel

  1. def OAI.JointDickman.splitProductMass line 12
  2. def OAI.JointDickman.signedSplitProductMass line 15
  3. theorem OAI.JointDickman.splitProductMass_nonneg line 19
  4. theorem OAI.JointDickman.signedSplitProductMass_one line 27
  5. theorem OAI.JointDickman.signedSplitProductMass_abs_le line 42
  6. theorem OAI.JointDickman.signedSplitProductMass_coefficient_bound line 65