OAI/Probability/JammingConcavity/RowFiniteDiagonal.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Row Finite Diagonal.

  1. lemma OAI.MicroscopicJamming.RowExpGrowth.add line 65
  2. lemma OAI.MicroscopicJamming.rowExpGrowth_const line 81
  3. lemma OAI.MicroscopicJamming.RowExpGrowth.const_mul line 84
  4. lemma OAI.MicroscopicJamming.rowDensity_score_integrable line 87
  5. lemma OAI.MicroscopicJamming.rowHeat_parameter_derivative line 100
  6. lemma OAI.MicroscopicJamming.rowFamily_linear_envelope line 154
  7. lemma OAI.MicroscopicJamming.rowFamily_exp_envelope line 170
  8. lemma OAI.MicroscopicJamming.rowTiltStep_parameter_zero line 202
  9. lemma OAI.MicroscopicJamming.rowTiltStep_variance_decomposition line 206
  10. lemma OAI.MicroscopicJamming.rowOperator_parameter_derivative line 230
  11. lemma OAI.MicroscopicJamming.rowVariance_integrand_bound line 301
  12. lemma OAI.MicroscopicJamming.rowVarianceFamily_bounds line 320
  13. lemma OAI.MicroscopicJamming.rowFiniteVariance_of_bounded line 359
  14. theorem OAI.MicroscopicJamming.rowFiniteVariance line 412
  15. lemma OAI.MicroscopicJamming.rowInterpolatedBlocks_valid line 427
  16. lemma OAI.MicroscopicJamming.rowDepthPairing_measurable line 437
  17. lemma OAI.MicroscopicJamming.rowDepthPairing_bound line 444
  18. lemma OAI.MicroscopicJamming.rowDepthPairing_tilt line 460
  19. def OAI.MicroscopicJamming.gaussianRankProfile line 489
  20. def OAI.MicroscopicJamming.RowFiniteIntegralStatement line 491
  21. lemma OAI.MicroscopicJamming.gaussianRankProfile_cons line 511
  22. lemma OAI.MicroscopicJamming.measurable_gaussianRankProfile line 515
  23. lemma OAI.MicroscopicJamming.gaussianRankProfile_bound line 522
  24. lemma OAI.MicroscopicJamming.measurable_rowRankSelect line 532
  25. lemma OAI.MicroscopicJamming.rowRankSelect_bound line 538
  26. lemma OAI.MicroscopicJamming.rowRankProduct_intervalIntegrable line 555
  27. lemma OAI.MicroscopicJamming.gaussianRankProfile_before line 582
  28. lemma OAI.MicroscopicJamming.rowRankIntegral_pairing line 590
  29. lemma OAI.MicroscopicJamming.rowVarianceTotal_cons line 655
  30. lemma OAI.MicroscopicJamming.rowFiniteVarianceResponse_diagonal line 659
  31. theorem OAI.MicroscopicJamming.rowFiniteDiagonal line 718
  32. theorem OAI.MicroscopicJamming.rowFiniteIntegral line 733