OAI/MathematicalPhysics/BFSS/ClosedProfiles.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Closed charge graphs, continuous profiles and extraction from graph closures.

  1. lemma OAI.BFSSQuantum.AlgebraData.deformedCoreCharge_add line 13
  2. lemma OAI.BFSSQuantum.AlgebraData.deformedCoreCharge_smul line 20
  3. def OAI.BFSSQuantum.AlgebraData.deformedChargeMap line 38
  4. lemma OAI.BFSSQuantum.AlgebraData.coreInner_re_eq_mixed line 43
  5. lemma OAI.BFSSQuantum.AlgebraData.deformedCoreCharge_re_symmetric line 53
  6. theorem OAI.BFSSQuantum.AlgebraData.deformedChargeMap_symmetric line 64
  7. def OAI.BFSSQuantum.AlgebraData.deformedChargeVector line 75
  8. def OAI.BFSSQuantum.AlgebraData.deformedCoreGraph line 78
  9. def OAI.BFSSQuantum.AlgebraData.deformedClosedGraph line 81
  10. lemma OAI.BFSSQuantum.AlgebraData.deformedClosedGraph_pairing line 84
  11. theorem OAI.BFSSQuantum.AlgebraData.deformedClosedGraph_vertical line 99
  12. lemma OAI.BFSSRellich.normSquare_distance_le line 110
  13. def OAI.BFSSQuantum.AlgebraData.GaugeData.coreNormClosure line 125
  14. def OAI.BFSSQuantum.AlgebraData.GaugeData.coreNormEmbedding line 128
  15. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.coreNormEmbedding_dense line 132
  16. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.coreNormEmbedding_norm line 139
  17. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_ae line 145
  18. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_add line 149
  19. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_smul line 158
  20. def OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profileLinear line 168
  21. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_norm_le line 174
  22. def OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.closedProfile line 180
  23. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.closedProfile_core line 184
  24. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.closedProfile_norm_le line 192
  25. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.closedProfile_dist_le line 202
  26. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.closedProfile_core_dist_le line 209
  27. def OAI.BFSSQuantum.AlgebraData.GaugeData.deformedModelGraphMap line 226
  28. def OAI.BFSSQuantum.AlgebraData.GaugeData.deformedModelGraph line 231
  29. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.deformedModelGraph_le_full line 234
  30. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.deformedModelGraph_vertical line 240
  31. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.deformedModelGraph_coreNormClosure line 244
  32. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.deformedModelGraph_approx line 254
  33. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalClosed_extraction line 275