OAI/Combinatorics/Progressions/FixedDensity/ConfigurationWeightedDefect.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.OrderedCoarseFineComplex.coarseDiagonal line 11
  2. def OAI.Erdos3.FixedDensity.mixedConfigurationCoarseDensity line 20
  3. def OAI.Erdos3.FixedDensity.mixedConfigurationFineDensity line 34
  4. def OAI.Erdos3.FixedDensity.mixedConfigurationDefect line 49
  5. def OAI.Erdos3.FixedDensity.mixedConfigurationUniform line 59
  6. def OAI.Erdos3.FixedDensity.mixedConfigurationBoundaryIndicator line 69
  7. theorem OAI.Erdos3.FixedDensity.mixedConfigurationCoarseDensity_nonneg line 84
  8. theorem OAI.Erdos3.FixedDensity.mixedConfigurationCoarseDensity_le_one line 94
  9. theorem OAI.Erdos3.FixedDensity.mixedConfigurationBoundaryIndicator_nonneg line 104
  10. theorem OAI.Erdos3.FixedDensity.mixedConfigurationBoundaryIndicator_le_one line 114
  11. theorem OAI.Erdos3.FixedDensity.mixedConfigurationFaceWeight_decompose line 124
  12. theorem OAI.Erdos3.FixedDensity.coarse_boundary_mem_of_coarse_configuration_weight_ne_zero line 138
  13. theorem OAI.Erdos3.FixedDensity.mixedConfigurationBoundaryIndicator_mul_remainder line 160
  14. theorem OAI.Erdos3.FixedDensity.partialConfigurationCount_mixed_decompose line 179
  15. def OAI.Erdos3.FixedDensity.IsFullyMixedPreliminaryOrderedRegular line 213
  16. theorem OAI.Erdos3.FixedDensity.ClosedOrderedAtomConfiguration.IsMixedGood.atPositiveFace line 224
  17. theorem OAI.Erdos3.FixedDensity.mixedConfigurationFace_isFaceCutRegular line 243
  18. theorem OAI.Erdos3.FixedDensity.mixedConfigurationContribution_uniform_eq_mean_faceCutCorrelation line 266
  19. theorem OAI.Erdos3.FixedDensity.abs_mixedConfigurationContribution_uniform_le line 301
  20. theorem OAI.Erdos3.FixedDensity.isFullyMixedPreliminaryOrderedRegular_of_fine line 353
  21. theorem OAI.Erdos3.FixedDensity.abs_mixedConfigurationContribution_uniform_le_of_fine line 372
  22. theorem OAI.Erdos3.FixedDensity.mixedConfigurationDefect_mul_boundaryIndicator line 400
  23. theorem OAI.Erdos3.FixedDensity.mean_sq_mixedConfigurationDefect_mul_boundaryIndicator line 454
  24. theorem OAI.Erdos3.FixedDensity.mixedConfigurationContribution_defect_eq_localized line 484
  25. theorem OAI.Erdos3.FixedDensity.mixedConfigurationContribution_defect_sq_le line 507
  26. theorem OAI.Erdos3.FixedDensity.abs_mixedConfigurationContribution_defect_le line 609
  27. theorem OAI.Erdos3.FixedDensity.abs_partialConfigurationCount_sub_mixedDensity_mul_le line 640
  28. theorem OAI.Erdos3.FixedDensity.abs_partialConfigurationCount_sub_mixedDensity_mul_le_of_fine line 699
  29. def OAI.Erdos3.FixedDensity.mixedExtendedConfigurationCount line 735
  30. theorem OAI.Erdos3.FixedDensity.mixedExtendedConfigurationCount_empty line 749
  31. theorem OAI.Erdos3.FixedDensity.mixedExtendedConfigurationCount_univ line 759
  32. theorem OAI.Erdos3.FixedDensity.mixedConfigurationCoarseDensity_lower line 770
  33. theorem OAI.Erdos3.FixedDensity.mixedExtendedConfigurationCount_step_rankwise line 781
  34. theorem OAI.Erdos3.FixedDensity.mixedFullConfigurationCount_lower_bound_rankwise line 883
  35. theorem OAI.Erdos3.FixedDensity.mixedFullConfigurationCount_pos_rankwise line 962
  36. theorem OAI.Erdos3.FixedDensity.mixedFullConfigurationCount_lower_bound_of_fine line 989
  37. theorem OAI.Erdos3.FixedDensity.mixedFullConfigurationCount_pos_of_fine line 1028
  38. theorem OAI.Erdos3.FixedDensity.configurationFaceWeight_sq line 1069
  39. theorem OAI.Erdos3.FixedDensity.partialConfigurationWeight_sq line 1080
  40. theorem OAI.Erdos3.FixedDensity.mean_sq_partialConfigurationWeight_eq_count line 1096
  41. theorem OAI.Erdos3.FixedDensity.partialConfigurationCount_nonneg line 1110
  42. theorem OAI.Erdos3.FixedDensity.mean_sq_mixedConfigurationDefect_localized_le line 1121
  43. theorem OAI.Erdos3.FixedDensity.mixedConfigurationContribution_defect_sq_le_mul_count line 1193
  44. theorem OAI.Erdos3.FixedDensity.abs_mixedConfigurationContribution_defect_le_sqrt_mul_count line 1248
  45. theorem OAI.Erdos3.FixedDensity.abs_partialConfigurationCount_sub_mixedDensity_mul_le_sqrt line 1282