OAI/Analysis/PeriodicLattice/Basic.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Finite machines, computable names, torus fields and the lattice conclusion.

  1. theorem OAI.PeriodicLattice.neZeroThree line 9
  2. theorem OAI.PeriodicLattice.twoAtLeastTwo line 10
  3. theorem OAI.PeriodicLattice.threeAtLeastTwo line 11
  4. theorem OAI.PeriodicLattice.fourAtLeastTwo line 12
  5. theorem OAI.PeriodicLattice.eightAtLeastTwo line 13
  6. structure OAI.PeriodicLattice.Instruction line 18
  7. def OAI.PeriodicLattice.Instruction.codeEquiv line 24
  8. instance OAI.PeriodicLattice.(instance at line 30) line 30
  9. structure OAI.PeriodicLattice.Machine line 32
  10. def OAI.PeriodicLattice.Machine.codeEquiv line 39
  11. instance OAI.PeriodicLattice.(instance at line 45) line 45
  12. def OAI.PeriodicLattice.Machine.lookup line 47
  13. def OAI.PeriodicLattice.Machine.WellFormed line 50
  14. structure OAI.PeriodicLattice.Input line 57
  15. def OAI.PeriodicLattice.Input.codeEquiv line 62
  16. instance OAI.PeriodicLattice.(instance at line 68) line 68
  17. def OAI.PeriodicLattice.Input.WellFormed line 70
  18. structure OAI.PeriodicLattice.Configuration line 73
  19. def OAI.PeriodicLattice.initialConfiguration line 78
  20. def OAI.PeriodicLattice.machineStep line 83
  21. def OAI.PeriodicLattice.execution line 91
  22. def OAI.PeriodicLattice.Halts line 94
  23. abbrev OAI.PeriodicLattice.Space line 98
  24. abbrev OAI.PeriodicLattice.Torus line 99
  25. abbrev OAI.PeriodicLattice.Field line 100
  26. abbrev OAI.PeriodicLattice.VectorField line 101
  27. abbrev OAI.PeriodicLattice.ScalarField line 102
  28. abbrev OAI.PeriodicLattice.MultiIndex line 103
  29. def OAI.PeriodicLattice.torusMk line 107
  30. def OAI.PeriodicLattice.torusVolume line 109
  31. def OAI.PeriodicLattice.initialParticle line 112
  32. def OAI.PeriodicLattice.detector line 114
  33. def OAI.PeriodicLattice.lifted line 120
  34. def OAI.PeriodicLattice.spaceLift line 123
  35. def OAI.PeriodicLattice.Smooth line 126
  36. def OAI.PeriodicLattice.timeD line 129
  37. def OAI.PeriodicLattice.spaceD line 132
  38. def OAI.PeriodicLattice.mixedD line 136
  39. def OAI.PeriodicLattice.laplacian line 139
  40. def OAI.PeriodicLattice.MeanZero line 142
  41. def OAI.PeriodicLattice.spatialSup line 145
  42. def OAI.PeriodicLattice.CylinderContinuous line 148
  43. def OAI.PeriodicLattice.gradient line 153
  44. def OAI.PeriodicLattice.divergence line 156
  45. def OAI.PeriodicLattice.advection line 159
  46. def OAI.PeriodicLattice.Solenoidal line 162
  47. def OAI.PeriodicLattice.NavierStokes line 165
  48. structure OAI.PeriodicLattice.ClassicalSolution line 171
  49. def OAI.PeriodicLattice.UniqueClassical line 185
  50. def OAI.PeriodicLattice.IsParticle line 189
  51. def OAI.PeriodicLattice.MaterialEvent line 193
  52. abbrev OAI.PeriodicLattice.Program line 196
  53. abbrev OAI.PeriodicLattice.RationalPoint line 197
  54. def OAI.PeriodicLattice.accuracy line 199
  55. def OAI.PeriodicLattice.ComputableReal line 203
  56. def OAI.PeriodicLattice.rationalVector line 207
  57. def OAI.PeriodicLattice.UniformlyEffective line 210
  58. def OAI.PeriodicLattice.EffectiveConstants line 222
  59. def OAI.PeriodicLattice.RapidPair line 226
  60. def OAI.PeriodicLattice.UniqueMeanZeroPoisson line 231
  61. def OAI.PeriodicLattice.LatticeConclusion line 237