OAI/Combinatorics/Progressions/Linear/FixedSpatialKernelSliceDensity.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.fixedSpatialKernelBlockEquiv line 13
  2. theorem OAI.Erdos3.fixedSpatialKernelBlockEquiv_coe line 18
  3. theorem OAI.Erdos3.fixedSpatialKernelBlockEquiv_apply line 25
  4. theorem OAI.Erdos3.fixedSpatialKernelBlockEquiv_jacobian line 33
  5. def OAI.Erdos3.fixedSpatialKernelDensity line 46
  6. theorem OAI.Erdos3.fixedSpatialKernelDensity_bounds line 53
  7. theorem OAI.Erdos3.fixedSpatialKernelDensity_probability_density line 64
  8. theorem OAI.Erdos3.fixedSpatialKernelDensity_probability line 72
  9. theorem OAI.Erdos3.fixedSpatialKernelDensity_image_law line 77
  10. theorem OAI.Erdos3.fixedSpatialKernelDensity_bounds_of_det line 85
  11. theorem OAI.Erdos3.fixedSpatialKernelMap_norm_le_two line 128
  12. theorem OAI.Erdos3.fixedSpatialKernelDensity_zero_of_norm_gt_two line 154
  13. theorem OAI.Erdos3.columnScaledEquiv_symm_apply line 186
  14. theorem OAI.Erdos3.columnScaledEquiv_inverse_norm_le line 197
  15. theorem OAI.Erdos3.fixedSpatialKernelBlockEquiv_slice_apply line 223
  16. theorem OAI.Erdos3.fixedSpatialKernelBlockEquiv_slice_inverse_norm_le line 240
  17. theorem OAI.Erdos3.fixedSpatialKernelBlockEquiv_slice_inverseJacobian_le line 258
  18. def OAI.Erdos3.fixedSpatialKernelSliceDensity line 308
  19. theorem OAI.Erdos3.fixedSpatialKernelSliceDensity_image_law line 313
  20. theorem OAI.Erdos3.fixedSpatialKernelSliceDensity_probability_data line 320
  21. theorem OAI.Erdos3.fixedSpatialKernelSliceDensity_bounds line 324
  22. theorem OAI.Erdos3.fixedSpatialKernelBlock_slice_det_lower line 334
  23. theorem OAI.Erdos3.fixedSpatialKernelBlock_slice_entry_bound line 352
  24. theorem OAI.Erdos3.fixedSpatialKernelSliceDensity_bounds_of_det line 363
  25. theorem OAI.Erdos3.fixedSpatialKernelSliceDensity_zero_of_norm_gt_two line 381