OAI/MathematicalPhysics/BFSS/NormExhaustion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Measured normal patches and complete finite-patch norm exhaustion.

  1. lemma OAI.BFSSNormalMeasure.disjoint_cutoff_sum line 13
  2. structure OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch line 44
  3. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.exists_measuredNormalPatch line 83
  4. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalPatch_norm_exhaustion line 132