OAI/Combinatorics/Progressions/Estimates/SampledNativeModel.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.detector_of_unit_detector line 15
  2. structure OAI.Erdos3.NativeSampleCorrelation line 56
  3. def OAI.Erdos3.NativeSampleCorrelation.mono line 83
  4. theorem OAI.Erdos3.NativeSampleCorrelation.exists_of_expansion line 89
  5. structure OAI.Erdos3.NativeSampleModel line 114
  6. def OAI.Erdos3.NativeSampleModel.constOne line 140
  7. def OAI.Erdos3.NativeSampleCorrelation.ofMean line 150
  8. def OAI.Erdos3.NativeSampleModel.smul line 160
  9. theorem OAI.Erdos3.NativeSampleModel.norm_le line 170
  10. def OAI.Erdos3.NativeSampleCorrelation.toSampleModel line 175
  11. def OAI.Erdos3.twistedNativeSampleFunctions line 186
  12. theorem OAI.Erdos3.twistedNativeSampleFunctions_zero line 191
  13. theorem OAI.Erdos3.twistedNativeSampleFunctions_balanced line 194
  14. theorem OAI.Erdos3.twistedNativeSampleFunctions_norm line 204
  15. theorem OAI.Erdos3.nativeCorrelation_restrict_model line 226
  16. theorem OAI.Erdos3.nativeCorrelation_finite_site_model line 252
  17. theorem OAI.Erdos3.commonStridePoint_index_of_mem line 277
  18. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.commonStridePullback line 299
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.commonStridePullback_observable line 303
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.commonStridePullback_normBound line 307
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.commonStridePullback_lipBound line 311
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.commonStridePullback_complexityLE line 315
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.commonStridePullback_eval line 319
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.commonStridePullback_eval_index_of_modEq line 325
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.commonStridePullback_eval_index_of_mem line 331
  26. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.commonStrideSampleModelOfModEq line 347
  27. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.commonStrideSampleModel line 361
  28. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.residueSliceSampleModel line 375
  29. structure OAI.Erdos3.NativeSampleModel.VerticalExpansion line 414
  30. theorem OAI.Erdos3.NativeSampleModel.exists_verticalExpansion line 443
  31. theorem OAI.Erdos3.NativeSampleModel.exists_verticalExpansion_exp_error line 465
  32. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.complexity line 478
  33. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.normBound_le line 483
  34. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.eval_error line 487
  35. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.evalReal_error line 493
  36. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.sample_error line 499
  37. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.norm_eval_le line 504
  38. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.norm_evalReal_le line 507
  39. def OAI.Erdos3.NativeSampleModel.VerticalExpansion.sampleModel line 510
  40. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.coefficient_mass line 520
  41. theorem OAI.Erdos3.exists_sampled_native_model line 535