OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TailSpaceToC0.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.VelocityDetection.TailSpace.toC0 line 14
2. def OAI.VelocityDetection.TailSpace.toL1 line 17
3. theorem OAI.VelocityDetection.TailSpace.toC0_apply line 20
4. theorem OAI.VelocityDetection.TailSpace.toL1_apply line 22
5. theorem OAI.VelocityDetection.TailSpace.ContinuousTails.C0_rep line 24
6. theorem OAI.VelocityDetection.TailSpace.C1Tails.L1_rep line 29