OAI/Geometry/CylinderCovering/Rational/EnergyIntegral.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RationalEnergy.vec2_zero line 13
  2. theorem OAI.RationalEnergy.vec2_one line 14
  3. theorem OAI.RationalEnergy.plane_norm_le_sum line 16
  4. theorem OAI.RationalEnergy.baseDomain_mem_iff line 23
  5. theorem OAI.RationalEnergy.baseDomain_isCompact line 36
  6. theorem OAI.RationalEnergy.energyDensity_continuousOn line 53
  7. theorem OAI.RationalEnergy.energyDensity_integrableOn line 63
  8. def OAI.RationalEnergy.pairPlaneEquiv line 67
  9. theorem OAI.RationalEnergy.pairPlane_measurePreserving line 70
  10. theorem OAI.RationalEnergy.plane_integral_pair line 74
  11. theorem OAI.RationalEnergy.plane_integrable_pair line 78
  12. theorem OAI.RationalEnergy.plane_setIntegral_horizontal line 82
  13. theorem OAI.RationalEnergy.plane_setIntegral_horizontal_interval line 96
  14. theorem OAI.RationalEnergy.energyIntegral_eq_wedgeCost line 116
  15. theorem OAI.RationalEnergy.baseDomain_volume line 149
  16. theorem OAI.RationalEnergy.field_component_bounds line 175
  17. theorem OAI.RationalEnergy.energyDensity_bounds line 203
  18. theorem OAI.SlopeRational.energyIntegral_tendsto line 219