OAI/Combinatorics/Progressions/Geometry/PhysicalSpatialScales.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BooleanCubeKernel.physicalCubeOptionEquiv line 9
  2. def OAI.Erdos3.BooleanCubeKernel.physicalCubePivotIndex line 15
  3. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubePivotIndex_inl line 27
  4. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubePivotIndex_inr line 30
  5. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeCoefficient_reindex line 33
  6. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeCoefficient_pivot line 40
  7. def OAI.Erdos3.BooleanCubeKernel.physicalSpatialInputScale line 47
  8. def OAI.Erdos3.BooleanCubeKernel.physicalSpatialOutputScale line 50
  9. theorem OAI.Erdos3.BooleanCubeKernel.physicalSpatialInputScale_pos line 53
  10. theorem OAI.Erdos3.BooleanCubeKernel.physicalSpatialOutputScale_pos line 60
  11. theorem OAI.Erdos3.BooleanCubeKernel.physicalCube_normalized_columns line 68
  12. theorem OAI.Erdos3.BooleanCubeKernel.physicalCube_normalized_pivot line 85
  13. theorem OAI.Erdos3.BooleanCubeKernel.physicalCube_coefficient_bound line 110
  14. theorem OAI.Erdos3.BooleanCubeKernel.physicalCube_normalized_entry_bound line 120
  15. theorem OAI.Erdos3.BooleanCubeKernel.physicalCube_pivot_control line 138
  16. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeCoefficient_range line 178
  17. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeCoefficient_index line 184
  18. theorem OAI.Erdos3.BooleanCubeKernel.physicalCube_remaining_norm line 191
  19. def OAI.Erdos3.BooleanCubeKernel.physicalSpatialInverseBound line 216
  20. def OAI.Erdos3.BooleanCubeKernel.physicalSpatialMeshCost line 219
  21. def OAI.Erdos3.BooleanCubeKernel.physicalSpatialErrorConstant line 225
  22. theorem OAI.Erdos3.BooleanCubeKernel.physicalCube_full_comparison line 233
  23. def OAI.Erdos3.BooleanCubeKernel.physicalSpatialCommonBudget line 298
  24. theorem OAI.Erdos3.BooleanCubeKernel.physicalSpatialCommonBudget_bounds line 301
  25. def OAI.Erdos3.BooleanCubeKernel.physicalSpatialLogAllowance line 316
  26. theorem OAI.Erdos3.BooleanCubeKernel.physicalSpatialLogAllowance_nonneg line 322
  27. theorem OAI.Erdos3.BooleanCubeKernel.physicalSpatialInverseBound_le_exp line 329
  28. theorem OAI.Erdos3.BooleanCubeKernel.physicalSpatial_constants_le_exp line 343
  29. theorem OAI.Erdos3.BooleanCubeKernel.physicalSpatial_tolerance_numerics line 380
  30. def OAI.Erdos3.BooleanCubeKernel.trimmedSpatialRootScale line 425
  31. def OAI.Erdos3.BooleanCubeKernel.trimmedSpatialSlopeScale line 428
  32. theorem OAI.Erdos3.BooleanCubeKernel.trimmedSpatial_residue_scale line 431
  33. theorem OAI.Erdos3.BooleanCubeKernel.trimmedSpatial_scales_pos line 439
  34. theorem OAI.Erdos3.BooleanCubeKernel.trimmedSpatial_scale_ratio line 447
  35. theorem OAI.Erdos3.BooleanCubeKernel.trimmedSpatial_root_control line 455
  36. theorem OAI.Erdos3.BooleanCubeKernel.trimmedSpatial_scale_lower line 465