OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/InitializedFluid.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The loaded program retains the analytic properties of its two shear fields.

  1. theorem OAI.ForcedComputation.force_zero line 14
  2. theorem OAI.ForcedComputation.force_eq_of_eventuallyEq line 19
  3. theorem OAI.ForcedComputation.initializedProgram_zero_extend line 25
  4. theorem OAI.ForcedComputation.initializedProgram_loading_extend line 33
  5. theorem OAI.ForcedComputation.initializedProgram_tail_extend line 50
  6. theorem OAI.ForcedComputation.initializedProgram_loading_germ line 63
  7. theorem OAI.ForcedComputation.initializedProgram_tail_germ line 72
  8. theorem OAI.ForcedComputation.initializedProgram_zero_germ line 80
  9. theorem OAI.ForcedComputation.initializedForce_loading line 88
  10. theorem OAI.ForcedComputation.initializedForce_tail line 95
  11. theorem OAI.ForcedComputation.initializedForce_before line 102
  12. theorem OAI.ForcedComputation.initializedProgram_eventually_periodic line 110
  13. theorem OAI.ForcedComputation.initializedForce_eventually_periodic line 116
  14. theorem OAI.ForcedComputation.initializedForce_bounded line 126
  15. theorem OAI.ForcedComputation.initializedForce_mean_zero line 142
  16. theorem OAI.ForcedComputation.initializedProgram_slice line 158
  17. theorem OAI.ForcedComputation.initializedProgram_integer_collars line 169
  18. theorem OAI.ForcedComputation.initializedForce_integer_collars line 179
  19. theorem OAI.ForcedComputation.initializedProgram_solenoidal line 191
  20. theorem OAI.ForcedComputation.initializedProgram_zero_advection line 203
  21. theorem OAI.ForcedComputation.initializedForce_solenoidal line 215
  22. theorem OAI.ForcedComputation.initializedProgram_mean_zero line 221
  23. theorem OAI.ForcedComputation.initializedProgram_solution line 231
  24. theorem OAI.ForcedComputation.initializedProgram_spatial_lipschitz line 241
  25. theorem OAI.ForcedComputation.initializedProgram_materialFlow line 267
  26. theorem OAI.ForcedComputation.initializedProgram_unique line 278
  27. theorem OAI.ForcedComputation.initializedProgram_energy_bounded line 293