OAI/MathematicalPhysics/BFSS/OrbitCutoffs.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Disjoint orbit chambers and smooth cutoff norm exhaustion.

  1. lemma OAI.BFSSQuantum.AlgebraData.gauge_neighborhood_plateau line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.gaugeOrbit_image line 62
  3. lemma OAI.BFSSQuantum.AlgebraData.gaugeOrbit_infDist line 71
  4. lemma OAI.BFSSQuantum.AlgebraData.gaugeOrbit_eq_of_mem line 77
  5. lemma OAI.BFSSQuantum.AlgebraData.gaugeOrbit_disjoint_of_ne line 94
  6. theorem OAI.BFSSQuantum.AlgebraData.massiveZeros_disjoint_orbits line 100
  7. def OAI.BFSSQuantum.AlgebraData.orbitChamber line 119
  8. lemma OAI.BFSSQuantum.AlgebraData.orbitChamber_open line 122
  9. lemma OAI.BFSSQuantum.AlgebraData.orbitChamber_gauge line 133
  10. lemma OAI.BFSSQuantum.AlgebraData.orbitChamber_contains line 138
  11. lemma OAI.BFSSQuantum.AlgebraData.orbitChamber_disjoint line 147
  12. theorem OAI.BFSSQuantum.AlgebraData.massive_core_cutoff_exhaustion line 161