OAI/Probability/JammingConcavity/FamilyPathRatio.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Family Path Ratio.

  1. theorem OAI.MicroscopicJamming.familyReplica line 54
  2. lemma OAI.MicroscopicJamming.lintegral_pi_prod_countable line 188
  3. lemma OAI.MicroscopicJamming.lintegral_pi_fixed_root line 200
  4. lemma OAI.MicroscopicJamming.familySampleLeafLaw_apply_good line 228
  5. lemma OAI.MicroscopicJamming.familySampleLeafLaw_probability line 240
  6. lemma OAI.MicroscopicJamming.familySampleLeafLaw_singleton line 251
  7. lemma OAI.MicroscopicJamming.markedPatternIndex_card line 258
  8. lemma OAI.MicroscopicJamming.measurable_familyLeafMass line 274
  9. lemma OAI.MicroscopicJamming.measurable_familySampleLeafLaw_singleton line 280
  10. lemma OAI.MicroscopicJamming.measurable_familySampleObservable line 299
  11. lemma OAI.MicroscopicJamming.measurable_familySampleMean line 326
  12. lemma OAI.MicroscopicJamming.familySampleLeafLaw_child_density line 342
  13. lemma OAI.MicroscopicJamming.familySampleMean_cons line 372
  14. lemma OAI.MicroscopicJamming.familySampleMean_eq_ae line 487
  15. theorem OAI.MicroscopicJamming.familySample line 528
  16. def OAI.MicroscopicJamming.RowExpGrowth line 548
  17. lemma OAI.MicroscopicJamming.gaussian_exp_abs_integrable line 551
  18. lemma OAI.MicroscopicJamming.RowExpGrowth.integrable_affine line 565
  19. lemma OAI.MicroscopicJamming.RowExpGrowth.bounded line 580
  20. lemma OAI.MicroscopicJamming.RowExpGrowth.mul_bounded line 583
  21. lemma OAI.MicroscopicJamming.bounded_deriv_linear line 592
  22. lemma OAI.MicroscopicJamming.RowExpGrowth.of_bounded_deriv line 602
  23. lemma OAI.MicroscopicJamming.RowExpGrowth.exp_bounded_deriv line 613
  24. lemma OAI.MicroscopicJamming.rowExpHeat_space_derivative line 623
  25. lemma OAI.MicroscopicJamming.measurable_rowTiltStep line 663
  26. lemma OAI.MicroscopicJamming.rowTiltStep_weight_integrable line 669
  27. lemma OAI.MicroscopicJamming.rowTiltStep_product_integrable line 674
  28. lemma OAI.MicroscopicJamming.rowTiltStep_abs_bound line 680
  29. lemma OAI.MicroscopicJamming.rowTiltStep_nonneg line 699
  30. lemma OAI.MicroscopicJamming.rowTiltStep_mono line 704
  31. lemma OAI.MicroscopicJamming.rowTiltStep_square_ge line 715
  32. lemma OAI.MicroscopicJamming.rowTiltStep_zero line 739