OAI/Probability/JammingConcavity/RowZeroRefinementClosureProfileDistanceEqZeroOfTests.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Row Zero Refinement Closure Profile Distance Eq Zero Of Tests.

  1. lemma OAI.MicroscopicJamming.replica_ensemble_clipping_errors line 65
  2. lemma OAI.MicroscopicJamming.replica_cauchy_clipped line 126
  3. lemma OAI.MicroscopicJamming.replica_small_exp_tail line 172
  4. theorem OAI.MicroscopicJamming.replicaTruncation line 180
  5. lemma OAI.MicroscopicJamming.replica_integral_snoc line 228
  6. lemma OAI.MicroscopicJamming.replicaFirst_snoc line 237
  7. lemma OAI.MicroscopicJamming.replica_integral_split line 242
  8. lemma OAI.MicroscopicJamming.replica_integral_all_products line 273
  9. lemma OAI.MicroscopicJamming.measurable_replicaFieldView line 295
  10. lemma OAI.MicroscopicJamming.replica_exp_clip_product_bound line 306
  11. def OAI.MicroscopicJamming.replicaTailTest line 314
  12. def OAI.MicroscopicJamming.replicaFullTest line 323
  13. lemma OAI.MicroscopicJamming.replica_tail_law_moment line 335
  14. lemma OAI.MicroscopicJamming.replica_full_law_moment line 359
  15. theorem OAI.MicroscopicJamming.replicaLawContinuity line 390
  16. def OAI.MicroscopicJamming.RowFiniteProfile.mesh line 421
  17. lemma OAI.MicroscopicJamming.rowTestExtend_bound line 430
  18. lemma OAI.MicroscopicJamming.rowFullPair_mesh_bound line 434
  19. lemma OAI.MicroscopicJamming.measurable_rowFullPotential line 443
  20. lemma OAI.MicroscopicJamming.measurable_rowFullPair line 446
  21. lemma OAI.MicroscopicJamming.rowMeshExpectation_converges line 458
  22. lemma OAI.MicroscopicJamming.measurable_rankMeshValue line 497
  23. lemma OAI.MicroscopicJamming.RowFiniteProfile.test_fubini line 500
  24. lemma OAI.MicroscopicJamming.rowMeshExpectation_eq_test line 531
  25. lemma OAI.MicroscopicJamming.rowProfileTest_error_tendsto line 552
  26. lemma OAI.MicroscopicJamming.rowProfileTest_integrable line 584
  27. theorem OAI.MicroscopicJamming.rowProfileTestConvergence line 597
  28. lemma OAI.MicroscopicJamming.profileTest_lipschitz line 625
  29. lemma OAI.MicroscopicJamming.profileTest_tendsto_of_L1 line 644
  30. lemma OAI.MicroscopicJamming.profileTest_closed line 654
  31. lemma OAI.MicroscopicJamming.profile_ae_eq_of_tests line 663
  32. lemma OAI.MicroscopicJamming.profileDistance_eq_zero_of_tests line 697