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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Integration on the fixed unit interval as a bounded linear operator. This permits elapsed time to be a parameter of the Picard equation.

  1. abbrev OAI.ForcedComputation.Flow.UnitTime line 15
  2. def OAI.ForcedComputation.Flow.extendPath line 19
  3. theorem OAI.ForcedComputation.Flow.extendPath_apply line 23
  4. theorem OAI.ForcedComputation.Flow.extendPath_coe line 27
  5. def OAI.ForcedComputation.Flow.primitivePath line 30
  6. theorem OAI.ForcedComputation.Flow.primitivePath_apply line 36
  7. theorem OAI.ForcedComputation.Flow.primitivePath_norm line 39
  8. def OAI.ForcedComputation.Flow.primitivePathL line 50
  9. theorem OAI.ForcedComputation.Flow.primitivePathL_apply line 71
  10. theorem OAI.ForcedComputation.Flow.primitivePathL_norm line 74