OAI/Probability/JammingConcavity/RowZeroRefinementClosure.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Row Zero Refinement Closure.

  1. lemma OAI.MicroscopicJamming.replica_coordinate_map line 65
  2. lemma OAI.MicroscopicJamming.gaussianAdjunction_constant_snd line 80
  3. lemma OAI.MicroscopicJamming.rowSingleField_law line 95
  4. lemma OAI.MicroscopicJamming.rowExpAbs_gaussian_integrable line 133
  5. lemma OAI.MicroscopicJamming.rowUniformMoments line 147
  6. lemma OAI.MicroscopicJamming.replica_cauchy_of_uniform_approx line 179
  7. lemma OAI.MicroscopicJamming.replica_integrable_of_bound line 194
  8. lemma OAI.MicroscopicJamming.replica_cauchy_polynomial_moments line 200
  9. lemma OAI.MicroscopicJamming.replica_cauchy_continuous_moments line 231
  10. lemma OAI.MicroscopicJamming.replica_product_between line 282
  11. lemma OAI.MicroscopicJamming.replica_product_integral_difference line 296
  12. lemma OAI.MicroscopicJamming.replica_density_difference line 363
  13. lemma OAI.MicroscopicJamming.replica_normalized_integral_eq line 396
  14. lemma OAI.MicroscopicJamming.replica_normalized_integral_difference line 407
  15. lemma OAI.MicroscopicJamming.replicaClip_mem line 435
  16. lemma OAI.MicroscopicJamming.replicaClip_abs_le line 440
  17. lemma OAI.MicroscopicJamming.replicaClip_eq_of_abs_le line 446
  18. lemma OAI.MicroscopicJamming.measurable_replicaClip line 449
  19. lemma OAI.MicroscopicJamming.continuous_replicaClip line 453
  20. lemma OAI.MicroscopicJamming.replica_exp_clip_difference line 457
  21. lemma OAI.MicroscopicJamming.replica_integrable_exp_abs_mono line 474
  22. lemma OAI.MicroscopicJamming.replica_inverse_Z_bound line 484
  23. lemma OAI.MicroscopicJamming.replica_moment_square_le line 521
  24. lemma OAI.MicroscopicJamming.replica_abs_log_bound line 545
  25. lemma OAI.MicroscopicJamming.replica_abs_log_sub_bound line 551
  26. lemma OAI.MicroscopicJamming.replica_clip_exp_integrable line 583
  27. lemma OAI.MicroscopicJamming.replica_clip_Z_bounds line 592
  28. lemma OAI.MicroscopicJamming.replica_weighted_product_bound line 603
  29. lemma OAI.MicroscopicJamming.replica_fiber_log_estimates line 620
  30. lemma OAI.MicroscopicJamming.replica_fiber_tilt_estimates line 674