OAI/Analysis/PeriodicLattice/FieldCertificates.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Uniform certificates for all field derivative words.

  1. def OAI.PeriodicLattice.Quantitative.coordD line 21
  2. def OAI.PeriodicLattice.Quantitative.fieldWord line 26
  3. theorem OAI.PeriodicLattice.Quantitative.fieldWord_nil line 28
  4. theorem OAI.PeriodicLattice.Quantitative.fieldWord_cons line 29
  5. theorem OAI.PeriodicLattice.Quantitative.fieldWord_append line 32
  6. theorem OAI.PeriodicLattice.Quantitative.coordD_contDiff line 35
  7. theorem OAI.PeriodicLattice.Quantitative.fieldWord_contDiff line 41
  8. theorem OAI.PeriodicLattice.Quantitative.coordD_add line 47
  9. theorem OAI.PeriodicLattice.Quantitative.fieldWord_add line 57
  10. theorem OAI.PeriodicLattice.Quantitative.coordD_scale line 64
  11. theorem OAI.PeriodicLattice.Quantitative.fieldWord_scale line 70
  12. theorem OAI.PeriodicLattice.Quantitative.coordD_zero line 76
  13. theorem OAI.PeriodicLattice.Quantitative.fieldWord_zero line 79
  14. structure OAI.PeriodicLattice.Quantitative.FieldCertificate line 84
  15. def OAI.PeriodicLattice.Quantitative.FieldCertificate.diff line 92
  16. def OAI.PeriodicLattice.Quantitative.FieldCertificate.add line 101
  17. def OAI.PeriodicLattice.Quantitative.FieldCertificate.scale line 113
  18. def OAI.PeriodicLattice.Quantitative.FieldCertificate.neg line 123
  19. def OAI.PeriodicLattice.Quantitative.FieldCertificate.sub line 126
  20. def OAI.PeriodicLattice.Quantitative.FieldCertificate.zero line 129
  21. theorem OAI.PeriodicLattice.Quantitative.coordD_mul line 137
  22. theorem OAI.PeriodicLattice.Quantitative.fieldWord_mul_estimate line 147
  23. def OAI.PeriodicLattice.Quantitative.FieldCertificate.mul line 178
  24. theorem OAI.PeriodicLattice.Quantitative.fieldWord_tensor_estimate line 196
  25. def OAI.PeriodicLattice.Quantitative.FieldCertificate.tensor line 231
  26. theorem OAI.PeriodicLattice.Quantitative.coordD_component line 245
  27. theorem OAI.PeriodicLattice.Quantitative.fieldWord_component line 255
  28. def OAI.PeriodicLattice.Quantitative.FieldCertificate.components line 263
  29. def OAI.PeriodicLattice.Quantitative.FieldCertificate.component line 278
  30. def OAI.PeriodicLattice.Quantitative.FieldCertificate.diffusion line 288
  31. def OAI.PeriodicLattice.Quantitative.FieldCertificate.transport line 297
  32. def OAI.PeriodicLattice.Quantitative.FieldCertificate.gradient line 312
  33. def OAI.PeriodicLattice.Quantitative.FieldCertificate.residual line 316
  34. def OAI.PeriodicLattice.Quantitative.velocityCertificate line 321
  35. def OAI.PeriodicLattice.Quantitative.potentialCertificate line 328
  36. def OAI.PeriodicLattice.Quantitative.forceCertificate line 333
  37. def OAI.PeriodicLattice.Quantitative.solenoidalForceCertificate line 336
  38. theorem OAI.PeriodicLattice.Quantitative.fieldWord_replicate line 343
  39. def OAI.PeriodicLattice.Quantitative.spatialWord line 349
  40. def OAI.PeriodicLattice.Quantitative.mixedWord line 351
  41. theorem OAI.PeriodicLattice.Quantitative.mixedD_eq_fieldWord line 354
  42. def OAI.PeriodicLattice.Quantitative.mixedOrder line 363
  43. theorem OAI.PeriodicLattice.Quantitative.mixedOrder_recursive line 365
  44. def OAI.PeriodicLattice.Quantitative.FieldCertificate.mixedBudget line 371
  45. theorem OAI.PeriodicLattice.Quantitative.FieldCertificate.mixedBudget_recursive line 374
  46. theorem OAI.PeriodicLattice.Quantitative.FieldCertificate.mixed_estimate line 379
  47. theorem OAI.PeriodicLattice.Quantitative.FieldCertificate.sup_estimate line 386