OAI/NumberTheory/JointDickman/Probability/WeightedKernelCutoff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Removing a bounded weight only discards the low-exclusive union

  1. def OAI.JointDickman.weightedDiscardedMass line 14
  2. theorem OAI.JointDickman.weightedDiscardedMass_eq line 19
  3. theorem OAI.JointDickman.weightedDiscardedMass_nonneg line 34
  4. theorem OAI.JointDickman.weightedDiscardedMass_le_lowUnion line 52
  5. def OAI.JointDickman.weightedDiscardedKernel line 81
  6. theorem OAI.JointDickman.weightedDiscardedKernel_nonneg line 85
  7. theorem OAI.JointDickman.weightedDiscardedKernel_le_lowUnion line 92