OAI/Probability/JammingConcavity/FiniteRowRecursion.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Finite Row Recursion.

  1. def OAI.MicroscopicJamming.MarkedCascadeTree line 23
  2. instance OAI.MicroscopicJamming.markedCascadeTreeMeasurable line 27
  3. def OAI.MicroscopicJamming.forgetCascadeMarks line 33
  4. def OAI.MicroscopicJamming.incrementCascadeLaw line 37
  5. def OAI.MicroscopicJamming.incrementCascadeTotal line 41
  6. def OAI.MicroscopicJamming.incrementUnmarkedTotal line 46
  7. def OAI.MicroscopicJamming.finiteRowRecursion line 49
  8. def OAI.MicroscopicJamming.RecursionMomentsFinite line 54
  9. def OAI.MicroscopicJamming.incrementLogPartition line 61
  10. def OAI.MicroscopicJamming.FiniteRowRecursionStatement line 65
  11. def OAI.MicroscopicJamming.rowVarianceSum line 83
  12. def OAI.MicroscopicJamming.GaussianRowEnvelopeStatement line 87
  13. lemma OAI.MicroscopicJamming.measurable_forgetCascadeMarks line 106
  14. lemma OAI.MicroscopicJamming.incrementCascadeLaw_probability line 111
  15. lemma OAI.MicroscopicJamming.incrementCascadeLaw_forget line 121
  16. lemma OAI.MicroscopicJamming.measurable_pointCloudFunctional_param line 138
  17. lemma OAI.MicroscopicJamming.measurable_incrementCascadeTotal line 148
  18. lemma OAI.MicroscopicJamming.measurable_incrementUnmarkedTotal line 159
  19. lemma OAI.MicroscopicJamming.measurable_finiteRowRecursion line 162
  20. lemma OAI.MicroscopicJamming.incrementUnmarkedTotal_cons line 174
  21. lemma OAI.MicroscopicJamming.incrementUnmarkedTotal_properties line 179
  22. lemma OAI.MicroscopicJamming.gaussian_shift_square line 201
  23. lemma OAI.MicroscopicJamming.gaussian_envelope_integrable line 218
  24. lemma OAI.MicroscopicJamming.gaussian_envelope_integral_lower line 235
  25. lemma OAI.MicroscopicJamming.gaussian_log_operator_barrier line 251
  26. lemma OAI.MicroscopicJamming.hasDerivAt_standardGaussianPDF line 295
  27. lemma OAI.MicroscopicJamming.integrable_gaussianPDF_mul line 305
  28. theorem OAI.MicroscopicJamming.standardGaussian_integration_by_parts line 314
  29. theorem OAI.MicroscopicJamming.standardGaussian_product_integration_by_parts line 341
  30. theorem OAI.MicroscopicJamming.standardGaussian_pi_integration_by_parts line 356
  31. def OAI.MicroscopicJamming.HeatQuadraticGrowth line 383
  32. lemma OAI.MicroscopicJamming.gaussian_abs_one_pow_integrable line 386
  33. lemma OAI.MicroscopicJamming.heat_affine_bound line 403
  34. lemma OAI.MicroscopicJamming.heat_affine_quadratic_integrable line 408
  35. lemma OAI.MicroscopicJamming.heat_affine_mul_integrable line 422
  36. lemma OAI.MicroscopicJamming.row_terminal_deriv_linear line 445
  37. lemma OAI.MicroscopicJamming.row_terminal_quadratic_growth line 466
  38. lemma OAI.MicroscopicJamming.row_terminal_deriv_growth line 479
  39. lemma OAI.MicroscopicJamming.row_terminal_second_growth line 485
  40. def OAI.MicroscopicJamming.rowExpFirst line 501
  41. def OAI.MicroscopicJamming.rowExpSecond line 502
  42. lemma OAI.MicroscopicJamming.row_exp_derivatives line 505
  43. lemma OAI.MicroscopicJamming.row_exp_measurable line 519
  44. lemma OAI.MicroscopicJamming.row_exp_growth line 531
  45. lemma OAI.MicroscopicJamming.heat_curve_derivative line 589
  46. lemma OAI.MicroscopicJamming.gaussianHeat_space_derivative line 654
  47. lemma OAI.MicroscopicJamming.gaussianHeat_time_derivative line 666