OAI/Geometry/WeakHessian/Entropy/EntropyCell.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.integrable_plan_energy_of_length line 58
  2. lemma OAI.WeakHessian.optimal_planEnergy_eq line 66
  3. lemma OAI.WeakHessian.dominated_mono_constant line 77
  4. structure OAI.WeakHessian.EntropyCell line 82
  5. structure OAI.WeakHessian.CellPlan line 99
  6. structure OAI.WeakHessian.CDEnvironment line 104
  7. def OAI.WeakHessian.EntropyCell.nextCap line 113
  8. def OAI.WeakHessian.EntropyCell.uniformCap line 116
  9. lemma OAI.WeakHessian.EntropyCell.nextCap_pos line 120
  10. lemma OAI.WeakHessian.EntropyCell.nextCap_finite line 123
  11. lemma OAI.WeakHessian.EntropyCell.uniformCap_pos line 126
  12. lemma OAI.WeakHessian.EntropyCell.uniformCap_finite line 129
  13. lemma OAI.WeakHessian.EntropyCell.cap_le_nextCap line 132
  14. lemma OAI.WeakHessian.EntropyCell.cap_le_uniformCap line 137
  15. lemma OAI.WeakHessian.CellPlan.integrable_energy line 146
  16. lemma OAI.WeakHessian.CellPlan.energy_eq line 149
  17. structure OAI.WeakHessian.CellMidpoint line 154
  18. lemma OAI.WeakHessian.CDEnvironment.midpoint_nonempty line 163
  19. def OAI.WeakHessian.CDEnvironment.midpoint line 173
  20. def OAI.WeakHessian.CellMidpoint.middle line 180
  21. lemma OAI.WeakHessian.CellMidpoint.middle_supported line 184
  22. lemma OAI.WeakHessian.CellMidpoint.short_halves line 190
  23. def OAI.WeakHessian.CellMidpoint.leftCell line 195
  24. def OAI.WeakHessian.CellMidpoint.rightCell line 213
  25. lemma OAI.WeakHessian.CellMidpoint.left_uniformCap line 231
  26. lemma OAI.WeakHessian.CellMidpoint.right_uniformCap line 240