OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TailDifferentiability.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.TailSpace.ContinuousTails line 14
  2. def OAI.VelocityDetection.TailSpace.C1Tails line 18
  3. def OAI.VelocityDetection.TailSpace.evalLinear line 24

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:353 (same declaration text).

  4. def OAI.VelocityDetection.TailSpace.eval line 29

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:358 (same declaration text).

  5. theorem OAI.VelocityDetection.TailSpace.eval_apply line 36
  6. theorem OAI.VelocityDetection.TailSpace.ContinuousTails.integrable line 38
  7. theorem OAI.VelocityDetection.TailSpace.ContinuousTails.memLp line 46
  8. theorem OAI.VelocityDetection.TailSpace.ContinuousTails.cylinderL2 line 51
  9. theorem OAI.VelocityDetection.TailSpace.ContinuousTails.bounded line 59
  10. theorem OAI.VelocityDetection.TailSpace.C1Tails.continuous line 71
  11. theorem OAI.VelocityDetection.TailSpace.hasDerivWithinAt_eval line 75
  12. theorem OAI.VelocityDetection.TailSpace.C1Tails.cylinderC1 line 81
  13. theorem OAI.VelocityDetection.TailSpace.continuousTails_zero line 105