OAI/Analysis/LiebThirring/
1200 declarations, 0 contain sorry, 0 declared as axioms; 62 files
Files
- ActionBounds.lean 17 declarations
- ActionPenalty.lean 13 declarations
- BoundState.lean 68 declarations
- BoundaryParity.lean 11 declarations
- BoundaryValues.lean 20 declarations
- CoerciveInverse.lean 5 declarations
- CompactAlternative.lean 1 declarations
- ComplexFamilies.lean 5 declarations
- ConnectingPath.lean 5 declarations
- Continuation.lean 23 declarations
- ContinuousRepresentative.lean 3 declarations
- CubeFlags.lean 70 declarations
- CutoffEnergy.lean 54 declarations
- DiscreteSpectrum.lean 3 declarations
- Eigenspace.lean 13 declarations
- EigenvalueSum.lean 6 declarations
- EnergyAlgebra.lean 14 declarations
- EquivariantFlags.lean 27 declarations
- ExtremizerMass.lean 3 declarations
- FieldFlow.lean 20 declarations
- FieldLimit.lean 28 declarations
- FieldPrimitive.lean 28 declarations
- FieldRegularity.lean 38 declarations
- FiniteParity.lean 53 declarations
- FlagApproximation.lean 2 declarations
- FlagGeometry.lean 38 declarations
- FlowContinuation.lean 10 declarations
- FormCongruence.lean 9 declarations
- FreeForm.lean 7 declarations
- FreeLocus.lean 27 declarations
- Gamma.lean 7 declarations
- GenericPosition.lean 34 declarations
- InitialOrbit.lean 26 declarations
- IntervalAction.lean 7 declarations
- LocalCompactness.lean 10 declarations
- LocalWeight.lean 5 declarations
- LowestEigenvalue.lean 4 declarations
- Main.lean 4 declarations
- MatrixFlow.lean 45 declarations
- MatrixOrder.lean 88 declarations
- MatrixTangent.lean 21 declarations
- Model.lean 15 declarations
- MomentBound.lean 7 declarations
- Multiplication.lean 12 declarations
- NegativeResolvent.lean 6 declarations
- OneState.lean 2 declarations
- OperatorForm.lean 6 declarations
- OperatorGraph.lean 24 declarations
- PotentialCompactness.lean 5 declarations
- PotentialSplit.lean 1 declarations
- QuadraticForms.lean 4 declarations
- RankOne.lean 57 declarations
- Resolvent.lean 11 declarations
- ResolventCalculus.lean 37 declarations
- RowSigns.lean 74 declarations
- SchrodingerOperator.lean 5 declarations
- SobolevBound.lean 6 declarations
- SobolevProjection.lean 18 declarations
- SpectralMain.lean 12 declarations
- SpectralMoment.lean 4 declarations
- SpectralTrials.lean 7 declarations
- WeightedCutoff.lean 15 declarations