OAI/MathematicalPhysics/BFSS/GroundEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Spectral quantization and the exact fermionic zero-point energy.

  1. lemma OAI.BFSSQuantum.AlgebraData.complexFrequency_spectral_entry line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.thetaMode_product line 30
  3. lemma OAI.BFSSQuantum.AlgebraData.sum_move_last line 38
  4. theorem OAI.BFSSQuantum.AlgebraData.quantizeFrequency_diagonal line 47
  5. lemma OAI.BFSSQuantum.AlgebraData.complexFrequency_eigenvalues_sum line 104
  6. lemma OAI.BFSSQuantum.AlgebraData.negative_sum_eq_abs line 122
  7. theorem OAI.BFSSQuantum.AlgebraData.normal_fermion_ground_energy_value line 136
  8. def OAI.BFSSQuantum.AlgebraData.normalFermionZeroPoint line 209
  9. theorem OAI.BFSSQuantum.AlgebraData.normal_fermion_ground_exact line 213