OAI/Probability/LatticeSurface/Moments/CoercivityEnergy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SparseHoles.squareEdges line 33
  2. def OAI.SparseHoles.buffer line 37
  3. def OAI.SparseHoles.goodEnergy line 39
  4. lemma OAI.SparseHoles.horizontal_injective line 45
  5. lemma OAI.SparseHoles.vertical_injective line 54
  6. lemma OAI.SparseHoles.squareEdges_good line 63
  7. lemma OAI.SparseHoles.squareEdges_endpoints line 67
  8. lemma OAI.SparseHoles.square_horizontal line 71
  9. lemma OAI.SparseHoles.square_vertical line 86
  10. lemma OAI.SparseHoles.energy_le_square line 101
  11. lemma OAI.SparseHoles.grid_energy_nonneg line 125
  12. lemma OAI.SparseHoles.goodEnergy_nonneg line 130