OAI/Combinatorics/Progressions/Estimates/MixedBooleanSiteValues.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.BoundedBooleanJet line 15
  2. def OAI.Erdos3.booleanReconstructionMatrix line 17
  3. theorem OAI.Erdos3.booleanJetExtraction_mul_reconstruction line 20
  4. theorem OAI.Erdos3.booleanReconstruction_mul_extraction line 27
  5. def OAI.Erdos3.boundedBooleanReconstructionMatrix line 31
  6. theorem OAI.Erdos3.boundedBooleanReconstruction_siteMatrix line 34
  7. theorem OAI.Erdos3.boundedBooleanExtraction_mul_reconstruction line 74
  8. theorem OAI.Erdos3.booleanJetExtractionMatrix_abs_le_one line 84
  9. theorem OAI.Erdos3.boundedBooleanReconstruction_zsmul_inverse line 90
  10. def OAI.Erdos3.boundedBooleanJetRows line 113
  11. theorem OAI.Erdos3.mem_boundedBooleanJetRows line 116
  12. theorem OAI.Erdos3.boundedBooleanJetRows_subtype_eq line 120
  13. def OAI.Erdos3.boundedBooleanJetRowsEquiv line 124
  14. theorem OAI.Erdos3.boundedBooleanJetRowsEquiv_val line 131
  15. def OAI.Erdos3.realBoundedSiteReconstruction line 145
  16. theorem OAI.Erdos3.realBoundedSiteReconstruction_coefficient line 149
  17. def OAI.Erdos3.realSitesFromBoundedJets line 162
  18. theorem OAI.Erdos3.booleanSiteJets_realSitesFromBoundedJets line 166
  19. abbrev OAI.Erdos3.VectorPolynomial.LowBooleanJetTorus line 183
  20. def OAI.Erdos3.VectorPolynomial.siteFromLowBooleanJets line 187
  21. theorem OAI.Erdos3.VectorPolynomial.siteFromLowBooleanJets_continuous line 194
  22. theorem OAI.Erdos3.VectorPolynomial.siteFromLowBooleanJets_coefficient line 199
  23. theorem OAI.Erdos3.VectorPolynomial.coefficientSiteImage_lowJet_injective line 216
  24. theorem OAI.Erdos3.VectorPolynomial.coefficientSiteImage_lowJet_surjective line 232
  25. def OAI.Erdos3.VectorPolynomial.lowJetSiteImageSection line 245
  26. theorem OAI.Erdos3.VectorPolynomial.lowJetSiteImageSection_continuous line 258
  27. theorem OAI.Erdos3.VectorPolynomial.lowJetSiteImageSection_site line 266
  28. theorem OAI.Erdos3.realBoundedSiteReconstruction_bound line 290
  29. theorem OAI.Erdos3.realBoundedSiteReconstruction_sub line 310
  30. theorem OAI.Erdos3.realSitesFromBoundedJets_bound line 320
  31. theorem OAI.Erdos3.realSitesFromBoundedJets_lipschitz line 326
  32. def OAI.Erdos3.VectorPolynomial.euclideanCoefficientJetMap line 354
  33. theorem OAI.Erdos3.VectorPolynomial.euclideanCoefficientJetMap_continuous line 361
  34. theorem OAI.Erdos3.VectorPolynomial.euclideanCoefficientJetMap_surjective line 368
  35. theorem OAI.Erdos3.VectorPolynomial.euclideanCoefficientJetMap_measurePreserving line 379
  36. def OAI.Erdos3.VectorPolynomial.euclideanSiteImageEquiv line 435
  37. theorem OAI.Erdos3.VectorPolynomial.euclideanSiteImageEquiv_continuous line 444
  38. def OAI.Erdos3.VectorPolynomial.euclideanSiteImageHomeomorph line 449
  39. theorem OAI.Erdos3.VectorPolynomial.euclideanSiteImageHomeomorph_sample line 457
  40. theorem OAI.Erdos3.VectorPolynomial.euclideanSiteImageHomeomorph_haar line 468
  41. theorem OAI.Erdos3.realBoundedSiteReconstruction_div line 493
  42. def OAI.Erdos3.VectorPolynomial.mixedBooleanSiteValue line 504
  43. theorem OAI.Erdos3.VectorPolynomial.mixedBooleanSiteValue_real line 511
  44. theorem OAI.Erdos3.VectorPolynomial.mixedBooleanSiteValue_integer line 523