OAI/Combinatorics/Progressions/Geometry/ScalarReferenceNativeDetectionCoordinateEquiv.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.normalizedSliceTest_equiv line 13
  2. theorem OAI.Erdos3.sampledSingleSliceSeminorm_equiv line 20
  3. theorem OAI.Erdos3.sampledSliceSeminorm_coordinateEquiv line 36
  4. def OAI.Erdos3.scalarNoiseIndexEquiv line 77
  5. theorem OAI.Erdos3.scalarNoiseIndexEquiv_none line 80
  6. theorem OAI.Erdos3.scalarNoiseIndexEquiv_some line 83
  7. theorem OAI.Erdos3.scalarNoiseIndexEquiv_symm line 86
  8. theorem OAI.Erdos3.trimmedSpatialWidths_scalarNoiseIndexEquiv line 89
  9. def OAI.Erdos3.scalarNoiseSupportEquiv line 98
  10. theorem OAI.Erdos3.scalarNoiseSupportEquiv_val line 123
  11. theorem OAI.Erdos3.scalarNoiseSupportEquiv_symm_val line 129
  12. def OAI.Erdos3.scalarJointPathEquiv line 135
  13. theorem OAI.Erdos3.scalarJointPathEquiv_fst line 141
  14. theorem OAI.Erdos3.scalarJointPathEquiv_snd_val line 146
  15. theorem OAI.Erdos3.BooleanCubeKernel.jointIntegerPhysicalSite_scalarNoiseIndexEquiv line 156
  16. theorem OAI.Erdos3.BooleanCubeKernel.jointIntegerPhysicalSite_scalarNoiseSupportEquiv line 167
  17. theorem OAI.Erdos3.BooleanCubeKernel.jointIntegerPhysicalSite_scalarJointPathEquiv line 175
  18. theorem OAI.Erdos3.selectedResidueSmoothMass_scalarCoordinateEquiv line 202
  19. theorem OAI.Erdos3.selectedResidueFiniteLaw_scalarCoordinateEquiv_weight line 217
  20. theorem OAI.Erdos3.selectedJointReference_scalarCoordinateEquiv_weight line 234
  21. theorem OAI.Erdos3.selectedJointReference_scalarCoordinateEquiv_mean line 246
  22. theorem OAI.Erdos3.selectedJointReference_scalarCoordinateEquiv_complexMean line 256
  23. theorem OAI.Erdos3.selectedJointReference_scalarCoordinateEquiv_mass line 266
  24. def OAI.Erdos3.VectorPolynomial.OrdinarySliceNativeDetection line 288
  25. theorem OAI.Erdos3.VectorPolynomial.niltestSliceSeminorm_coordinateEquiv line 315
  26. theorem OAI.Erdos3.VectorPolynomial.OrdinarySliceNativeDetection.coordinateReturn line 362
  27. def OAI.Erdos3.VectorPolynomial.ScalarReferenceNativeDetection line 428
  28. theorem OAI.Erdos3.VectorPolynomial.ScalarReferenceNativeDetection.coordinateReturn line 446
  29. theorem OAI.Erdos3.VectorPolynomial.ScalarReferenceNativeDetection.retag_of_isEmpty line 476