OAI/Combinatorics/Progressions/Estimates/EmbeddedFiniteConditioning.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights line 12
  2. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_mean line 18
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_complexMean line 23
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_weight_ne_zero line 29
  5. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_complexMean_sub_le_weight_l1 line 50
  6. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_positive_weight_norm_ge_mean line 60
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_piece_discrepancy_of_weight_l1 line 92
  8. theorem OAI.Erdos3.normalized_finite_weights_l1_le line 114
  9. theorem OAI.Erdos3.finite_weight_mass_pos_of_relative_error line 143
  10. theorem OAI.Erdos3.normalized_finite_weights_l1_relative line 154
  11. theorem OAI.Erdos3.normalized_finite_weights_pair_l1 line 170
  12. theorem OAI.Erdos3.FiniteProbabilityWeights.eq_of_weight_eq line 197
  13. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_probability line 207
  14. def OAI.Erdos3.FiniteProbabilityWeights.restrictedWeight line 214
  15. theorem OAI.Erdos3.FiniteProbabilityWeights.restrictedWeight_nonneg line 217
  16. theorem OAI.Erdos3.FiniteProbabilityWeights.restrictedWeight_total line 224
  17. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_mass line 228
  18. def OAI.Erdos3.FiniteProbabilityWeights.conditionPositiveWeights line 233
  19. theorem OAI.Erdos3.FiniteProbabilityWeights.conditionPositiveWeights_weight line 240
  20. theorem OAI.Erdos3.FiniteProbabilityWeights.conditionPositiveWeights_eq_restricted line 252
  21. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_complexMean_equiv line 274
  22. theorem OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_mean_equiv line 287
  23. def OAI.Erdos3.finiteEmbeddingRange line 306
  24. theorem OAI.Erdos3.sum_finiteEmbeddingRange line 308
  25. def OAI.Erdos3.finiteEmbeddingRangeEquiv line 312
  26. theorem OAI.Erdos3.FiniteProbabilityWeights.total_pos_of_embedding line 324
  27. theorem OAI.Erdos3.FiniteProbabilityWeights.conditionPositiveWeights_complexMean line 330
  28. def OAI.Erdos3.FiniteProbabilityWeights.conditionAlongEmbedding line 340
  29. theorem OAI.Erdos3.FiniteProbabilityWeights.conditionAlongEmbedding_complexMean line 346
  30. theorem OAI.Erdos3.FiniteProbabilityWeights.conditionAlongEmbedding_mean line 353
  31. theorem OAI.Erdos3.FiniteProbabilityWeights.uniform_condition_embedding_mean line 360