OAI/Probability/JammingConcavity/RowZeroRefinementClosureRowDensityScoreIdentity.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Row Zero Refinement Closure Row Density Score Identity.

  1. lemma OAI.MicroscopicJamming.profileL1_tendsto_of_tests line 65
  2. def OAI.MicroscopicJamming.RowFiniteProfile.derivativeProfile line 101
  3. theorem OAI.MicroscopicJamming.rowDerivativeLimit line 107
  4. def OAI.MicroscopicJamming.RowGeneralDerivativeStatement line 124
  5. lemma OAI.MicroscopicJamming.gridStep_total line 143
  6. lemma OAI.MicroscopicJamming.gridStep_total_le line 155
  7. def OAI.MicroscopicJamming.SphericalProfile.rowGrid line 160
  8. lemma OAI.MicroscopicJamming.rowGaussianBlocks_cumulative line 179
  9. lemma OAI.MicroscopicJamming.sphericalProfile_ext line 189
  10. lemma OAI.MicroscopicJamming.rowGrid_profile line 192
  11. lemma OAI.MicroscopicJamming.rowGrid_distance_tendsto line 203
  12. lemma OAI.MicroscopicJamming.profile_L1_limit_unique line 220
  13. lemma OAI.MicroscopicJamming.rowTerminal_of_C2 line 229
  14. lemma OAI.MicroscopicJamming.rowDerivativeLimits_eq line 236
  15. lemma OAI.MicroscopicJamming.rowPrecision_tendsto line 276
  16. theorem OAI.MicroscopicJamming.rowGeneralDerivative line 279
  17. lemma OAI.MicroscopicJamming.rowZero_fields_exact line 327
  18. lemma OAI.MicroscopicJamming.rowLog_converges line 350
  19. theorem OAI.MicroscopicJamming.rowCascadeLogContinuity line 376
  20. def OAI.MicroscopicJamming.rowInterpolatedBlocks line 389
  21. def OAI.MicroscopicJamming.rowFiniteVarianceResponse line 392
  22. def OAI.MicroscopicJamming.RowFiniteVarianceStatement line 402
  23. def OAI.MicroscopicJamming.rowVarianceTotal line 418
  24. def OAI.MicroscopicJamming.rowVarianceCoefficients line 421
  25. def OAI.MicroscopicJamming.rowDepthPairing line 425
  26. def OAI.MicroscopicJamming.RowFiniteDiagonalStatement line 431
  27. def OAI.MicroscopicJamming.rowHeatDensity line 449
  28. lemma OAI.MicroscopicJamming.rowHeatDensity_nonneg line 452
  29. lemma OAI.MicroscopicJamming.rowHeatDensity_eq line 456
  30. lemma OAI.MicroscopicJamming.gaussianHeat_eq_density line 459
  31. lemma OAI.MicroscopicJamming.rowHeatDensity_derivative line 472
  32. lemma OAI.MicroscopicJamming.integrable_gaussian_linear_envelope line 485
  33. lemma OAI.MicroscopicJamming.rowHeatDensity_bounds line 507
  34. lemma OAI.MicroscopicJamming.rowDensity_product_bound line 550
  35. lemma OAI.MicroscopicJamming.rowDensity_response_bound line 563
  36. lemma OAI.MicroscopicJamming.rowDensity_parameter_derivative line 588
  37. lemma OAI.MicroscopicJamming.RowExpGrowth.mul line 629
  38. lemma OAI.MicroscopicJamming.rowExpGrowth_pow line 639
  39. lemma OAI.MicroscopicJamming.RowExpGrowth.affine line 645
  40. lemma OAI.MicroscopicJamming.RowExpGrowth.integrable line 656
  41. lemma OAI.MicroscopicJamming.rowGaussian_second_stein line 659
  42. lemma OAI.MicroscopicJamming.rowDensity_integrable line 699
  43. lemma OAI.MicroscopicJamming.rowDensity_score_identity line 708