OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/
1211 declarations, 0 contain sorry, 0 declared as axioms; 115 files
Files
- ChargePenalty.lean 8 declarations
- ChargeTransfer.lean 5 declarations
- CoerciveComplementLower.lean 3 declarations
- ComplementFormLower.lean 3 declarations
- ComplementParameterBounds.lean 2 declarations
- ComplementScaleBudget.lean 2 declarations
- ComplementSmallness.lean 2 declarations
- ElectronSlotBound.lean 9 declarations
- FiniteAtomicOutputs.lean 4 declarations
- FiniteBoxMatrix.lean 10 declarations
- FiniteBoxScale.lean 3 declarations
- FiniteCoefficientCorrection.lean 8 declarations
- FiniteCubeQuadrature.lean 10 declarations
- FiniteDifferenceError.lean 4 declarations
- FiniteOneBodyCorrection.lean 7 declarations
- FiniteOrbitalComplement.lean 1 declarations
- FiniteOrbitalLaplacian.lean 2 declarations
- FiniteOverlap.lean 1 declarations
- FiniteSourceBranch.lean 3 declarations
- FiniteTensorCross.lean 1 declarations
- FiniteTensorDiagonal.lean 2 declarations
- FiniteTensorFormCompression.lean 5 declarations
- FiniteTensorFormError.lean 4 declarations
- FiniteTensorKineticCompression.lean 2 declarations
- FiniteTensorNorm.lean 2 declarations
- FiniteTensorProjection.lean 7 declarations
- FiniteTensorResidual.lean 8 declarations
- FiniteTensorState.lean 6 declarations
- FiniteWellResidual.lean 4 declarations
- FockBlocks.lean 28 declarations
- FockChargePolynomial.lean 13 declarations
- FockCoefficientNorm.lean 11 declarations
- FockDensityTensor.lean 1 declarations
- FockEnergyError.lean 4 declarations
- FockGraphEntries.lean 5 declarations
- FockHubbardForm.lean 9 declarations
- FockNorm.lean 43 declarations
- FockOneBodyIntegral.lean 8 declarations
- FockResidualIntegral.lean 5 declarations
- FockSector.lean 21 declarations
- FockSiteOneBody.lean 9 declarations
- FockSlaterTensor.lean 17 declarations
- FockTensorCompression.lean 6 declarations
- FockTwoBodyContraction.lean 7 declarations
- FockTwoBodyIntegral.lean 7 declarations
- GlobalSinglet.lean 34 declarations
- GlobalSuperexchange.lean 4 declarations
- GramCorrection.lean 10 declarations
- GramPenalty.lean 5 declarations
- HalfFilledSector.lean 13 declarations
- HeisenbergOffsets.lean 11 declarations
- Hubbard.lean 34 declarations
- HubbardBottomBounds.lean 4 declarations
- HubbardEnergyLower.lean 3 declarations
- HubbardExcitation.lean 26 declarations
- HubbardFermionSpectrum.lean 30 declarations
- HubbardFormScale.lean 2 declarations
- HubbardGlobal.lean 32 declarations
- HubbardOccupation.lean 6 declarations
- HubbardReduction.lean 4 declarations
- HubbardSpin.lean 20 declarations
- HubbardTolerance.lean 3 declarations
- HubbardVariationalWitness.lean 4 declarations
- MediatorBlocks.lean 26 declarations
- MediatorCompression.lean 28 declarations
- MediatorEffective.lean 31 declarations
- MediatorForms.lean 12 declarations
- MediatorFullListCorrectness.lean 9 declarations
- MediatorGraph.lean 46 declarations
- MediatorIteration.lean 51 declarations
- MediatorListCorrectness.lean 10 declarations
- MediatorOffsets.lean 9 declarations
- MediatorParameters.lean 20 declarations
- MediatorPhysical.lean 11 declarations
- MediatorPromise.lean 8 declarations
- MediatorRounding.lean 10 declarations
- MediatorScaleBounds.lean 11 declarations
- MediatorSector.lean 21 declarations
- MediatorSimple.lean 13 declarations
- MediatorSpectrum.lean 8 declarations
- MediatorUnaryPrimitives.lean 16 declarations
- MediatorUnaryScale.lean 4 declarations
- MediatorUnarySecond.lean 5 declarations
- MediatorUnaryThird.lean 13 declarations
- OccupationFock.lean 8 declarations
- OccupationSector.lean 10 declarations
- OrthogonalBlockDecomposition.lean 8 declarations
- OrthonormalLocalizedModes.lean 13 declarations
- PairSpinOrbitals.lean 6 declarations
- PairTensorCompression.lean 4 declarations
- RepulsionBound.lean 9 declarations
- RepulsionCross.lean 9 declarations
- Singlet.lean 29 declarations
- SlaterOccupation.lean 15 declarations
- Spin.lean 33 declarations
- SpinEmbedding.lean 13 declarations
- SpinMatrixNorm.lean 33 declarations
- SpinTensorResidual.lean 2 declarations
- SuperexchangeSpectrum.lean 19 declarations
- TensorComplementBound.lean 2 declarations
- TensorComplementGap.lean 3 declarations
- TensorDifferential.lean 10 declarations
- TensorFirstReplacement.lean 8 declarations
- TensorFormDecomposition.lean 3 declarations
- TensorOccupationSector.lean 4 declarations
- TensorOperatorResidual.lean 4 declarations
- TensorSlotReplacement.lean 8 declarations
- TensorTotalReplacement.lean 4 declarations
- TensorTrial.lean 2 declarations
- TensorVariationalLower.lean 1 declarations
- WeightedNuclearCross.lean 6 declarations
- WeightedNuclearForm.lean 8 declarations
- WeightedPotentialBound.lean 2 declarations
- WeightedSourcePairing.lean 2 declarations
- WeightedSpinOrbitals.lean 4 declarations