OAI/Probability/JammingConcavity/RowVariableComparison.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Row Variable Comparison.

  1. lemma OAI.MicroscopicJamming.VariableDiffusion.backward_positive_strict_compact line 29
  2. lemma OAI.MicroscopicJamming.VariableDiffusion.polynomial_transport_neg line 84
  3. lemma OAI.MicroscopicJamming.VariableDiffusion.backward_polynomial_bound line 111
  4. lemma OAI.MicroscopicJamming.VariableDiffusion.backward_polynomial_comparison line 202
  5. lemma OAI.MicroscopicJamming.VariableDiffusion.backward_reaction_source_upper line 246
  6. lemma OAI.MicroscopicJamming.VariableDiffusion.backward_reaction_source_bound line 330
  7. lemma OAI.MicroscopicJamming.VariableDiffusion.polynomialBarrier_growth line 370
  8. lemma OAI.MicroscopicJamming.VariableDiffusion.backward_polynomial_source_upper line 385
  9. lemma OAI.MicroscopicJamming.VariableDiffusion.backward_polynomial_source_bound line 461
  10. def OAI.MicroscopicJamming.Higher.FamilyGrowth line 503
  11. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.const line 506
  12. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.of_bound line 510
  13. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.of_linear_bound line 514
  14. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.of_quadratic_bound line 518
  15. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.comp line 524
  16. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.add line 530
  17. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.mul line 544
  18. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.const_mul line 555
  19. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.sub line 559
  20. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.congr line 564
  21. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.finset_sum line 569
  22. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.individual line 579
  23. lemma OAI.MicroscopicJamming.Higher.FamilyGrowth.polynomial_source line 584
  24. def OAI.MicroscopicJamming.Higher.heatDomain line 606
  25. lemma OAI.MicroscopicJamming.Higher.heatDomain_open line 607
  26. lemma OAI.MicroscopicJamming.Higher.heatJet_hasFDeriv line 609
  27. lemma OAI.MicroscopicJamming.Higher.heatJet_contDiffOn line 645
  28. lemma OAI.MicroscopicJamming.Higher.heat_jointly_smooth line 663
  29. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_jointly_smooth line 669