OAI/Analysis/CoulombRadii/FieldAnalysis/PermuteJoinBlock.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.permute_join_block line 63
  2. lemma OAI.Coulomb.spins_block_left line 78
  3. lemma OAI.Coulomb.spins_block_right line 83
  4. lemma OAI.Coulomb.tensor_block_covariance line 89
  5. lemma OAI.Coulomb.position_join_left line 123
  6. lemma OAI.Coulomb.position_join_right line 127
  7. lemma OAI.Coulomb.position_split_left line 132
  8. lemma OAI.Coulomb.position_split_right line 136
  9. def OAI.Coulomb.blockRegion line 141
  10. lemma OAI.Coulomb.blockRegion_split line 145
  11. lemma OAI.Coulomb.isClosed_blockRegion line 152
  12. lemma OAI.Coulomb.tensor_configSupported line 163
  13. lemma OAI.Coulomb.blockRegion_orbit_disjoint line 188
  14. lemma OAI.Coulomb.configSupported_value_orthogonal line 203
  15. lemma OAI.Coulomb.configSupported_gradient_orthogonal line 215