OAI/MathematicalPhysics/NavierStokes/VelocityDetection/WeakVolterra.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.WeakVolterra.Curve line 18
  2. def OAI.VelocityDetection.WeakVolterra.extend line 20
  3. theorem OAI.VelocityDetection.WeakVolterra.continuous_extend line 22
  4. theorem OAI.VelocityDetection.WeakVolterra.extend_of_mem line 26
  5. theorem OAI.VelocityDetection.WeakVolterra.norm_extend_le line 30
  6. def OAI.VelocityDetection.WeakVolterra.raw line 51
  7. theorem OAI.VelocityDetection.WeakVolterra.integrable_raw line 77
  8. theorem OAI.VelocityDetection.WeakVolterra.continuous_raw line 94
  9. theorem OAI.VelocityDetection.WeakVolterra.norm_raw_le line 130
  10. def OAI.VelocityDetection.WeakVolterra.operator line 146
  11. theorem OAI.VelocityDetection.WeakVolterra.operator_apply line 170
  12. theorem OAI.VelocityDetection.WeakVolterra.norm_operator_apply_le line 173
  13. theorem OAI.VelocityDetection.WeakVolterra.raw_eq_integral line 197
  14. theorem OAI.VelocityDetection.WeakVolterra.raw_zero line 202
  15. def OAI.VelocityDetection.WeakVolterra.weight line 206
  16. theorem OAI.VelocityDetection.WeakVolterra.weight_apply line 210
  17. theorem OAI.VelocityDetection.WeakVolterra.weight_add line 213
  18. theorem OAI.VelocityDetection.WeakVolterra.weight_weight line 218
  19. theorem OAI.VelocityDetection.WeakVolterra.weight_zero line 225
  20. theorem OAI.VelocityDetection.WeakVolterra.weight_neg_weight line 229
  21. def OAI.VelocityDetection.WeakVolterra.dampKernel line 232
  22. def OAI.VelocityDetection.WeakVolterra.dampBound line 234
  23. theorem OAI.VelocityDetection.WeakVolterra.raw_weight line 236
  24. theorem OAI.VelocityDetection.WeakVolterra.existsUnique_of_small line 269
  25. theorem OAI.VelocityDetection.WeakVolterra.continuousOn_dampKernel line 288
  26. theorem OAI.VelocityDetection.WeakVolterra.integrableOn_dampBound line 295
  27. theorem OAI.VelocityDetection.WeakVolterra.dampBound_nonneg line 307
  28. theorem OAI.VelocityDetection.WeakVolterra.norm_dampKernel_le line 313
  29. theorem OAI.VelocityDetection.WeakVolterra.tendsto_integral_dampBound line 321
  30. theorem OAI.VelocityDetection.WeakVolterra.existsUnique line 359
  31. theorem OAI.VelocityDetection.WeakVolterra.existsUnique_pointwise line 393