OAI/Combinatorics/Progressions/Estimates/PhysicalRowsSiteReconstruction.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.identityCoefficientFrame line 13
  2. theorem OAI.Erdos3.VectorPolynomial.affineParameterSubstitution_identity line 16
  3. theorem OAI.Erdos3.VectorPolynomial.affineSampleCoefficientArray_identity line 21
  4. theorem OAI.Erdos3.VectorPolynomial.exists_coefficient_sample_realization line 29
  5. def OAI.Erdos3.BooleanCubeKernel.physicalCubeVertexValue line 69
  6. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeVertexValue_rootDifferences line 72
  7. theorem OAI.Erdos3.BooleanCubeKernel.integerSiteValue_affine_physical line 80
  8. def OAI.Erdos3.BooleanCubeKernel.physicalCubeCoveredSample line 90
  9. theorem OAI.Erdos3.BooleanCubeKernel.affineCoveredSiteSample_physical line 99
  10. def OAI.Erdos3.BooleanCubeKernel.physicalCubeSiteTest line 133
  11. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeSiteTest_norm_le line 137
  12. theorem OAI.Erdos3.BooleanCubeKernel.layeredSiteWeight_physicalCube line 143
  13. def OAI.Erdos3.BooleanCubeKernel.physicalCubeCoveredTest line 155
  14. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeCoveredTest_norm_le line 165
  15. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeCoveredTest_of_frame line 180
  16. def OAI.Erdos3.BooleanCubeKernel.starVertexSiteFactor line 209
  17. theorem OAI.Erdos3.BooleanCubeKernel.starVertexSiteFactor_bound line 213
  18. theorem OAI.Erdos3.BooleanCubeKernel.starVertexSiteFactor_prod line 223
  19. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeVertexValue_star line 233
  20. theorem OAI.Erdos3.BooleanCubeKernel.starVertexSiteFactor_physicalCube line 239
  21. theorem OAI.Erdos3.BooleanCubeKernel.starVertexSiteFactor_test line 246
  22. theorem OAI.Erdos3.BooleanCubeKernel.coefficientTorusFourierSum_sample line 265
  23. theorem OAI.Erdos3.BooleanCubeKernel.coefficientCoverSample_sites line 278
  24. def OAI.Erdos3.BooleanCubeKernel.physicalCubeEuclideanSample line 299
  25. theorem OAI.Erdos3.BooleanCubeKernel.coefficientCoverSample_physicalJet line 309
  26. def OAI.Erdos3.BooleanCubeKernel.physicalCubePositiveTest line 331
  27. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubePositiveTest_norm_le line 339
  28. def OAI.Erdos3.BooleanCubeKernel.physicalCubeRowSample line 362
  29. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeRowSample_standard line 371
  30. theorem OAI.Erdos3.BooleanCubeKernel.sampled_jet_approximation_global line 390
  31. def OAI.Erdos3.BooleanCubeKernel.standardPhysicalCubeOutput line 424
  32. def OAI.Erdos3.BooleanCubeKernel.standardPhysicalCubeFrame line 428
  33. theorem OAI.Erdos3.BooleanCubeKernel.standardPhysicalCubeOutput_frame line 432
  34. theorem OAI.Erdos3.BooleanCubeKernel.standardPhysicalCubeFrame_injective line 440
  35. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeRootDifferences_standard line 446
  36. def OAI.Erdos3.BooleanCubeKernel.standardPhysicalJetMap line 458
  37. theorem OAI.Erdos3.BooleanCubeKernel.affineCoveredSiteSample_zero_base_physical line 465
  38. theorem OAI.Erdos3.BooleanCubeKernel.coefficientCoverSample_standardPhysicalJet line 483
  39. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeEuclideanSample_frame line 510
  40. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeRowSample_fintype_independent line 529
  41. theorem OAI.Erdos3.VectorPolynomial.coefficientSite_eq_of_euclideanJet_eq line 549
  42. def OAI.Erdos3.BooleanCubeKernel.standardPhysicalSite line 571
  43. theorem OAI.Erdos3.BooleanCubeKernel.standard_jet_site_approximation line 574
  44. theorem OAI.Erdos3.BooleanCubeKernel.standardPhysicalJetMap_measurePreserving line 617
  45. theorem OAI.Erdos3.BooleanCubeKernel.standardPhysicalJetMap_density_mass line 629
  46. def OAI.Erdos3.BooleanCubeKernel.physicalSingleSiteValue line 661
  47. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeEuclideanSample_site_reconstruction line 666
  48. theorem OAI.Erdos3.BooleanCubeKernel.coveredBooleanSiteValue_physical line 688
  49. theorem OAI.Erdos3.BooleanCubeKernel.coveredRowsSiteValue_physical line 714