OAI/Analysis/CircleDomains/Probability/SparseTupleMeasure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite individual tuple costs suffice for arbitrarily small total cost after an injective reassignment of slots. No summability of the original weighted tuple costs is required.

  1. theorem OAI.CircleDomainRigidity.lintegral_weightedTupleMeasure line 18
  2. theorem OAI.CircleDomainRigidity.lintegral_weightedTupleMeasure_sparse line 24
  3. theorem OAI.CircleDomainRigidity.slotWeight_antitone line 40
  4. theorem OAI.CircleDomainRigidity.exists_sparse_weighted_sum_le line 44
  5. theorem OAI.CircleDomainRigidity.exists_sparse_tuple_cost_le line 69