OAI/NumberTheory/JointDickman/Amplification/FiniteWeightedUnion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nonnegative weights on finite unions

  1. theorem OAI.JointDickman.sum_union_le_nonneg line 10
  2. theorem OAI.JointDickman.sum_biUnion_le_nonneg line 17