OAI/Probability/LatticeSurface/Dynamics/ClusterAlgebra.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClusterDisplacement.energy line 13
  2. lemma OAI.ClusterDisplacement.weighted_sq_le line 15
  3. structure OAI.ClusterDisplacement.Kernel line 31
  4. def OAI.ClusterDisplacement.Kernel.apply line 37
  5. lemma OAI.ClusterDisplacement.Kernel.apply_nonneg line 39
  6. lemma OAI.ClusterDisplacement.Kernel.square_bound line 42
  7. lemma OAI.ClusterDisplacement.Kernel.energy_bound line 45
  8. def OAI.ClusterDisplacement.Kernel.identity line 51
  9. lemma OAI.ClusterDisplacement.Kernel.identity_apply line 58
  10. def OAI.ClusterDisplacement.Kernel.comp line 63
  11. lemma OAI.ClusterDisplacement.Kernel.comp_apply line 77
  12. lemma OAI.ClusterDisplacement.Kernel.row_deficit_nonneg line 87
  13. lemma OAI.ClusterDisplacement.Kernel.row_deficit_le line 90
  14. lemma OAI.ClusterDisplacement.Kernel.near_initial_level line 98