OAI/Probability/JammingConcavity/GaussianDerivativeMartingaleRowRefinementCovariance.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Derivative Martingale Row Refinement Covariance.

  1. lemma OAI.MicroscopicJamming.rowSignedPairMean_integrable line 54
  2. lemma OAI.MicroscopicJamming.rowFiniteRankObservable_eq_sum line 84
  3. lemma OAI.MicroscopicJamming.rowFiniteRankTest_expectation line 96
  4. theorem OAI.MicroscopicJamming.rowFiniteRankTest line 130
  5. lemma OAI.MicroscopicJamming.familyPathWeight_forget line 145
  6. lemma OAI.MicroscopicJamming.familyBaseLeaf_lintegral line 157
  7. lemma OAI.MicroscopicJamming.familyBaseLeaf_Z line 171
  8. lemma OAI.MicroscopicJamming.familySampleLeafLaw_eq_tilted line 180
  9. lemma OAI.MicroscopicJamming.replica_normalized_eq_tilted line 207
  10. lemma OAI.MicroscopicJamming.replica_pair_abs_le line 225
  11. def OAI.MicroscopicJamming.familyCoordinateKernel line 244
  12. instance OAI.MicroscopicJamming.(instance at line 248) line 248
  13. def OAI.MicroscopicJamming.familyCoordinatePotential line 250
  14. def OAI.MicroscopicJamming.familyCoordinatePair line 253
  15. lemma OAI.MicroscopicJamming.measurable_familyCoordinatePotential line 259
  16. lemma OAI.MicroscopicJamming.measurable_familyCoordinatePair line 264
  17. lemma OAI.MicroscopicJamming.measurable_rowCoordinatePotential line 270
  18. lemma OAI.MicroscopicJamming.measurable_rowCoordinatePair line 275
  19. lemma OAI.MicroscopicJamming.familyCoordinatePair_bound line 284
  20. lemma OAI.MicroscopicJamming.familyCoordinate_pair_expectation line 299
  21. lemma OAI.MicroscopicJamming.rowDirectingPair_expectation line 319
  22. theorem OAI.MicroscopicJamming.rowDirectingPair line 369
  23. lemma OAI.MicroscopicJamming.residual_weight_integrable line 384
  24. lemma OAI.MicroscopicJamming.residual_weight_integral line 392
  25. lemma OAI.MicroscopicJamming.residual_score_integrable line 402
  26. lemma OAI.MicroscopicJamming.residual_score_integral line 413
  27. lemma OAI.MicroscopicJamming.residual_exp_integrable_iff line 428
  28. lemma OAI.MicroscopicJamming.residual_partition_eq line 445
  29. lemma OAI.MicroscopicJamming.residual_pair_score_integral line 464
  30. lemma OAI.MicroscopicJamming.residual_pair_normalized line 512
  31. lemma OAI.MicroscopicJamming.rowResidualPair_pointwise line 533
  32. theorem OAI.MicroscopicJamming.rowResidualPair line 549
  33. def OAI.MicroscopicJamming.RowRefinementCovarianceStatement line 571
  34. lemma OAI.MicroscopicJamming.rowCascadeProfile_sum line 588
  35. lemma OAI.MicroscopicJamming.rowIncrementSum_filter line 621
  36. theorem OAI.MicroscopicJamming.rowRefinementCovariance line 631