OAI/Probability/JammingConcavity/RowMixedCalculus.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Row Mixed Calculus.

  1. def OAI.MicroscopicJamming.Higher.spacePartial line 30
  2. def OAI.MicroscopicJamming.Higher.timePartial line 33
  3. lemma OAI.MicroscopicJamming.Higher.spacePartial_eq_fderiv line 36
  4. lemma OAI.MicroscopicJamming.Higher.timePartial_eq_fderiv line 40
  5. lemma OAI.MicroscopicJamming.Higher.partial_space_smooth line 45
  6. lemma OAI.MicroscopicJamming.Higher.partial_time_smooth line 51
  7. lemma OAI.MicroscopicJamming.Higher.partial_time_space_commute line 58
  8. lemma OAI.MicroscopicJamming.Higher.iterated_space_smooth line 83
  9. lemma OAI.MicroscopicJamming.Higher.time_iterated_space line 100
  10. lemma OAI.MicroscopicJamming.Higher.normalizedHeatJet_iterated_continuous line 128
  11. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_iterated_continuous line 156
  12. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_iterated_growth line 181
  13. lemma OAI.MicroscopicJamming.Higher.iteratedDeriv_iteratedDeriv line 224
  14. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_jet_equation line 228
  15. lemma OAI.MicroscopicJamming.Higher.jet_square_decompose line 280
  16. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_higher_equation line 313
  17. lemma OAI.MicroscopicJamming.Higher.gaussianRowOperator_jet_bound line 327
  18. lemma OAI.MicroscopicJamming.Higher.jet_source_bound line 399
  19. lemma OAI.MicroscopicJamming.Higher.gaussianRowComposition_all_jets line 419
  20. lemma OAI.MicroscopicJamming.CylinderConvergence.deriv_and_differentiable line 543
  21. lemma OAI.MicroscopicJamming.CylinderConvergence.all_jets line 557
  22. lemma OAI.MicroscopicJamming.continuousOn_all_jets line 603
  23. lemma OAI.MicroscopicJamming.row_variance_all_jets line 622
  24. def OAI.MicroscopicJamming.Higher.JointSpatialSmooth line 661
  25. lemma OAI.MicroscopicJamming.Higher.JointSpatialSmooth.jet line 665
  26. lemma OAI.MicroscopicJamming.Higher.JointSpatialSmooth.add line 674
  27. lemma OAI.MicroscopicJamming.Higher.JointSpatialSmooth.coeff_mul line 683
  28. lemma OAI.MicroscopicJamming.Higher.JointSpatialSmooth.mul line 691
  29. lemma OAI.MicroscopicJamming.Higher.JointSpatialSmooth.row_rhs line 705