OAI/MathematicalPhysics/BFSS/
1264 declarations, 0 contain sorry, 0 declared as axioms; 74 files
Files
- CliffordSymbols.lean 31 declarations
- ClosedProfiles.lean 33 declarations
- ColorLie.lean 23 declarations
- ColorMatrices.lean 24 declarations
- Core.lean 54 declarations
- CoreCompactness.lean 24 declarations
- CovariantFields.lean 30 declarations
- Cutoffs.lean 9 declarations
- DeformedCharge.lean 14 declarations
- DistanceBounds.lean 12 declarations
- EnergyExtraction.lean 10 declarations
- EnergyLimits.lean 15 declarations
- FermionFrequency.lean 24 declarations
- FermionModes.lean 8 declarations
- FermionQuantization.lean 19 declarations
- FiniteFamilies.lean 16 declarations
- FormClosure.lean 24 declarations
- FormCompactness.lean 9 declarations
- FrequencyComparison.lean 8 declarations
- FrequencyContraction.lean 11 declarations
- FrequencyOperators.lean 6 declarations
- FrequencySpectrum.lean 6 declarations
- GammaIdentity.lean 19 declarations
- GammaWords.lean 40 declarations
- GaugeAverages.lean 12 declarations
- GaugeCore.lean 16 declarations
- GaugeGeometry.lean 22 declarations
- GaugeOrbits.lean 32 declarations
- GroundEnergy.lean 9 declarations
- GroundLine.lean 6 declarations
- Kinetic.lean 39 declarations
- KineticMeasures.lean 17 declarations
- LocalBounds.lean 2 declarations
- LocalL2.lean 13 declarations
- LowerContinuity.lean 5 declarations
- Main.lean 73 imports, no declarations
- MassIdentity.lean 49 declarations
- MassiveCoercivity.lean 32 declarations
- MassiveMoments.lean 6 declarations
- MeasuredFields.lean 8 declarations
- MixedEnergy.lean 32 declarations
- NormExhaustion.lean 4 declarations
- NormalCharts.lean 38 declarations
- NormalCocycle.lean 3 declarations
- NormalFields.lean 20 declarations
- NormalGap.lean 10 declarations
- NormalLinearization.lean 25 declarations
- NormalPotential.lean 19 declarations
- NormalTubes.lean 13 declarations
- OrbitCutoffs.lean 12 declarations
- OrbitDensity.lean 17 declarations
- OscillatorForms.lean 16 declarations
- OscillatorLimits.lean 14 declarations
- PotentialBasis.lean 38 declarations
- PotentialBounds.lean 15 declarations
- PotentialLimits.lean 11 declarations
- PotentialSquares.lean 9 declarations
- ProfileEnergy.lean 14 declarations
- ProfileExtraction.lean 14 declarations
- ProfileMoments.lean 8 declarations
- RellichCompactness.lean 10 declarations
- RellichSmoothing.lean 27 declarations
- SharpCutoffs.lean 8 declarations
- SliceDensity.lean 10 declarations
- SliceIntegrals.lean 19 declarations
- SmallPatches.lean 9 declarations
- SobolevGraphs.lean 25 declarations
- SpinCoupling.lean 17 declarations
- StabilizerProfiles.lean 14 declarations
- TaylorBounds.lean 17 declarations
- Vacuum.lean 4 declarations
- WeakLimits.lean 4 declarations
- WeightedCompactness.lean 16 declarations
- WeightedGradients.lean 15 declarations