OAI/MathematicalPhysics/AlternatingFlow/Model.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AlternatingNS.neZeroThree line 9
2. theorem OAI.AlternatingNS.twoAtLeastTwo line 11
3. theorem OAI.AlternatingNS.threeAtLeastTwo line 13
4. theorem OAI.AlternatingNS.eightAtLeastTwo line 15
5. abbrev OAI.AlternatingNS.Rule line 17

   Also declared: ComparatorChallenges/NavierStokesAlternating.lean:10 (same declaration text).

6. abbrev OAI.AlternatingNS.Machine line 19

   Also declared: ComparatorChallenges/NavierStokesAlternating.lean:12 (same declaration text).

7. def OAI.AlternatingNS.Machine.states line 23

   Also declared: ComparatorChallenges/NavierStokesAlternating.lean:16 (same declaration text).

8. def OAI.AlternatingNS.Machine.alphabet line 25

   Also declared: ComparatorChallenges/NavierStokesAlternating.lean:18 (same declaration text).

9. def OAI.AlternatingNS.Machine.initialState line 27

   Also declared: ComparatorChallenges/NavierStokesAlternating.lean:20 (same declaration text).

10. def OAI.AlternatingNS.Machine.haltingStates line 29

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:22 (same declaration text).

11. def OAI.AlternatingNS.Machine.table line 31

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:24 (same declaration text).

12. def OAI.AlternatingNS.Machine.instruction line 33

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:26 (same declaration text).

13. def OAI.AlternatingNS.Machine.WellFormed line 36

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:29 (same declaration text).

14. def OAI.AlternatingNS.Machine.ValidInput line 42

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:35 (same declaration text).

15. structure OAI.AlternatingNS.Machine.Configuration line 45

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:38 (same declaration text).

16. def OAI.AlternatingNS.Machine.isHalting line 50

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:43 (same declaration text).

17. def OAI.AlternatingNS.Machine.initial line 53

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:46 (same declaration text).

18. def OAI.AlternatingNS.Machine.step line 58

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:51 (same declaration text).

19. def OAI.AlternatingNS.Machine.run line 67

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:60 (same declaration text).

20. def OAI.AlternatingNS.Machine.Halts line 70

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:63 (same declaration text).

21. abbrev OAI.AlternatingNS.Space line 75

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:68 (same declaration text).

22. abbrev OAI.AlternatingNS.Field line 76

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:69 (same declaration text).

23. abbrev OAI.AlternatingNS.Velocity line 77

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:70 (same declaration text).

24. abbrev OAI.AlternatingNS.Pressure line 78

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:71 (same declaration text).

25. abbrev OAI.AlternatingNS.MultiIndex line 79

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:72 (same declaration text).

26. def OAI.AlternatingNS.e line 83

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:76 (same declaration text).

27. def OAI.AlternatingNS.dx line 85

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:78 (same declaration text).

28. def OAI.AlternatingNS.dt line 89

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:82 (same declaration text).

29. def OAI.AlternatingNS.spatial line 93

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:86 (same declaration text).

30. def OAI.AlternatingNS.mixed line 97

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:90 (same declaration text).

31. def OAI.AlternatingNS.div line 101

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:94 (same declaration text).

32. def OAI.AlternatingNS.grad line 104

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:97 (same declaration text).

33. def OAI.AlternatingNS.laplacian line 107

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:100 (same declaration text).

34. def OAI.AlternatingNS.advection line 110

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:103 (same declaration text).

35. def OAI.AlternatingNS.residual line 113

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:106 (same declaration text).

36. def OAI.AlternatingNS.timeCylinder line 116

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:109 (same declaration text).

37. def OAI.AlternatingNS.Smooth line 118

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:111 (same declaration text).

38. def OAI.AlternatingNS.ClassicalRegularity line 122

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:115 (same declaration text).

39. def OAI.AlternatingNS.ContinuousInH line 135

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:128 (same declaration text).

40. def OAI.AlternatingNS.C1InL2 line 143

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:136 (same declaration text).

41. def OAI.AlternatingNS.CompetitorEnergyClass line 151

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:144 (same declaration text).

42. def OAI.AlternatingNS.EnergyClass line 156

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:149 (same declaration text).

43. def OAI.AlternatingNS.NavierStokes line 161

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:154 (same declaration text).

44. def OAI.AlternatingNS.Rapid line 168

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:161 (same declaration text).

45. def OAI.AlternatingNS.SupportedIn line 173

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:166 (same declaration text).

46. def OAI.AlternatingNS.IsTrajectory line 176

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:169 (same declaration text).

47. def OAI.AlternatingNS.observedParticle line 179

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:172 (same declaration text).

48. abbrev OAI.AlternatingNS.RationalPoint line 181

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:174 (same declaration text).

49. abbrev OAI.AlternatingNS.RationalVector line 182

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:175 (same declaration text).

50. abbrev OAI.AlternatingNS.IndexCode line 183

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:176 (same declaration text).

51. abbrev OAI.AlternatingNS.Program line 184

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:177 (same declaration text).

52. abbrev OAI.AlternatingNS.FieldProgram line 185

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:178 (same declaration text).

53. def OAI.AlternatingNS.Returns line 187

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:180 (same declaration text).

54. def OAI.AlternatingNS.index line 191

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:184 (same declaration text).

55. def OAI.AlternatingNS.rationalVector line 193

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:186 (same declaration text).

56. def OAI.AlternatingNS.rationalPoint line 196

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:189 (same declaration text).

57. def OAI.AlternatingNS.dyadicError line 199

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:192 (same declaration text).

58. def OAI.AlternatingNS.ComputableReal line 201

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:194 (same declaration text).

59. def OAI.AlternatingNS.ProgramFor line 205

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:198 (same declaration text).

60. def OAI.AlternatingNS.AlternatingConclusion line 222

    Also declared: ComparatorChallenges/NavierStokesAlternating.lean:215 (same declaration text).