OAI/Combinatorics/Progressions/Geometry/AllocatedNarrowSpatialCanonicalComparison.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.canonicalZeroSpatialInputMap_apply line 17
  2. theorem OAI.Erdos3.canonicalZeroSpatialInputMap_lipschitz line 36
  3. theorem OAI.Erdos3.canonicalZeroSpatialInputProjection_law line 96
  4. theorem OAI.Erdos3.canonicalZeroSpatialInputProjection_integral_complex line 106
  5. def OAI.Erdos3.canonicalZeroSpatialKernelEmbedding line 127
  6. theorem OAI.Erdos3.canonicalZeroSpatialKernelEmbedding_apply line 134
  7. def OAI.Erdos3.canonicalZeroSpatialNarrowInput line 138
  8. theorem OAI.Erdos3.canonicalZeroSpatialNarrowInput_none line 144
  9. theorem OAI.Erdos3.canonicalZeroSpatialNarrowInput_inl line 148
  10. theorem OAI.Erdos3.canonicalZeroSpatialNarrowInput_inr line 152
  11. theorem OAI.Erdos3.canonicalZeroSpatialNarrowInput_measurable line 156
  12. theorem OAI.Erdos3.canonicalZeroSpatialNarrowInput_kernel line 165
  13. theorem OAI.Erdos3.canonicalZeroSpatialPrincipal_difference line 180
  14. theorem OAI.Erdos3.canonicalZeroSpatialPrincipal_norm_le line 193
  15. theorem OAI.Erdos3.canonicalZeroSpatialPrincipal_test_error line 222
  16. theorem OAI.Erdos3.canonicalZeroSpatialNarrowInput_lipschitz line 237
  17. theorem OAI.Erdos3.canonicalZeroSpatialNarrowPrincipal_difference line 255
  18. theorem OAI.Erdos3.canonicalZeroSpatialNarrowPrincipal_norm_le line 281
  19. theorem OAI.Erdos3.canonicalZeroSpatialNarrowPrincipal_test_error line 293
  20. theorem OAI.Erdos3.selectedCanonicalZeroSpatial_complex_quadrature line 322
  21. theorem OAI.Erdos3.canonicalZeroSpatialInputMap_physicalSite line 358
  22. theorem OAI.Erdos3.canonicalZeroSpatialNarrowInput_normalized line 385
  23. theorem OAI.Erdos3.canonicalZeroSpatialNarrowInputMap_physicalSite line 400
  24. theorem OAI.Erdos3.canonicalZeroSpatialPrincipal_mass_ratio_le_one line 430
  25. theorem OAI.Erdos3.canonicalZeroSpatialNarrow_integral_error line 438
  26. theorem OAI.Erdos3.selectedCanonicalZeroSpatial_narrow_principal_comparison line 481
  27. theorem OAI.Erdos3.selectedNarrowPhysicalSpatial_canonical_comparison line 522
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedNarrowPhysicalSpatial_canonical_comparison line 596