OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CylinderMeasure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VelocityDetection.Cylinder.probability_vertical line 15
  2. theorem OAI.VelocityDetection.Cylinder.measurePreserving_horizontal line 19
  3. def OAI.VelocityDetection.Cylinder.liftL2 line 24
  4. theorem OAI.VelocityDetection.Cylinder.coeFn_liftL2 line 27
  5. theorem OAI.VelocityDetection.Cylinder.norm_liftL2 line 31
  6. theorem OAI.VelocityDetection.Cylinder.liftL2_rep line 34
  7. theorem OAI.VelocityDetection.Cylinder.memLp_lift line 39
  8. def OAI.VelocityDetection.Cylinder.tailsToL2 line 43
  9. theorem OAI.VelocityDetection.Cylinder.coeFn_tailsToL2 line 46