OAI/NumberTheory/JointDickman/Probability/WeightedFirstMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A positive first moment for weights equal to one on the interior rectangle

  1. theorem OAI.JointDickman.fairRegularAmplificationAt_nonneg line 14
  2. theorem OAI.JointDickman.independentWeighted_first_identity line 29
  3. theorem OAI.JointDickman.interior_mass_le_weighted_first line 73
  4. theorem OAI.JointDickman.independentWeighted_first_lower line 90