OAI/NumberTheory/Ostmann/Arithmetic/CompensationEqualityPatternsSources.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.commonCandidates line 12
  2. abbrev OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.CommonSample line 15
  3. abbrev OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.IndependentSamples line 18
  4. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.sourceEmbed line 21
  5. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.tupleEmbed line 25
  6. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.tupleEmbed_injective line 30
  7. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.sourceWeight line 37
  8. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.sourceWeight_embed line 43
  9. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.sourceWeight_nonneg line 50
  10. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.source_sum_eq_common line 57
  11. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.source_cmean_eq_patterns line 82
  12. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.commonSample_prime line 96
  13. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.source_product_by_multiplicity line 102