OAI/MathematicalPhysics/BFSS/SmallPatches.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Small slice patches, localized measures and norm moments.

  1. theorem OAI.BFSSQuantum.AlgebraData.normalPatch_exists_small line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.sliceLinearEquiv_normal_norm_le line 89
  3. lemma OAI.BFSSQuantum.AlgebraData.normalSliceDensity_eq_zero line 99
  4. theorem OAI.BFSSQuantum.AlgebraData.normalSlice_measure_small line 109
  5. theorem OAI.BFSSQuantum.AlgebraData.normalOrbit_measure_small line 141
  6. lemma OAI.BFSSQuantum.AlgebraData.massiveDistance_gauge line 198
  7. theorem OAI.BFSSQuantum.AlgebraData.normalOrbit_norm_moment line 205
  8. lemma OAI.BFSSNormalMeasure.square_compact line 257
  9. lemma OAI.BFSSNormalMeasure.square_integrable line 264