OAI/Probability/JammingConcavity/SphericalGridDensity.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Spherical Grid Density.

  1. lemma OAI.MicroscopicJamming.gridStep_error_cell line 62
  2. lemma OAI.MicroscopicJamming.gridStep_distance_bound line 71
  3. lemma OAI.MicroscopicJamming.gridStep_distance_le line 104
  4. lemma OAI.MicroscopicJamming.exists_spinGrid_precision line 113
  5. lemma OAI.MicroscopicJamming.rowGrid_distance_sample line 123
  6. lemma OAI.MicroscopicJamming.gridStep_distance_tendsto_pointwise line 159
  7. lemma OAI.MicroscopicJamming.profileDistance_tendsto_pointwise line 178
  8. lemma OAI.MicroscopicJamming.profileCompactFilter line 208
  9. structure OAI.MicroscopicJamming.RowFiniteProfile line 245
  10. def OAI.MicroscopicJamming.RowFiniteProfile.profile line 254
  11. def OAI.MicroscopicJamming.RowFiniteProfile.derivative line 259
  12. def OAI.MicroscopicJamming.RowProfileTestConvergenceStatement line 267
  13. def OAI.MicroscopicJamming.RowDerivativeLimitStatement line 276
  14. def OAI.MicroscopicJamming.rowRankSelect line 290
  15. def OAI.MicroscopicJamming.rowDerivativeRankMoment line 297
  16. def OAI.MicroscopicJamming.RowZeroRefinementStatement line 307
  17. def OAI.MicroscopicJamming.RowZeroRefinementClosureStatement line 324
  18. def OAI.MicroscopicJamming.rowRankIndex line 343
  19. lemma OAI.MicroscopicJamming.rowRankSelect_index line 347
  20. lemma OAI.MicroscopicJamming.rowDerivativeRankMoment_index line 359
  21. lemma OAI.MicroscopicJamming.rowDerivativeRankMoment_cons line 366
  22. lemma OAI.MicroscopicJamming.rowGaussianComposition_insert_zero line 376
  23. lemma OAI.MicroscopicJamming.rowDerivativeRankMoment_below line 384
  24. lemma OAI.MicroscopicJamming.rowDerivativeRankMoment_insert_zero line 391
  25. theorem OAI.MicroscopicJamming.rowZeroRefinement line 415
  26. lemma OAI.MicroscopicJamming.rowComposition_filter_zero line 431
  27. lemma OAI.MicroscopicJamming.rowRankDerivative_filter_zero line 444
  28. theorem OAI.MicroscopicJamming.rowZeroRefinementClosure line 468
  29. lemma OAI.MicroscopicJamming.rowGaussianBlocks_ranks line 477
  30. lemma OAI.MicroscopicJamming.rowGaussianBlocks_mem line 483
  31. lemma OAI.MicroscopicJamming.rowRootResidual_valid line 494
  32. lemma OAI.MicroscopicJamming.rowRootResidual_sorted line 506
  33. lemma OAI.MicroscopicJamming.rowRankIndex_eq_rpcStepLevel line 533
  34. lemma OAI.MicroscopicJamming.rowRankMoment_blocks line 548
  35. lemma OAI.MicroscopicJamming.rowMesh_depth_invariant line 554
  36. lemma OAI.MicroscopicJamming.rowDepth_integrable line 568
  37. lemma OAI.MicroscopicJamming.rowDepth_joint_measurable line 577
  38. lemma OAI.MicroscopicJamming.RowFiniteProfile.derivative_measurable line 586
  39. lemma OAI.MicroscopicJamming.RowFiniteProfile.derivative_bounds line 593
  40. lemma OAI.MicroscopicJamming.RowFiniteProfile.derivative_monotone line 606
  41. lemma OAI.MicroscopicJamming.RowFiniteProfile.bound line 625
  42. lemma OAI.MicroscopicJamming.rowVariableMesh_fields_converge line 628