OAI/Probability/JammingConcavity/GaussianDerivativeMartingale.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Derivative Martingale.

  1. lemma OAI.MicroscopicJamming.rowTiltStep_affine line 54
  2. lemma OAI.MicroscopicJamming.rowTiltStep_linear line 64
  3. lemma OAI.MicroscopicJamming.decoratedGaussian_ofReal line 74
  4. lemma OAI.MicroscopicJamming.rowAffine_bound line 105
  5. lemma OAI.MicroscopicJamming.rowSinglePattern_valid line 111
  6. lemma OAI.MicroscopicJamming.rowPairPattern_valid line 122
  7. lemma OAI.MicroscopicJamming.familyReplicaMean_single_affine line 143
  8. lemma OAI.MicroscopicJamming.rowTiltStep_three line 168
  9. def OAI.MicroscopicJamming.rowAffineMoment line 184
  10. lemma OAI.MicroscopicJamming.rowAffineMoment_measurable line 187
  11. lemma OAI.MicroscopicJamming.rowAffineMoment_nonneg line 193
  12. lemma OAI.MicroscopicJamming.rowAffineMoment_bound line 202
  13. lemma OAI.MicroscopicJamming.familyReplicaMean_pair_affine line 215
  14. lemma OAI.MicroscopicJamming.familySample_pair_affine line 269
  15. theorem OAI.MicroscopicJamming.rowGaussianPair line 290
  16. lemma OAI.MicroscopicJamming.rowSinglePattern_shape line 320
  17. lemma OAI.MicroscopicJamming.rowPairPattern_shape line 329
  18. def OAI.MicroscopicJamming.rowAffineIidObservable line 337
  19. def OAI.MicroscopicJamming.rowAffineIidMean line 343
  20. lemma OAI.MicroscopicJamming.rowAffineIidObservable_bound line 348
  21. lemma OAI.MicroscopicJamming.rowAffineIidObservable_integrable line 360
  22. lemma OAI.MicroscopicJamming.rowAffineIidMean_eq line 371
  23. lemma OAI.MicroscopicJamming.rowAffineIidMean_bound line 388
  24. lemma OAI.MicroscopicJamming.rowAffineIidMean_measurable line 398
  25. lemma OAI.MicroscopicJamming.rowAffineIidMean_integrable line 412
  26. lemma OAI.MicroscopicJamming.rowAffineIidMean_expectation line 422
  27. lemma OAI.MicroscopicJamming.rowSignedPairObservable_polarization line 456
  28. lemma OAI.MicroscopicJamming.rowSignedPairObservable_integrable line 464
  29. lemma OAI.MicroscopicJamming.rowSignedPairMean_polarization line 479
  30. lemma OAI.MicroscopicJamming.rowSignedPair_expectation line 503
  31. theorem OAI.MicroscopicJamming.rowSignedPair line 553
  32. lemma OAI.MicroscopicJamming.rowSinglePattern_size line 568
  33. lemma OAI.MicroscopicJamming.rowPairPattern_size line 575
  34. lemma OAI.MicroscopicJamming.partitionProduct_one line 583
  35. lemma OAI.MicroscopicJamming.partitionProduct_two line 586
  36. lemma OAI.MicroscopicJamming.partitionProduct_one_one line 590
  37. lemma OAI.MicroscopicJamming.rpcPatternProduct_single line 593
  38. def OAI.MicroscopicJamming.rowPairWeight line 602
  39. lemma OAI.MicroscopicJamming.rowPairWeight_nil line 605
  40. lemma OAI.MicroscopicJamming.rowPairWeight_cons_zero line 607
  41. lemma OAI.MicroscopicJamming.rowPairWeight_cons_succ line 613
  42. lemma OAI.MicroscopicJamming.rpcStepLevel_le_length line 619
  43. lemma OAI.MicroscopicJamming.rpcStepLevel_of_lt_head line 622
  44. lemma OAI.MicroscopicJamming.rpcStepLevel_of_le_head line 635
  45. lemma OAI.MicroscopicJamming.rpcStepTest_intervalIntegrable line 639
  46. lemma OAI.MicroscopicJamming.integral_rpcStepTest_weights line 652