OAI/Combinatorics/Progressions/Linear/NativeChartKernel.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.chartCoordinateKernel line 14
  2. theorem OAI.Erdos3.chartCoordinateKernel_of_mem line 18
  3. theorem OAI.Erdos3.chartCoordinateKernel_of_not_mem line 26
  4. theorem OAI.Erdos3.chartCoordinateKernel_recover line 34
  5. theorem OAI.Erdos3.chartCoordinateKernel_range line 40
  6. theorem OAI.Erdos3.chartCoordinateKernel_support line 45
  7. theorem OAI.Erdos3.chartCoordinateKernel_lipschitz line 66
  8. theorem OAI.Erdos3.chartKernelScaling_lipschitz line 105
  9. def OAI.Erdos3.scaledChartKernel line 121
  10. theorem OAI.Erdos3.scaledChartKernel_value line 145
  11. theorem OAI.Erdos3.scaledChartKernel_lip line 149
  12. theorem OAI.Erdos3.scaledChartKernel_recover line 153
  13. theorem OAI.Erdos3.chartKernel_log_bound line 164
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.realObservable_lipschitz line 202
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.realObservable_tsupport line 209
  16. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.chartKernel line 225
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.chartKernel_lip line 231
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.chartKernel_value line 235
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.chartKernel_recover line 240
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.chartKernel_log_bound line 248