OAI/Combinatorics/Progressions/Estimates/NativePhysicalHaarExpansion.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BooleanCubeKernel.coefficientAmbientRowsJet line 16
  2. theorem OAI.Erdos3.BooleanCubeKernel.coefficientAmbientRowsJet_eq line 22
  3. theorem OAI.Erdos3.BooleanCubeKernel.coefficientAmbientRowsJet_lipschitz line 31
  4. def OAI.Erdos3.BooleanCubeKernel.coefficientAmbientRowsSite line 54
  5. theorem OAI.Erdos3.BooleanCubeKernel.coefficientAmbientRowsSite_lipschitz line 60
  6. theorem OAI.Erdos3.BooleanCubeKernel.coefficientAmbientRowsSite_eq line 67
  7. theorem OAI.Erdos3.torus_nsmul_reindex_lipschitz line 86
  8. def OAI.Erdos3.VectorPolynomial.physicalFactorCoverMap line 103
  9. theorem OAI.Erdos3.VectorPolynomial.physicalFactorCoverMap_lipschitz line 110
  10. theorem OAI.Erdos3.VectorPolynomial.physicalFactorCoverMap_lipschitz_mul line 118
  11. theorem OAI.Erdos3.VectorPolynomial.physicalFactorCoverMap_input line 128
  12. theorem OAI.Erdos3.VectorPolynomial.physical_factor_on_common_cover line 153
  13. def OAI.Erdos3.VectorPolynomial.physicalCoverPolynomial line 169
  14. theorem OAI.Erdos3.VectorPolynomial.physicalCoverPolynomial_eval line 173
  15. theorem OAI.Erdos3.VectorPolynomial.physicalCoverPolynomial_degree line 181
  16. theorem OAI.Erdos3.VectorPolynomial.physicalGridFactorInput_coverPolynomial line 186
  17. theorem OAI.Erdos3.BooleanCubeKernel.coefficientCoverSample_physicalRows line 211
  18. theorem OAI.Erdos3.BooleanCubeKernel.physicalSingleSiteValue_ambient_one line 231
  19. def OAI.Erdos3.BooleanCubeKernel.coefficientAmbientVertex line 246
  20. theorem OAI.Erdos3.BooleanCubeKernel.coefficientAmbientVertex_lipschitz line 252
  21. theorem OAI.Erdos3.BooleanCubeKernel.coefficientAmbientVertex_sample line 265
  22. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.complex_dist_product line 288
  23. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.product line 296
  24. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.product_eval line 356
  25. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.product_lipschitz_le line 397
  26. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.productUniform line 409
  27. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.productUniform_eval line 416
  28. def OAI.Erdos3.BooleanCubeKernel.coefficientAmbientModelTerm line 437
  29. theorem OAI.Erdos3.BooleanCubeKernel.coefficientAmbientModelTerm_bounds line 442
  30. theorem OAI.Erdos3.BooleanCubeKernel.coefficientAmbientModelTerm_sample line 461
  31. theorem OAI.Erdos3.BooleanCubeKernel.physicalRowsCoefficient_measurePreserving line 506
  32. theorem OAI.Erdos3.BooleanCubeKernel.physicalRowsCoefficient_square_integral line 518
  33. theorem OAI.Erdos3.BooleanCubeKernel.physicalRowsCoefficient_square_le_of_l1 line 534
  34. def OAI.Erdos3.VectorPolynomial.nativeSingleSiteCoverObservable line 565
  35. theorem OAI.Erdos3.VectorPolynomial.nativeSingleSiteCoverObservable_continuous line 572
  36. theorem OAI.Erdos3.VectorPolynomial.norm_nativeSingleSiteCoverObservable_le line 582
  37. theorem OAI.Erdos3.VectorPolynomial.nativeSingleSiteCoverObservable_physical line 589
  38. theorem OAI.Erdos3.VectorPolynomial.nativeSingleSiteCoverObservable_projection line 598
  39. theorem OAI.Erdos3.VectorPolynomial.nativeSingleSiteCoverObservable_product line 610
  40. theorem OAI.Erdos3.VectorPolynomial.nativePhysicalHaarExpansion line 635