OAI/Analysis/Conductivity/Geometry/BoxEnergyPoincare.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.cubeEnergyDensity line 13
  2. lemma OAI.ScalarConductivity.continuous_cubeEnergyDensity line 17
  3. lemma OAI.ScalarConductivity.cubeEnergyDensity_nonneg line 22
  4. theorem OAI.ScalarConductivity.smooth_box_volume_poincare line 25
  5. structure OAI.ScalarConductivity.RectFootprint line 65
  6. def OAI.ScalarConductivity.RectFootprint.carrier line 71
  7. def OAI.ScalarConductivity.RectFootprint.inter line 74
  8. lemma OAI.ScalarConductivity.RectFootprint.inter_carrier line 77
  9. def OAI.ScalarConductivity.RectFootprint.prism line 84
  10. lemma OAI.ScalarConductivity.RectFootprint.prism_closedBox line 87
  11. lemma OAI.ScalarConductivity.RectFootprint.prism_compact line 91
  12. def OAI.ScalarConductivity.centralThickness line 94
  13. def OAI.ScalarConductivity.centralOuterX line 95
  14. def OAI.ScalarConductivity.centralInnerX line 96
  15. def OAI.ScalarConductivity.centralOuterY line 97
  16. def OAI.ScalarConductivity.centralInnerY line 98
  17. def OAI.ScalarConductivity.centralHeight line 99
  18. def OAI.ScalarConductivity.centralChildHeight line 100
  19. def OAI.ScalarConductivity.centralChildOuterX line 101
  20. def OAI.ScalarConductivity.centralChildOuterY line 102
  21. def OAI.ScalarConductivity.centralChildInnerX line 103
  22. def OAI.ScalarConductivity.centralChildInnerY line 104
  23. def OAI.ScalarConductivity.centralParentStrip line 106
  24. def OAI.ScalarConductivity.centralChildOption line 112
  25. def OAI.ScalarConductivity.centralParentFootprint line 120
  26. def OAI.ScalarConductivity.centralAvoidChild line 124
  27. lemma OAI.ScalarConductivity.centralParentStrip_mem line 128
  28. lemma OAI.ScalarConductivity.centralChildOption_mem line 150
  29. def OAI.ScalarConductivity.centralColumn line 172
  30. lemma OAI.ScalarConductivity.centralColumn_cover line 175
  31. def OAI.ScalarConductivity.centralClosed line 190
  32. def OAI.ScalarConductivity.centralTop line 193
  33. def OAI.ScalarConductivity.centralBottom line 196
  34. theorem OAI.ScalarConductivity.centralClosed_cover line 199