OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BalancedTransport.Recorder.Direction line 8

   Also declared: ComparatorChallenges/BalancedThreeStack.lean:7 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:8 (same declaration text).

2. instance OAI.BalancedTransport.Recorder.(instance at line 12) line 12
3. structure OAI.BalancedTransport.Recorder.Transition line 15

   Also declared: ComparatorChallenges/BalancedThreeStack.lean:14 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:12 (same declaration text).

4. structure OAI.BalancedTransport.FiniteMachine line 26

   Also declared: ComparatorChallenges/BalancedThreeStack.lean:20 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:18 (same declaration text).

5. abbrev OAI.BalancedTransport.Input line 34

   Also declared: ComparatorChallenges/BalancedThreeStack.lean:28 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:26 (same declaration text).

6. structure OAI.BalancedTransport.TapeConfiguration line 36

   Also declared: ComparatorChallenges/BalancedThreeStack.lean:30 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:28 (same declaration text).

7. def OAI.BalancedTransport.initialConfiguration line 41

   Also declared: ComparatorChallenges/BalancedThreeStack.lean:35 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:33 (same declaration text).

8. def OAI.BalancedTransport.machineStep line 44

   Also declared: ComparatorChallenges/BalancedThreeStack.lean:38 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:36 (same declaration text).

9. def OAI.BalancedTransport.Halts line 49

   Also declared: ComparatorChallenges/BalancedThreeStack.lean:43 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:41 (same declaration text).

10. def OAI.BalancedTransport.Recorder.Direction.number line 53

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:47 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:45 (same declaration text).

11. def OAI.BalancedTransport.FiniteMachine.code line 58

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:52 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:50 (same declaration text).

12. def OAI.BalancedTransport.inputCode line 64

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:58 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:56 (same declaration text).

13. abbrev OAI.BalancedTransport.Space line 67

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:61 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:59 (same declaration text).

14. abbrev OAI.BalancedTransport.Field line 69

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:62 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:60 (same declaration text).

15. abbrev OAI.BalancedTransport.Velocity line 71

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:63 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:61 (same declaration text).

16. abbrev OAI.BalancedTransport.Pressure line 73

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:64 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:62 (same declaration text).

17. abbrev OAI.BalancedTransport.Family line 75

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:65 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:63 (same declaration text).

18. abbrev OAI.BalancedTransport.MaterialFlow line 77

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:66 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:64 (same declaration text).

19. abbrev OAI.BalancedTransport.MultiIndex line 79

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:67 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:65 (same declaration text).

20. abbrev OAI.BalancedTransport.RationalPoint line 81

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:68 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:66 (same declaration text).

21. def OAI.BalancedTransport.timeD line 92

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:77 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:75 (same declaration text).

22. def OAI.BalancedTransport.spaceD line 95

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:80 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:78 (same declaration text).

23. def OAI.BalancedTransport.mixedD line 98

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:83 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:81 (same declaration text).

24. def OAI.BalancedTransport.spatialD line 103

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:88 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:86 (same declaration text).

25. def OAI.BalancedTransport.Smooth line 107

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:92 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:90 (same declaration text).

26. def OAI.BalancedTransport.BoundedMixed line 110

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:95 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:93 (same declaration text).

27. def OAI.BalancedTransport.CH line 113

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:98 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:96 (same declaration text).

28. def OAI.BalancedTransport.C1L2 line 119

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:104 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:102 (same declaration text).

29. def OAI.BalancedTransport.div line 127

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:112 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:110 (same declaration text).

30. def OAI.BalancedTransport.laplacian line 130

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:115 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:113 (same declaration text).

31. def OAI.BalancedTransport.convection line 133

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:118 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:116 (same declaration text).

32. def OAI.BalancedTransport.gradient line 136

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:121 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:119 (same declaration text).

33. def OAI.BalancedTransport.affineForce line 139

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:124 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:122 (same declaration text).

34. def OAI.BalancedTransport.inertialCoefficient line 142

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:127 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:125 (same declaration text).

35. def OAI.BalancedTransport.viscousCoefficient line 145

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:130 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:128 (same declaration text).

36. def OAI.BalancedTransport.ZeroDataSolution line 148

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:133 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:131 (same declaration text).

37. def OAI.BalancedTransport.BoundedOnFiniteSlabs line 156

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:141 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:139 (same declaration text).

38. def OAI.BalancedTransport.ComparisonClass line 161

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:146 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:144 (same declaration text).

39. def OAI.BalancedTransport.UniqueInComparison line 165

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:150 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:148 (same declaration text).

40. def OAI.BalancedTransport.CommonCompactSupport line 170

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:155 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:153 (same declaration text).

41. def OAI.BalancedTransport.PeriodicAfterOne line 174

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:159 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:157 (same declaration text).

42. def OAI.BalancedTransport.IsMaterialFlow line 177

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:162 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:160 (same declaration text).

43. def OAI.BalancedTransport.fixedLabel line 181

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:166 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:164 (same declaration text).

44. def OAI.BalancedTransport.observer line 183

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:168 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:166 (same declaration text).

45. def OAI.BalancedTransport.rationalSpace line 186

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:171 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:169 (same declaration text).

46. def OAI.BalancedTransport.error line 188

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:173 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:171 (same declaration text).

47. def OAI.BalancedTransport.EffectiveFamily line 190

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:175 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:173 (same declaration text).

48. def OAI.BalancedTransport.EffectiveFieldIn line 203

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:188 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:186 (same declaration text).

49. def OAI.BalancedTransport.RealName line 212

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:197 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:195 (same declaration text).

50. def OAI.BalancedTransport.ComputableReal line 215

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:200 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:198 (same declaration text).

51. def OAI.BalancedTransport.nameOracle line 218

    Also declared: ComparatorChallenges/BalancedThreeStack.lean:203 (same declaration text), ComparatorChallenges/ForcedNavierStokesComputation.lean:201 (same declaration text).