OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TailSpace.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.TailSpace.compatible line 14

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

  2. theorem OAI.VelocityDetection.TailSpace.memLp_two line 32
  3. theorem OAI.VelocityDetection.TailSpace.integral_sq_le line 44
  4. theorem OAI.VelocityDetection.TailSpace.L2_norm_sq line 56
  5. theorem OAI.VelocityDetection.TailSpace.member_memLp line 63
  6. def OAI.VelocityDetection.TailSpace.toL2Linear line 67
  7. theorem OAI.VelocityDetection.TailSpace.norm_toL2Linear_sq_le line 87
  8. theorem OAI.VelocityDetection.TailSpace.norm_toL2Linear_le line 96
  9. def OAI.VelocityDetection.TailSpace.toL2 line 104
  10. theorem OAI.VelocityDetection.TailSpace.coeFn_toL2 line 109
  11. theorem OAI.VelocityDetection.TailSpace.continuousOn_L2 line 113
  12. theorem OAI.VelocityDetection.TailSpace.hasDerivWithinAt_compatible line 122
  13. theorem OAI.VelocityDetection.TailSpace.hasDerivWithinAt_L2 line 134
  14. theorem OAI.VelocityDetection.TailSpace.C1_L2 line 151