OAI/Geometry/CylinderCovering/Physical/Finite.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RadialPhysical.PhysicalFiniteProof.vec line 14
  2. def OAI.RadialPhysical.PhysicalFiniteProof.upperW line 16
  3. def OAI.RadialPhysical.PhysicalFiniteProof.lowerW line 20
  4. lemma OAI.RadialPhysical.PhysicalFiniteProof.upperW_deriv line 24
  5. lemma OAI.RadialPhysical.PhysicalFiniteProof.lowerW_deriv line 35
  6. lemma OAI.RadialPhysical.PhysicalFiniteProof.height_pos line 46
  7. lemma OAI.RadialPhysical.PhysicalFiniteProof.axialBound_pos line 49
  8. def OAI.RadialPhysical.PhysicalFiniteProof.upperData line 53
  9. def OAI.RadialPhysical.PhysicalFiniteProof.lowerData line 83
  10. lemma OAI.RadialPhysical.PhysicalFiniteProof.upperData_point line 117
  11. lemma OAI.RadialPhysical.PhysicalFiniteProof.lowerData_point line 128
  12. lemma OAI.RadialPhysical.PhysicalFiniteProof.upperData_sweep line 139
  13. lemma OAI.RadialPhysical.PhysicalFiniteProof.lowerData_sweep line 145
  14. lemma OAI.RadialPhysical.PhysicalFiniteProof.upperData_localSweep line 151
  15. lemma OAI.RadialPhysical.PhysicalFiniteProof.lowerData_localSweep line 158
  16. lemma OAI.RadialPhysical.PhysicalFiniteProof.upperData_direction line 165
  17. lemma OAI.RadialPhysical.PhysicalFiniteProof.lowerData_direction line 175
  18. lemma OAI.RadialPhysical.PhysicalFiniteProof.upperData_actualBase line 185
  19. lemma OAI.RadialPhysical.PhysicalFiniteProof.lowerData_actualBase line 191
  20. lemma OAI.RadialPhysical.PhysicalFiniteProof.upperData_kappa line 197
  21. lemma OAI.RadialPhysical.PhysicalFiniteProof.lowerData_kappa line 207
  22. lemma OAI.RadialPhysical.PhysicalFiniteProof.upperW_norm_sq line 217
  23. lemma OAI.RadialPhysical.PhysicalFiniteProof.lowerW_norm_sq line 225
  24. lemma OAI.RadialPhysical.PhysicalFiniteProof.upperData_weightedArea line 233
  25. lemma OAI.RadialPhysical.PhysicalFiniteProof.lowerData_weightedArea line 254
  26. lemma OAI.RadialPhysical.PhysicalFiniteProof.physicalActualCost_eq line 275
  27. theorem OAI.RadialPhysical.physical_finite line 287