OAI/Probability/JammingConcavity/RowFiniteDiagonalRowGeneralInterpolation.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Row Finite Diagonal Row General Interpolation.

  1. structure OAI.MicroscopicJamming.RowExtensionData line 67
  2. lemma OAI.MicroscopicJamming.rowExtension_exists line 84
  3. lemma OAI.MicroscopicJamming.RowExtensionData.finite_value line 91
  4. lemma OAI.MicroscopicJamming.RowExtensionData.finite_derivative line 97
  5. lemma OAI.MicroscopicJamming.RowExtensionData.pairing_continuous line 103
  6. def OAI.MicroscopicJamming.rowGaussianPairBlocks line 119
  7. lemma OAI.MicroscopicJamming.rowGaussianPairBlocks_left line 123
  8. lemma OAI.MicroscopicJamming.rowGaussianPairBlocks_right line 128
  9. lemma OAI.MicroscopicJamming.rowGaussianPairBlocks_ranks line 133
  10. lemma OAI.MicroscopicJamming.rowGaussianBlocks_total line 137
  11. lemma OAI.MicroscopicJamming.rowGaussianPairBlocks_valid line 143
  12. def OAI.MicroscopicJamming.rowNNMix line 157
  13. lemma OAI.MicroscopicJamming.rowNNMix_coe line 159
  14. lemma OAI.MicroscopicJamming.rowGaussianPairBlocks_interpolated line 164
  15. lemma OAI.MicroscopicJamming.rowGaussianBlocks_mix_cumulative line 174
  16. def OAI.MicroscopicJamming.RowFiniteProfile.mix line 196
  17. lemma OAI.MicroscopicJamming.RowFiniteProfile.mix_profile line 215
  18. def OAI.MicroscopicJamming.RowFiniteProfile.pairBlocks line 230
  19. lemma OAI.MicroscopicJamming.RowFiniteProfile.pairBlocks_left line 233
  20. lemma OAI.MicroscopicJamming.RowFiniteProfile.pairBlocks_right line 237
  21. lemma OAI.MicroscopicJamming.RowFiniteProfile.pairBlocks_valid line 241
  22. lemma OAI.MicroscopicJamming.RowFiniteProfile.pairBlocks_sorted line 249
  23. lemma OAI.MicroscopicJamming.RowFiniteProfile.pairBlocks_total line 254
  24. lemma OAI.MicroscopicJamming.RowFiniteProfile.pairBlocks_interpolated line 270
  25. lemma OAI.MicroscopicJamming.rowDerivativeRankMoment_append_terminal line 284
  26. lemma OAI.MicroscopicJamming.rowFullBlocks_profile line 299
  27. lemma OAI.MicroscopicJamming.rowFullBlocks_derivative line 305
  28. lemma OAI.MicroscopicJamming.rowFiniteSubFTC line 322
  29. lemma OAI.MicroscopicJamming.RowExtensionData.finite_pairing line 363
  30. lemma OAI.MicroscopicJamming.rowFiniteProfileFTC line 372
  31. lemma OAI.MicroscopicJamming.rowProfileMix_tendsto line 411
  32. lemma OAI.MicroscopicJamming.rowProfile_distance_le line 419
  33. lemma OAI.MicroscopicJamming.rowGeneralFTC line 432
  34. lemma OAI.MicroscopicJamming.rowGeneral_hasDerivWithinAt line 473
  35. lemma OAI.MicroscopicJamming.rowGeneral_lipschitz line 488
  36. lemma OAI.MicroscopicJamming.rowRankDerivative_segment line 517
  37. lemma OAI.MicroscopicJamming.sphericalProfile_plateau_pointwise line 546
  38. lemma OAI.MicroscopicJamming.rowGaussianBlocks_mem_index line 568
  39. lemma OAI.MicroscopicJamming.rowGrid_derivative_plateau line 586
  40. lemma OAI.MicroscopicJamming.profileCompactFilter_pointwise line 633
  41. lemma OAI.MicroscopicJamming.sphericalProfileDistance_zero_ae line 663
  42. lemma OAI.MicroscopicJamming.rowGeneral_plateau line 680
  43. theorem OAI.MicroscopicJamming.rowGeneralInterpolation line 724