OAI/Probability/JammingConcavity/RowFiniteDiagonalRowDirectionPairingTendsto.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Row Finite Diagonal Row Direction Pairing Tendsto.

  1. def OAI.MicroscopicJamming.RowFiniteFTCStatement line 66
  2. lemma OAI.MicroscopicJamming.rowBoundedFamily_composed_continuousAt line 87
  3. lemma OAI.MicroscopicJamming.rowOperator_parameter_continuousAt line 104
  4. lemma OAI.MicroscopicJamming.rowVarianceComposition_continuous line 174
  5. theorem OAI.MicroscopicJamming.rowFiniteFTC line 194
  6. def OAI.MicroscopicJamming.RowFiniteProfile.functional line 227
  7. def OAI.MicroscopicJamming.RowFiniteFunctionalStatement line 232
  8. lemma OAI.MicroscopicJamming.gaussianRowComposition_append_eq line 245
  9. lemma OAI.MicroscopicJamming.integrable_cascade_coordinates line 251
  10. lemma OAI.MicroscopicJamming.replica_log_integrable line 270
  11. lemma OAI.MicroscopicJamming.rowResidual_partition_pointwise line 284
  12. theorem OAI.MicroscopicJamming.rowGaussianCascade line 299
  13. lemma OAI.MicroscopicJamming.rowFiniteFunctional_log_integrable line 334
  14. lemma OAI.MicroscopicJamming.familyCoordinate_log_expectation line 343
  15. theorem OAI.MicroscopicJamming.rowFiniteFunctional line 361
  16. abbrev OAI.MicroscopicJamming.RowProfile line 414
  17. def OAI.MicroscopicJamming.rowUnitClip line 415
  18. lemma OAI.MicroscopicJamming.rowUnitClip_mem line 416
  19. lemma OAI.MicroscopicJamming.rowUnitClip_eq line 418
  20. def OAI.MicroscopicJamming.rowProfileMix line 422
  21. def OAI.MicroscopicJamming.RowGeneralInterpolationStatement line 438
  22. lemma OAI.MicroscopicJamming.rowUnitClip_continuous line 466
  23. lemma OAI.MicroscopicJamming.rowProfileMix_zero line 467
  24. lemma OAI.MicroscopicJamming.rowProfileMix_one line 472
  25. lemma OAI.MicroscopicJamming.rowFiniteProfile_top_le line 478
  26. def OAI.MicroscopicJamming.RowFiniteProfile.asProfile line 493
  27. lemma OAI.MicroscopicJamming.rowProfileMix_distance line 495
  28. lemma OAI.MicroscopicJamming.rowProfileMix_parameter_distance line 514
  29. lemma OAI.MicroscopicJamming.rowProfileMix_parameter_tendsto line 528
  30. lemma OAI.MicroscopicJamming.rowFunctional_converges line 541
  31. lemma OAI.MicroscopicJamming.rowFunctionalLimits_eq line 548
  32. lemma OAI.MicroscopicJamming.rowGeneralFunctional line 573
  33. lemma OAI.MicroscopicJamming.rowProfile_mul_integrable line 619
  34. lemma OAI.MicroscopicJamming.rowDirection_integrable line 628
  35. def OAI.MicroscopicJamming.rowDirectionPairing line 632
  36. lemma OAI.MicroscopicJamming.rowDirectionPairing_bound line 635
  37. lemma OAI.MicroscopicJamming.rowDirectionPairing_difference_bound line 648
  38. lemma OAI.MicroscopicJamming.rowProfile_difference_bound line 681
  39. lemma OAI.MicroscopicJamming.rowDirectionPairing_tendsto line 687