OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarBranchBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Effective rational bounds for dependence of one entire branch on its source point. The same bound covers all eight anchors and all partial pulses.

  1. def OAI.ForcedComputation.Recorder.Planar.branchExpansion line 15
  2. def OAI.ForcedComputation.Recorder.Planar.branchGrowth line 19
  3. def OAI.ForcedComputation.Recorder.Planar.branchRadius line 22
  4. theorem OAI.ForcedComputation.Recorder.Planar.primitive_growth_le_expansion line 25
  5. theorem OAI.ForcedComputation.Recorder.Planar.branchExpansion_one_le line 35
  6. theorem OAI.ForcedComputation.Recorder.Planar.branchGrowth_one_le line 39
  7. theorem OAI.ForcedComputation.Recorder.Planar.branchRadius_pos line 43
  8. theorem OAI.ForcedComputation.Recorder.Planar.branchAnchor_sub_bound line 48
  9. theorem OAI.ForcedComputation.Recorder.Planar.branchAnchor_sub_uniform line 76
  10. theorem OAI.ForcedComputation.Recorder.Planar.branchPath_sub_uniform line 87
  11. theorem OAI.ForcedComputation.Recorder.Planar.growth_mul_radius line 113
  12. theorem OAI.ForcedComputation.Recorder.Planar.branchAnchor_dist_lt_collar line 122
  13. theorem OAI.ForcedComputation.Recorder.Planar.branchPath_dist_lt_collar line 135
  14. def OAI.ForcedComputation.Recorder.Planar.branchNeighborhood line 151
  15. theorem OAI.ForcedComputation.Recorder.Planar.source_subset_branchNeighborhood line 155