OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TailConvolution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.VelocityDetection.TailSpace.Jets.averageL line 15
2. theorem OAI.VelocityDetection.TailSpace.Jets.averageL_apply line 33
3. def OAI.VelocityDetection.TailSpace.Jets.convolve line 36
4. theorem OAI.VelocityDetection.TailSpace.Jets.value_convolve line 39
5. theorem OAI.VelocityDetection.TailSpace.Jets.norm_convolve_le line 44
6. theorem OAI.VelocityDetection.TailSpace.Jets.continuous_average line 48
7. theorem OAI.VelocityDetection.TailSpace.Jets.average_zero_scale line 63
8. theorem OAI.VelocityDetection.TailSpace.Jets.average_tendsto_identity line 67
9. theorem OAI.VelocityDetection.TailSpace.Jets.norm_average_le_of_probability_kernel line 73