OAI/MathematicalPhysics/BFSS/FrequencyComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact field-frequency identification and quantitative frequency lower bounds.

  1. lemma OAI.BFSSQuantum.AlgebraData.colorEuclidean_matrix_entry line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.colorJ_matrix_entry line 21
  3. lemma OAI.BFSSQuantum.AlgebraData.normal_frequency_tensor_entry line 41
  4. lemma OAI.BFSSQuantum.AlgebraData.zero_relations_coordinate_tail line 54
  5. theorem OAI.BFSSQuantum.AlgebraData.fermionCoefficient_eq_normalFrequency line 59
  6. lemma OAI.BFSSQuantum.AlgebraData.normalFermionFrequency_skew line 108
  7. theorem OAI.BFSSQuantum.AlgebraData.normalFermionFrequency_norm_lower line 130
  8. theorem OAI.BFSSQuantum.AlgebraData.normal_fermion_field_exact line 166