OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/CompactRapidEmbedding.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

An explicit reflected similarity places the compact rapid-forcing construction in a single unit chart. The first-coordinate observation is preserved, and material trajectories are conjugated by the same map.

  1. def OAI.RapidForcing.CompactEmbedding.reflection line 14
  2. theorem OAI.RapidForcing.CompactEmbedding.reflection_apply line 18
  3. theorem OAI.RapidForcing.CompactEmbedding.reflection_reflection line 22
  4. def OAI.RapidForcing.CompactEmbedding.linear line 26
  5. def OAI.RapidForcing.CompactEmbedding.inverseLinear line 29
  6. def OAI.RapidForcing.CompactEmbedding.coordinateSign line 32
  7. theorem OAI.RapidForcing.CompactEmbedding.linear_apply line 34
  8. theorem OAI.RapidForcing.CompactEmbedding.inverseLinear_basis line 38
  9. theorem OAI.RapidForcing.CompactEmbedding.inverseLinear_linear line 47
  10. theorem OAI.RapidForcing.CompactEmbedding.linear_inverseLinear line 50
  11. theorem OAI.RapidForcing.CompactEmbedding.norm_linear line 53
  12. theorem OAI.RapidForcing.CompactEmbedding.norm_inverseLinear line 56
  13. def OAI.RapidForcing.CompactEmbedding.center line 59
  14. def OAI.RapidForcing.CompactEmbedding.embed line 61
  15. def OAI.RapidForcing.CompactEmbedding.unembed line 63
  16. theorem OAI.RapidForcing.CompactEmbedding.unembed_embed line 65
  17. theorem OAI.RapidForcing.CompactEmbedding.embed_unembed line 68
  18. theorem OAI.RapidForcing.CompactEmbedding.embed_zero line 71
  19. theorem OAI.RapidForcing.CompactEmbedding.unembed_center line 73
  20. theorem OAI.RapidForcing.CompactEmbedding.embed_injective line 75
  21. theorem OAI.RapidForcing.CompactEmbedding.unembed_injective line 78
  22. theorem OAI.RapidForcing.CompactEmbedding.embed_first line 81
  23. theorem OAI.RapidForcing.CompactEmbedding.embed_second line 84
  24. theorem OAI.RapidForcing.CompactEmbedding.embed_third line 87
  25. theorem OAI.RapidForcing.CompactEmbedding.embed_observation line 90
  26. def OAI.RapidForcing.CompactEmbedding.chart line 94
  27. theorem OAI.RapidForcing.CompactEmbedding.embed_mem_chart line 96
  28. theorem OAI.RapidForcing.CompactEmbedding.chart_inside_unit line 103
  29. def OAI.RapidForcing.CompactEmbedding.compactChart line 110
  30. theorem OAI.RapidForcing.CompactEmbedding.compactChart_compact line 112
  31. theorem OAI.RapidForcing.CompactEmbedding.compactChart_subset_chart line 115
  32. theorem OAI.RapidForcing.CompactEmbedding.embed_hasFDerivAt line 119
  33. theorem OAI.RapidForcing.CompactEmbedding.unembed_hasFDerivAt line 122
  34. theorem OAI.RapidForcing.CompactEmbedding.embed_contDiff line 129
  35. theorem OAI.RapidForcing.CompactEmbedding.unembed_contDiff line 132
  36. def OAI.RapidForcing.CompactEmbedding.field line 135
  37. theorem OAI.RapidForcing.CompactEmbedding.field_embed line 138
  38. theorem OAI.RapidForcing.CompactEmbedding.field_zero line 141
  39. theorem OAI.RapidForcing.CompactEmbedding.field_supported line 144
  40. theorem OAI.RapidForcing.CompactEmbedding.field_smooth line 153
  41. theorem OAI.RapidForcing.CompactEmbedding.embed_curve_hasDerivWithinAt line 158
  42. theorem OAI.RapidForcing.CompactEmbedding.unembed_curve_hasDerivWithinAt line 163
  43. def OAI.RapidForcing.CompactEmbedding.flow line 169
  44. theorem OAI.RapidForcing.CompactEmbedding.flow_embed line 172
  45. theorem OAI.RapidForcing.CompactEmbedding.trajectory_unembed line 175
  46. theorem OAI.RapidForcing.CompactEmbedding.materialFlow line 183
  47. theorem OAI.RapidForcing.CompactEmbedding.flow_observation line 197
  48. theorem OAI.RapidForcing.CompactEmbedding.reaches_iff line 201