OAI/Combinatorics/Progressions/Geometry/MixedCoefficientSmallSupport.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.translatedQuotientChart line 19
  2. theorem OAI.Erdos3.translatedQuotientChart_measurable line 22
  3. theorem OAI.Erdos3.translatedQuotientChart_image line 29
  4. theorem OAI.Erdos3.translatedQuotientChart_measurable_image line 42
  5. theorem OAI.Erdos3.translatedQuotientChart_haar_image line 57
  6. theorem OAI.Erdos3.translatedQuotientChart_map_restrict line 75
  7. theorem OAI.Erdos3.translatedQuotientChart_embedding line 103
  8. def OAI.Erdos3.normalizedLatticePoint line 127
  9. theorem OAI.Erdos3.normalizedLatticePoint_continuous line 131
  10. def OAI.Erdos3.normalizedLatticeQuotient line 136
  11. theorem OAI.Erdos3.normalizedLatticeQuotient_measurable line 143
  12. theorem OAI.Erdos3.normalizedLatticePoint_eq_sheet line 147
  13. theorem OAI.Erdos3.normalizedLatticeQuotient_injOn line 153
  14. theorem OAI.Erdos3.normalizedLatticeQuotient_embedding line 168
  15. theorem OAI.Erdos3.normalizedLatticeQuotient_map_restrict line 176
  16. theorem OAI.Erdos3.basisAxisScale_cast_pos line 203
  17. def OAI.Erdos3.latticeConstantMass line 207
  18. theorem OAI.Erdos3.constantCoefficient_chart_support line 211
  19. def OAI.Erdos3.normalizedChartReference line 259
  20. def OAI.Erdos3.normalizedChartRegion line 265
  21. theorem OAI.Erdos3.normalizedChartRegion_measurable line 270
  22. theorem OAI.Erdos3.normalizedChartReference_map line 292
  23. theorem OAI.Erdos3.normalizedChartReference_finite line 307
  24. theorem OAI.Erdos3.normalizedLatticeQuotient_linear_lift line 332
  25. def OAI.Erdos3.normalizedLatticeQuotientHom line 338
  26. theorem OAI.Erdos3.normalizedLatticeQuotient_sum_zsmul line 359
  27. def OAI.Erdos3.normalizedLatticePointHom line 367
  28. theorem OAI.Erdos3.normalizedLatticePoint_sum_zsmul line 381
  29. def OAI.Erdos3.orthonormalMixedChartHom line 389
  30. theorem OAI.Erdos3.orthonormalMixedChart_sum_zsmul line 400
  31. theorem OAI.Erdos3.affineProbabilityProfile_abs_le line 420
  32. theorem OAI.Erdos3.normalizedMixedPoint_small line 427
  33. theorem OAI.Erdos3.mixedCoefficient_small_support line 452
  34. theorem OAI.Erdos3.mixedCoefficientDensity_width_cap line 466