OAI/Probability/JammingConcavity/RowBoundedTerminal.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Row Bounded Terminal.

  1. structure OAI.MicroscopicJamming.RowBoundedTerminal line 54
  2. def OAI.MicroscopicJamming.rowBoundedExpFirst line 62
  3. def OAI.MicroscopicJamming.rowBoundedExpSecond line 64
  4. lemma OAI.MicroscopicJamming.rowBounded_exp_derivatives line 67
  5. lemma OAI.MicroscopicJamming.rowBounded_exp_measurable line 76
  6. lemma OAI.MicroscopicJamming.rowBounded_exp_growth line 85
  7. lemma OAI.MicroscopicJamming.rowBounded_tilt_slope line 104
  8. lemma OAI.MicroscopicJamming.rowBounded_tilt_curvature line 109
  9. lemma OAI.MicroscopicJamming.rowBounded_tilt_slope_square line 114
  10. lemma OAI.MicroscopicJamming.rowBoundedOperator_derivatives line 129
  11. lemma OAI.MicroscopicJamming.rowBoundedOperator_terminal line 207
  12. lemma OAI.MicroscopicJamming.rowBoundedComposition_terminal line 240
  13. lemma OAI.MicroscopicJamming.rowDerivativeDepthMoment_nil line 252
  14. lemma OAI.MicroscopicJamming.measurable_rowDerivativeDepthMoment line 256
  15. lemma OAI.MicroscopicJamming.rowDerivativeDepthMoment_bounds line 270
  16. lemma OAI.MicroscopicJamming.rowDerivativeDepthMoment_monotone line 299
  17. lemma OAI.MicroscopicJamming.rowDerivativeDepthMoment_plateau line 338
  18. theorem OAI.MicroscopicJamming.gaussianDerivativeMartingale line 364
  19. lemma OAI.MicroscopicJamming.rowGaussianLaw_map line 383
  20. lemma OAI.MicroscopicJamming.rowGaussian_integral line 388
  21. lemma OAI.MicroscopicJamming.rowGaussian_lintegral line 393
  22. lemma OAI.MicroscopicJamming.rowGaussian_integrable line 398
  23. lemma OAI.MicroscopicJamming.rowGaussianBlocks_valid line 404
  24. lemma OAI.MicroscopicJamming.rowGaussian_recursion line 414
  25. instance OAI.MicroscopicJamming.rowSingleIndexUnique line 452
  26. def OAI.MicroscopicJamming.rowPairIndexEquiv line 463
  27. lemma OAI.MicroscopicJamming.rowPairIndexEquiv_zero line 484
  28. lemma OAI.MicroscopicJamming.rowPairIndexEquiv_succ line 488
  29. lemma OAI.MicroscopicJamming.familySampleObservable_single line 492
  30. lemma OAI.MicroscopicJamming.familySampleObservable_pair_zero line 523
  31. lemma OAI.MicroscopicJamming.familySampleObservable_pair_succ line 576
  32. lemma OAI.MicroscopicJamming.familySampleObservable_pair line 624
  33. theorem OAI.MicroscopicJamming.rowPairSemantic_proved line 654