OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarPulseExpressions.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Scalar expressions for the planar processor after its phase is installed as the third spatial coordinate. The expression contains only finite rational data and the existing certified smooth profile syntax.

  1. def OAI.ShearFlows.PeriodicExpr.quadratic line 15
  2. theorem OAI.ShearFlows.PeriodicExpr.quadratic_valid line 18
  3. theorem OAI.ShearFlows.PeriodicExpr.quadratic_body line 28
  4. def OAI.ShearFlows.PeriodicExpr.intervalPulse line 34
  5. theorem OAI.ShearFlows.PeriodicExpr.intervalPulse_valid line 37
  6. theorem OAI.ShearFlows.PeriodicExpr.val_on_unit line 43
  7. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.axisCutoff line 63
  8. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.axisLinear line 67
  9. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.axisQuadratic line 71
  10. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.axisCutoff_valid line 75
  11. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.axisLinear_valid line 79
  12. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.axisQuadratic_valid line 83
  13. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.spatialExpression line 87
  14. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.expression line 99
  15. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.spatialExpression_valid line 103
  16. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.expression_valid line 112
  17. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.spatialExpression_noTime line 115
  18. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.expression_noTime line 119
  19. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.spatialExpression_unitPeriods line 122
  20. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.expression_unitPeriods line 129
  21. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.InUnit line 132
  22. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.axisMask line 136
  23. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.axisCutoff_on_unit line 140
  24. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.axisLinear_on_unit line 149
  25. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.axisQuadratic_on_unit line 159
  26. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.spatialExpression_on_unit line 168
  27. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.expression_on_unit line 212
  28. def OAI.ForcedComputation.PlanarHamiltonian.processorExpression line 222
  29. theorem OAI.ForcedComputation.PlanarHamiltonian.processorExpression_valid line 225
  30. theorem OAI.ForcedComputation.PlanarHamiltonian.sum_noTime line 232
  31. theorem OAI.ForcedComputation.PlanarHamiltonian.sum_unitPeriods line 238
  32. theorem OAI.ForcedComputation.PlanarHamiltonian.processorExpression_noTime line 244
  33. theorem OAI.ForcedComputation.PlanarHamiltonian.processorExpression_unitPeriods line 251
  34. theorem OAI.ForcedComputation.PlanarHamiltonian.processorExpression_on_unit line 258
  35. theorem OAI.ForcedComputation.PlanarHamiltonian.processorExpression_planar_germ line 269
  36. theorem OAI.ForcedComputation.PlanarHamiltonian.processorExpression_planar_field line 284