OAI/Combinatorics/Progressions/Estimates/PhysicalSingleSiteCommonCover.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.BooleanCubeKernel.coefficientLayerArray_affineSample line 15
  2. theorem OAI.Erdos3.BooleanCubeKernel.coefficientSiteTorusMap_coverSample line 23
  3. theorem OAI.Erdos3.VectorPolynomial.root_coe_sum line 56
  4. def OAI.Erdos3.VectorPolynomial.coefficientAmbientRoot line 63
  5. def OAI.Erdos3.VectorPolynomial.coefficientAmbientRootLip line 68
  6. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientRoot_lipschitz line 72
  7. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientRoot_mk line 102
  8. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientRoot_sample line 116
  9. theorem OAI.Erdos3.boundedCoefficientJetMatrix_empty line 166
  10. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientRoot_eq_emptyJet line 180
  11. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientRoot_eq_oneSiteJet line 191
  12. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSamplePhysicalMixedValue line 223
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSamplePhysicalMixedValue_real line 231
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSamplePhysicalMixedValue_integer line 247
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSamplePhysicalMixedValue_integer_cast line 261
  16. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenAmbientRootObservable line 286
  17. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.norm_frozenAmbientRootObservable_le line 292
  18. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenAmbientRootObservable_lipschitz line 299
  19. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenAmbientRootObservable_sample line 306
  20. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.rootResidue line 319
  21. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.integerPhysicalSite_residue line 324
  22. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenSpatialEval_integerPhysicalSite_of_residue line 336
  23. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.selected_weighted_frozenSpatialEval_root_eq line 347
  24. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.selected_frozenSpatialEval_root_eq line 370
  25. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.selected_density_frozenSpatialEval_root_eq line 386
  26. theorem OAI.Erdos3.monomialArrayPolynomial_eval_normalized_input line 413
  27. theorem OAI.Erdos3.monomialArrayPolynomial_eval_div_coefficients line 427
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleNormalizedCoefficients_eval_physical line 457
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalSides_not_short line 486
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleSliceInput_physical line 493
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceMap_physical line 512
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceMap_physical_join line 522
  33. theorem OAI.Erdos3.VectorPolynomial.coefficientOneSiteJet_measurePreserving line 568
  34. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientRoot_haar_integral line 581
  35. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenSingleSiteHaarReference line 608
  36. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenSingleSiteHaarReference_integrable line 615
  37. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.norm_frozenSingleSiteHaarReference_le line 633
  38. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenSingleSiteHaarReference_lipschitz line 644
  39. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenAmbientRootObservable_integral line 659
  40. theorem OAI.Erdos3.VectorPolynomial.exists_normalizedTwist_singleSite_haar_sampling line 670
  41. def OAI.Erdos3.VectorPolynomial.singleSiteIntegerCover line 742
  42. theorem OAI.Erdos3.VectorPolynomial.singleSiteIntegerCover_continuous line 748
  43. theorem OAI.Erdos3.VectorPolynomial.singleSiteIntegerCover_surjective line 757
  44. theorem OAI.Erdos3.VectorPolynomial.coveredJetAmbientTorus_singleSiteIntegerCover line 765
  45. theorem OAI.Erdos3.VectorPolynomial.physicalSingleSiteValue_product_projection line 774
  46. theorem OAI.Erdos3.VectorPolynomial.physicalSingleSiteValue_divisor_projection line 794
  47. theorem OAI.Erdos3.VectorPolynomial.physicalSingleSiteValue_gridFactorInput line 805
  48. theorem OAI.Erdos3.VectorPolynomial.physicalSingleSiteValue_commonCover_gridFactorInput line 822
  49. theorem OAI.Erdos3.VectorPolynomial.singleSite_compactSpace_of_coefficientTorus line 833
  50. theorem OAI.Erdos3.VectorPolynomial.singleSiteIntegerCover_measurePreserving line 859
  51. theorem OAI.Erdos3.VectorPolynomial.singleSiteIntegerCover_integral line 876
  52. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenSingleSiteHaarReference_commonCover line 889