OAI/Combinatorics/Progressions/Linear/ExternalFamilyPrecenterProjectionData.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection line 18
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection_orbit line 26
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection_congr line 30
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection_complexity line 36
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection_unitInterval line 40
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection_observable_congr line 46
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection_invariant line 53
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection_tested_error line 68
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_external_family_centralRationalCircle_frequency line 125
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.external_family_kernelProjection_tested_error line 168
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection_observable_sub_norm_le line 235
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection_normBound line 246
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection_lipBound line 250
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_iteratedCentralCircle_translation line 270
  15. abbrev OAI.Erdos3.RationalFilteredNilmanifold.KernelProjectionParameters line 309
  16. def OAI.Erdos3.RationalFilteredNilmanifold.kernelProjectionCircleFamily line 312
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_kernelProjectionTranslation line 321
  18. def OAI.Erdos3.RationalFilteredNilmanifold.kernelProjectionTranslation line 333
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.kernelProjectionTranslation_mem line 337
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.kernelProjectionTranslation_central line 342
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.kernelProjectionTranslation_act line 347
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.continuous_kernelProjectionTranslation_act line 354
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.continuous_kernelProjectionTranslation_observable line 370
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integrable_kernelProjectionTranslation_observable line 376
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.kernelProjection_observable_eq_integral line 383
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_common_positive_kernel_projection line 408
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_external_family_common_positive_kernel_projection line 483
  28. theorem OAI.Erdos3.exists_external_family_contractive_quantitative_kernel_projection_budget line 572
  29. theorem OAI.Erdos3.exists_external_family_precenter_kernel_projection_budget line 676
  30. structure OAI.Erdos3.ExternalFamilyPrecenterProjectionData line 782
  31. theorem OAI.Erdos3.exists_externalFamilyPrecenterProjectionData line 831