OAI/Combinatorics/Progressions/Geometry/UnconditionedSpatialWidthBudget.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rectangularWeightIndices_zero_bound line 10
  2. theorem OAI.Erdos3.integer_center_quarter_mem line 19
  3. theorem OAI.Erdos3.BooleanCubeKernel.centeredIntegerPhysicalSite_mem_box line 27
  4. theorem OAI.Erdos3.mem_rectangularWeightIndices_zero_iff line 48
  5. theorem OAI.Erdos3.rectangularWeightIndices_zero_mono line 61
  6. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidueDensityPMF_centered_mem_box line 76
  7. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_trimmed_reference_compare line 102
  8. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_trimmed_comparison_transfer line 132
  9. theorem OAI.Erdos3.shiftedSmoothProductMass_pos_of_scales line 167
  10. theorem OAI.Erdos3.BooleanCubeKernel.exists_selectedResidue_physical_cap line 175
  11. theorem OAI.Erdos3.spatialBaseCap_exp_bound line 194
  12. theorem OAI.Erdos3.BooleanCubeKernel.exists_selected_reference_box_domination line 220
  13. def OAI.Erdos3.centeredSpatialWidths line 274
  14. theorem OAI.Erdos3.centeredSpatialWidths_pos line 279
  15. theorem OAI.Erdos3.centeredSpatialWidths_scale line 286
  16. theorem OAI.Erdos3.BooleanCubeKernel.centeredSpatialWidths_fit line 313
  17. theorem OAI.Erdos3.BooleanCubeKernel.exists_centered_reference_box_domination line 331
  18. def OAI.Erdos3.spatialSamplingBudget line 367
  19. theorem OAI.Erdos3.le_spatialSamplingBudget line 369
  20. def OAI.Erdos3.spatialWidthFraction line 373
  21. theorem OAI.Erdos3.spatialWidthFraction_pos line 375
  22. theorem OAI.Erdos3.spatialWidthFraction_inv_le line 380
  23. theorem OAI.Erdos3.spatialWidthFraction_mul_le_width line 393
  24. theorem OAI.Erdos3.root_sum_le_spatial_budget line 411
  25. theorem OAI.Erdos3.spatial_scale_of_exp_size line 423
  26. theorem OAI.Erdos3.spatial_threshold_dominates line 449
  27. theorem OAI.Erdos3.spatial_threshold_large line 463
  28. theorem OAI.Erdos3.four_le_of_spatial_threshold line 471
  29. def OAI.Erdos3.trimmedSpatialWidths line 487
  30. theorem OAI.Erdos3.trimmedSpatialWidths_pos line 490
  31. theorem OAI.Erdos3.spatialWidthFraction_le_trimmed_width line 495
  32. theorem OAI.Erdos3.BooleanCubeKernel.trimmedSpatialWidths_fit line 508
  33. def OAI.Erdos3.spatialTrimMargin line 527
  34. theorem OAI.Erdos3.spatialTrimMargin_fits line 530
  35. theorem OAI.Erdos3.spatialTrimMargin_bound line 537
  36. theorem OAI.Erdos3.spatialTrimMargin_proper line 544
  37. theorem OAI.Erdos3.spatialTrimMargin_error_bound line 552
  38. theorem OAI.Erdos3.spatialTrimMargin_size_of_exp_size line 562
  39. theorem OAI.Erdos3.trimmedSpatial_normalized_parameter_slope line 584
  40. theorem OAI.Erdos3.trimmedSpatial_normalized_parameter_slope_sum line 605
  41. theorem OAI.Erdos3.trimmedSpatialWidths_scale line 633
  42. def OAI.Erdos3.unconditionedSpatialTrimFraction line 666
  43. def OAI.Erdos3.unconditionedSpatialWidthCutoff line 669
  44. theorem OAI.Erdos3.unconditionedSpatialTrimFraction_bounds line 672
  45. theorem OAI.Erdos3.unconditionedSpatialWidthCutoff_bounds line 687
  46. theorem OAI.Erdos3.unconditionedSpatialWidthBudget line 734