OAI/Analysis/NavierStokes/VelocitySpace.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Solenoidal equivariant velocity spaces and preliminary discretely self-similar Navier-Stokes estimates.

  1. instance OAI.DSS.(instance at line 14) line 14
  2. abbrev OAI.DSS.R3 line 16
  3. abbrev OAI.DSS.V3 line 17
  4. abbrev OAI.DSS.Velocity line 18
  5. def OAI.DSS.basisVector line 20
  6. def OAI.DSS.gradient line 22
  7. theorem OAI.DSS.continuous_gradient line 25
  8. theorem OAI.DSS.compactSupport_gradient line 30
  9. structure OAI.DSS.ScalarTest line 35
  10. def OAI.DSS.ScalarTest.gradientLp line 40
  11. abbrev OAI.DSS.HorizontalOrthogonal line 45
  12. def OAI.DSS.horizontalValueMap line 47
  13. theorem OAI.DSS.horizontalValueMap_real line 52
  14. abbrev OAI.DSS.VelocityPair line 65
  15. def OAI.DSS.velocitySubmodule line 68
  16. abbrev OAI.DSS.X line 102
  17. def OAI.DSS.X.field line 104
  18. theorem OAI.DSS.X.norm_eq line 106
  19. theorem OAI.DSS.X.memLp line 110
  20. theorem OAI.DSS.X.solenoidal line 117
  21. theorem OAI.DSS.X.equivariant line 130
  22. theorem OAI.DSS.X.equivariant_real line 139
  23. theorem OAI.DSS.velocitySubmodule_isClosed line 143
  24. instance OAI.DSS.X.completeSpace line 173
  25. def OAI.DSS.complexifyVector line 178
  26. def OAI.DSS.ComplexDecomposition line 181
  27. def OAI.DSS.IsComplexification line 185
  28. def OAI.DSS.divergence line 189
  29. def OAI.DSS.laplacian line 192
  30. def OAI.DSS.SmoothUnforcedNS line 195
  31. def OAI.DSS.AxisymmetricSwirlFree line 204
  32. def OAI.DSS.DiscretelySelfSimilar line 208
  33. def OAI.DSS.period line 212
  34. def OAI.DSS.rescaled line 214
  35. def OAI.DSS.DecayBound line 217
  36. def OAI.DSS.DistributionalInitialTrace line 221
  37. def OAI.DSS.TraceProperties line 227
  38. structure OAI.DSS.SolenoidalTest line 234
  39. def OAI.DSS.rescaledWeakSpatial line 240
  40. def OAI.DSS.WeakLinearizedSolution line 248
  41. abbrev OAI.DSS.Evolution line 260
  42. def OAI.DSS.ForwardEvolution line 262
  43. structure OAI.DSS.SpectralSplitting line 271
  44. def OAI.DSS.FiniteAlgebraicEigenvalue line 285
  45. def OAI.DSS.IsolatedSpectralValue line 290
  46. structure OAI.DSS.RealSpectralSplitting line 294
  47. def OAI.DSS.SpectralConclusions line 305
  48. def OAI.DSS.UnstableDSSFlow line 319
  49. theorem OAI.DSS.period_pos line 326
  50. theorem OAI.DSS.exp_period line 329
  51. theorem OAI.DSS.essential_radius_eq_inv line 332
  52. theorem OAI.DSS.essential_radius_lt_one line 337
  53. theorem OAI.DSS.rescaled_at_log line 343
  54. theorem OAI.DSS.rescaled_periodic line 347
  55. theorem OAI.DSS.rescaled_decay line 363
  56. theorem OAI.DSS.spectralRadius_ge_of_fixed_orbit_growth line 382