OAI/Analysis/PeriodicLattice/Certificates.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Quantitative certificates for planar derivatives and products.

  1. structure OAI.PeriodicLattice.Quantitative.BiCertificate line 18
  2. theorem OAI.PeriodicLattice.Quantitative.word_mul_estimate line 25
  3. def OAI.PeriodicLattice.Quantitative.BiCertificate.diff line 56
  4. def OAI.PeriodicLattice.Quantitative.BiCertificate.add line 65
  5. def OAI.PeriodicLattice.Quantitative.BiCertificate.scale line 77
  6. def OAI.PeriodicLattice.Quantitative.BiCertificate.mul line 87
  7. def OAI.PeriodicLattice.Quantitative.BiCertificate.mean line 104
  8. def OAI.PeriodicLattice.Quantitative.BiCertificate.first line 120
  9. def OAI.PeriodicLattice.Quantitative.planarBudget line 139
  10. theorem OAI.PeriodicLattice.Quantitative.planarBudget_recursive line 144
  11. theorem OAI.PeriodicLattice.Quantitative.planarBudget_bound line 152
  12. def OAI.PeriodicLattice.Quantitative.aCertificate line 184
  13. def OAI.PeriodicLattice.Quantitative.bCertificate line 196
  14. structure OAI.PeriodicLattice.Quantitative.ProfileCertificate line 208
  15. def OAI.PeriodicLattice.Quantitative.ProfileCertificate.one line 215
  16. def OAI.PeriodicLattice.Quantitative.ProfileCertificate.neg line 221
  17. theorem OAI.PeriodicLattice.Quantitative.vertical_derivative_bound line 228
  18. def OAI.PeriodicLattice.Quantitative.etaCertificate line 253
  19. def OAI.PeriodicLattice.Quantitative.slopeCertificate line 260
  20. def OAI.PeriodicLattice.Quantitative.BiCertificate.neg line 268
  21. def OAI.PeriodicLattice.Quantitative.BiCertificate.sub line 271
  22. def OAI.PeriodicLattice.Quantitative.pressureSourceCertificate line 275
  23. def OAI.PeriodicLattice.Quantitative.pressureBaseCertificate line 279
  24. def OAI.PeriodicLattice.Quantitative.pressureModeCertificate line 282
  25. theorem OAI.PeriodicLattice.Quantitative.trig_iterated_bound line 285
  26. def OAI.PeriodicLattice.Quantitative.doubleSlopeCertificate line 292