OAI/Analysis/LaughlinGap/
5137 declarations, 0 contain sorry, 0 declared as axioms; 104 files
Files
- AuxiliaryComparison.lean 17 declarations
- Averaging.lean 28 declarations
- Basic.lean 143 declarations
- CachedIntegerRows.lean 2 declarations
- Certificate10.lean 70 declarations
- Certificate11.lean 77 declarations
- Certificate12.lean 78 declarations
- Certificate13.lean 85 declarations
- Certificate14.lean 86 declarations
- Certificate15.lean 93 declarations
- Certificate16.lean 94 declarations
- Certificate17.lean 101 declarations
- Certificate18.lean 102 declarations
- Certificate19.lean 109 declarations
- Certificate20.lean 110 declarations
- Certificate21.lean 117 declarations
- Certificate22.lean 118 declarations
- Certificate23.lean 125 declarations
- Certificate5.lean 40 declarations
- Certificate6.lean 22 declarations
- Certificate7.lean 61 declarations
- Certificate8.lean 62 declarations
- Certificate9.lean 69 declarations
- CheckedTables.lean 4 declarations
- Contraction.lean 58 declarations
- CovariantFamily.lean 10 declarations
- CovariantLift.lean 13 declarations
- Creation.lean 46 declarations
- ExactRows.lean 25 declarations
- ExtendedPair.lean 12 declarations
- ExteriorTermExpansion.lean 4 declarations
- FastCoupling.lean 12 declarations
- FastFourKeys.lean 9 declarations
- Four.lean 8 declarations
- FourAllowance.lean 11 declarations
- FourAveraging.lean 7 declarations
- FourBound.lean 4 declarations
- FourBoundCore.lean 8 declarations
- FourComparison.lean 15 declarations
- FourHighest.lean 4 declarations
- FourSpin.lean 19 declarations
- FourTables.lean 3 declarations
- FourTransfer.lean 21 declarations
- GlobalBound.lean 3 declarations
- GlobalBoundCore.lean 9 declarations
- HighestRatios.lean 7 declarations
- IntegerFourRows.lean 12 declarations
- IntertwinerAveraging.lean 13 declarations
- IntertwiningSpin.lean 19 declarations
- IrrepAveraging.lean 7 declarations
- LowNested.lean 6 declarations
- Main.lean 2 declarations
- NestedAveraging.lean 14 declarations
- NestedSpin.lean 18 declarations
- NormalOrder.lean 64 declarations
- Occupation.lean 79 declarations
- PairDecomposition.lean 9 declarations
- PairEndpoints.lean 3 declarations
- PairEnergy.lean 80 declarations
- PairSpin.lean 15 declarations
- PhysicalAveraging.lean 14 declarations
- PhysicalSpinSpectrum.lean 18 declarations
- RationalCoupling.lean 14 declarations
- RationalCreatedGram.lean 12 declarations
- RationalExterior.lean 14 declarations
- RationalFourCertificate.lean 10 declarations
- RationalFourCoefficients.lean 5 declarations
- RationalFourComputable.lean 6 declarations
- RationalFourRows.lean 11 declarations
- RationalRowComputable.lean 4 declarations
- RationalRows.lean 16 declarations
- RealOccupation.lean 18 declarations
- RealPositivity.lean 6 declarations
- RealSpinSquare.lean 10 declarations
- SpectralBound.lean 51 declarations
- SpinAveraging.lean 13 declarations
- SpinWork.lean 50 declarations
- SumTable10.lean 82 declarations
- SumTable11.lean 98 declarations
- SumTable12.lean 98 declarations
- SumTable13.lean 114 declarations
- SumTable14.lean 114 declarations
- SumTable15.lean 130 declarations
- SumTable16.lean 130 declarations
- SumTable17.lean 146 declarations
- SumTable18.lean 146 declarations
- SumTable19.lean 162 declarations
- SumTable20.lean 162 declarations
- SumTable21.lean 178 declarations
- SumTable22.lean 178 declarations
- SumTable23.lean 194 declarations
- SumTable5.lean 50 declarations
- SumTable7.lean 66 declarations
- SumTable8.lean 66 declarations
- SumTable9.lean 82 declarations
- TensorSpin.lean 87 declarations
- ThreeAveraging.lean 6 declarations
- ThreeBounds.lean 11 declarations
- ThreeComparison.lean 7 declarations
- ThreeGram.lean 25 declarations
- ThreeSpectrum.lean 12 declarations
- ThreeSpin.lean 14 declarations
- WedgeIdentification.lean 36 declarations
- ZeroCertificates.lean 9 declarations