OAI/Analysis/IncompressibleFlow/AffineExtension.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

Solid-box geometry and compactly supported solenoidal extensions of diagonal affine fields.

  1. abbrev OAI.BoxTransport.Space line 12
  2. abbrev OAI.BoxTransport.Spacetime line 13
  3. abbrev OAI.BoxTransport.RationalPoint line 14
  4. abbrev OAI.BoxTransport.Velocity line 15
  5. def OAI.BoxTransport.solidBox line 17
  6. def OAI.BoxTransport.ofRat line 20
  7. def OAI.BoxTransport.rationalBox line 22
  8. def OAI.BoxTransport.assignedMap line 25
  9. def OAI.BoxTransport.inCoordinates line 28
  10. def OAI.BoxTransport.mixedPartial line 31
  11. abbrev OAI.BoxTransport.RationalCode line 35
  12. abbrev OAI.BoxTransport.PointCode line 36
  13. abbrev OAI.BoxTransport.DerivativeQuery line 37
  14. def OAI.BoxTransport.decodeRational line 39
  15. def OAI.BoxTransport.decodePoint line 42
  16. def OAI.BoxTransport.dyadicError line 46
  17. def OAI.BoxTransport.EffectiveField line 48
  18. def OAI.BoxTransport.divergence line 59
  19. def OAI.BoxTransport.Solenoidal line 62
  20. def OAI.BoxTransport.IsMaterialFlow line 64
  21. def OAI.BoxTransport.RoutingConclusion line 68
  22. theorem OAI.BoxTransport.mem_solidBox line 79
  23. theorem OAI.BoxTransport.center_mem_solidBox line 82
  24. theorem OAI.BoxTransport.solidBox_eq_pi line 86
  25. theorem OAI.BoxTransport.isCompact_solidBox line 95
  26. theorem OAI.BoxTransport.disjoint_solidBox_of_gap line 99
  27. theorem OAI.BoxTransport.disjoint_solidBox_iff line 109
  28. theorem OAI.BoxTransport.centers_ne_of_disjoint line 133
  29. theorem OAI.BoxTransport.gap_le_expanded_gap line 141
  30. theorem OAI.BoxTransport.disjoint_solidBox_expand line 147
  31. theorem OAI.BoxTransport.disjoint_padded_solidBox line 156
  32. def OAI.BoxTransport.diagonalAffine line 163
  33. theorem OAI.BoxTransport.diagonalAffine_mem_iff line 166
  34. theorem OAI.BoxTransport.diagonalAffine_inverse line 172
  35. theorem OAI.BoxTransport.diagonalAffine_image line 179
  36. theorem OAI.BoxTransport.assignedMap_image line 195
  37. theorem OAI.BoxTransport.rationalBox_separating_coordinate line 211
  38. theorem OAI.BoxTransport.finite_positive_lower_bound line 223
  39. theorem OAI.BoxTransport.exists_uniform_rational_gap line 237
  40. theorem OAI.BoxTransport.exists_common_center_expansion line 257
  41. theorem OAI.BoxTransport.rational_centers_injective line 291
  42. theorem OAI.BoxTransport.disjoint_padded_of_center_clearance line 302
  43. def OAI.BoxTransport.shapeScale line 311
  44. theorem OAI.BoxTransport.shapeScale_zero line 314
  45. theorem OAI.BoxTransport.shapeScale_one line 318
  46. theorem OAI.BoxTransport.shapeScale_pos line 322
  47. theorem OAI.BoxTransport.sum_log_eq_zero line 325
  48. theorem OAI.BoxTransport.shapeScale_balanced line 329
  49. theorem OAI.BoxTransport.shapeScale_det_eq_one line 334
  50. theorem OAI.BoxTransport.geometric_width_eq line 340
  51. theorem OAI.BoxTransport.geometric_width_le_max line 353
  52. theorem OAI.BoxTransport.shapeScale_width_bound line 366
  53. theorem OAI.BoxTransport.real_balance_of_rational line 373
  54. theorem OAI.BoxTransport.mixedPartial_zero line 377
  55. theorem OAI.BoxTransport.effective_zero line 385
  56. theorem OAI.BoxTransport.solenoidal_zero line 399
  57. theorem OAI.BoxTransport.identity_isMaterialFlow line 403
  58. theorem OAI.BoxTransport.routingConclusion_empty line 408
  59. theorem OAI.BoxTransport.assignedMap_self line 418
  60. theorem OAI.BoxTransport.routingConclusion_reflexive line 423
  61. def OAI.BoxTransport.direction line 434
  62. def OAI.BoxTransport.jacobianEntry line 436
  63. def OAI.BoxTransport.curlFromJacobian line 439
  64. def OAI.BoxTransport.curl line 444
  65. theorem OAI.BoxTransport.curl_apply line 447
  66. theorem OAI.BoxTransport.contDiff_curl line 454
  67. theorem OAI.BoxTransport.hasCompactSupport_curl line 458
  68. theorem OAI.BoxTransport.divergence_curl line 462
  69. theorem OAI.BoxTransport.curl_eq_of_eventuallyEq line 482
  70. theorem OAI.BoxTransport.curl_cutoff_eq line 486
  71. def OAI.BoxTransport.potentialComponent line 493
  72. def OAI.BoxTransport.affinePotential line 497
  73. theorem OAI.BoxTransport.affinePotential_eq_cross line 501
  74. theorem OAI.BoxTransport.contDiff_potentialComponent line 507
  75. theorem OAI.BoxTransport.contDiff_affinePotential line 512
  76. theorem OAI.BoxTransport.potentialComponent_fderiv line 520
  77. theorem OAI.BoxTransport.curl_affinePotential line 535
  78. theorem OAI.BoxTransport.curl_affinePotential_trace_zero line 553
  79. theorem OAI.BoxTransport.localized_affine_extension line 557
  80. def OAI.BoxTransport.openBox line 575
  81. theorem OAI.BoxTransport.isOpen_openBox line 577
  82. theorem OAI.BoxTransport.solidBox_subset_openBox_padded line 583
  83. theorem OAI.BoxTransport.exists_padded_box_cutoff line 588
  84. theorem OAI.BoxTransport.tsupport_curl_subset line 615
  85. theorem OAI.BoxTransport.affine_extension_on_box line 619
  86. theorem OAI.BoxTransport.contDiff_shapeScale line 645
  87. theorem OAI.BoxTransport.hasDerivAt_shapeScale line 649
  88. theorem OAI.BoxTransport.sum_logarithmic_rate line 660
  89. def OAI.BoxTransport.shapeMotion line 664
  90. theorem OAI.BoxTransport.shapeMotion_hasDerivAt line 668
  91. theorem OAI.BoxTransport.shapeMotion_start line 679
  92. theorem OAI.BoxTransport.shapeMotion_finish line 684
  93. theorem OAI.BoxTransport.diagonalAffine_perturbation_bound line 690
  94. theorem OAI.BoxTransport.diagonalAffine_openBox_padded line 701