OAI/Combinatorics/Progressions/Estimates/CoefficientSliceEmbedding.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_successive_localized_cells line 13
  2. theorem OAI.Erdos3.exists_finite_family_localized_cells line 51
  3. structure OAI.Erdos3.ScalarCubeLocalizationData line 124
  4. def OAI.Erdos3.ScalarCubeLocalizationData.baseLaw line 157
  5. def OAI.Erdos3.ScalarCubeLocalizationData.point line 161
  6. def OAI.Erdos3.ScalarCubeLocalizationData.source line 164
  7. def OAI.Erdos3.ScalarCubeLocalizationData.cellLength line 167
  8. def OAI.Erdos3.ScalarCubeLocalizationData.cellCount line 169
  9. def OAI.Erdos3.ScalarCubeLocalizationData.cell line 171
  10. def OAI.Erdos3.ScalarCubeLocalizationData.error line 174
  11. theorem OAI.Erdos3.ScalarCubeLocalizationData.cellLength_pos line 180
  12. theorem OAI.Erdos3.ScalarCubeLocalizationData.cellLength_lower line 184
  13. theorem OAI.Erdos3.ScalarCubeLocalizationData.cellCount_pos line 188
  14. theorem OAI.Erdos3.ScalarCubeLocalizationData.source_complexMean line 190
  15. theorem OAI.Erdos3.ScalarCubeLocalizationData.localize line 195
  16. structure OAI.Erdos3.NormalizedScalarCubeSource line 221
  17. def OAI.Erdos3.NormalizedScalarCubeSource.baseLaw line 243
  18. def OAI.Erdos3.NormalizedScalarCubeSource.source line 247
  19. theorem OAI.Erdos3.scalarCube_weight_normalizer_bounds line 253
  20. def OAI.Erdos3.ScalarCubeLocalizationData.integerOffset line 285
  21. theorem OAI.Erdos3.ScalarCubeLocalizationData.point_scale line 288
  22. theorem OAI.Erdos3.ScalarCubeLocalizationData.cell_scale line 294
  23. theorem OAI.Erdos3.scalarCubeFamily_localize line 322
  24. def OAI.Erdos3.ScalarCubeLocalizationData.lengthLoss line 356
  25. theorem OAI.Erdos3.ScalarCubeLocalizationData.lengthLoss_pos line 358
  26. theorem OAI.Erdos3.ScalarCubeLocalizationData.length_le_lengthLoss_mul_cellLength line 362
  27. theorem OAI.Erdos3.reciprocal_product_le_of_lengths line 374
  28. theorem OAI.Erdos3.scalarCubeCell_inverse_product line 383
  29. def OAI.Erdos3.normalizedScalarCubeSourceOfMeanLower line 404
  30. def OAI.Erdos3.normalizedScalarCubeSourceOfWeight line 434
  31. def OAI.Erdos3.normalizedScalarCubeSourceOfContinuousWeight line 454
  32. def OAI.Erdos3.coefficientResidueSet line 475
  33. def OAI.Erdos3.emptyScalarCubeResidueEquiv line 478
  34. abbrev OAI.Erdos3.NormalizedScalarCubeSource.CoefficientDomain line 514
  35. theorem OAI.Erdos3.NormalizedScalarCubeSource.baseLaw_coefficient_mean line 517
  36. theorem OAI.Erdos3.NormalizedScalarCubeSource.weight_empty_coordinate line 523
  37. def OAI.Erdos3.NormalizedScalarCubeSource.coefficientDensity line 532
  38. theorem OAI.Erdos3.NormalizedScalarCubeSource.coefficientDensity_nonneg line 535
  39. theorem OAI.Erdos3.NormalizedScalarCubeSource.coefficientDensity_mean_one line 538
  40. def OAI.Erdos3.NormalizedScalarCubeSource.coefficientWeights line 546
  41. theorem OAI.Erdos3.NormalizedScalarCubeSource.source_coefficient_mean line 550
  42. theorem OAI.Erdos3.NormalizedScalarCubeSource.source_coefficient_complexMean line 560
  43. structure OAI.Erdos3.FiniteCoefficientSlice line 578
  44. abbrev OAI.Erdos3.FiniteCoefficientSlice.Domain line 587
  45. def OAI.Erdos3.FiniteCoefficientSlice.value line 590
  46. def OAI.Erdos3.FiniteCoefficientSlice.radius line 592
  47. theorem OAI.Erdos3.FiniteCoefficientSlice.value_abs_le line 594
  48. def OAI.Erdos3.coefficientSliceEmbedding line 617
  49. def OAI.Erdos3.coefficientSliceEvent line 627
  50. theorem OAI.Erdos3.coefficientSliceEmbedding_range line 631
  51. def OAI.Erdos3.conditionCoefficientSlice line 649
  52. theorem OAI.Erdos3.conditionCoefficientSlice_complexMean line 656
  53. theorem OAI.Erdos3.uniform_condition_coefficientSlice_mean line 665