OAI/NumberTheory/JointDickman/Amplification/FiniteHitMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite subset laws controlled by their hit probabilities

  1. theorem OAI.JointDickman.finitePushMass_probability line 12
  2. theorem OAI.JointDickman.finiteHitMass_l1_point line 19
  3. theorem OAI.JointDickman.finiteHitMass_l1_le_marginals line 45