`OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/`

2960 declarations, 0 contain sorry, 0 declared as axioms; 432 files

Files

AbsoluteNuclearForm.lean 1 declarations
AffinePhysicalOutput.lean 13 declarations
AffinePhysicalThreshold.lean 13 declarations
ApproximateBisection.lean 18 declarations
AtomicOutputs.lean 9 declarations
BoundedFormCross.lean 9 declarations
BoundedPotentialOperator.lean 10 declarations
CalibratedBisection.lean 9 declarations
CalibratedBisectionLocation.lean 5 declarations
CalibratedBisectionMachine.lean 2 declarations
CalibratedBisectionSchedule.lean 5 declarations
CalibratedContactCorrectness.lean 7 declarations
CalibratedEvaluationBudget.lean 3 declarations
CalibratedEvaluationComponents.lean 31 declarations
CalibratedEvaluationError.lean 1 declarations
CalibratedEvaluationParameters.lean 7 declarations
CalibratedGraphError.lean 4 declarations
CalibratedHoppingBound.lean 4 declarations
CalibratedLipschitzBound.lean 6 declarations
CalibratedMatrixError.lean 2 declarations
CalibrationCoefficientError.lean 1 declarations
CalibrationCoulombBrackets.lean 1 declarations
CalibrationEndpointSigns.lean 2 declarations
CalibrationGraphBudget.lean 2 declarations
CalibrationMesh.lean 16 declarations
CalibrationRationalBracket.lean 3 declarations
CalibrationSquareError.lean 3 declarations
CappedCoulombKernel.lean 13 declarations
CappedCoulombMass.lean 2 declarations
CappedCoulombTruncation.lean 3 declarations
CappedRawModulus.lean 2 declarations
CappedWells.lean 16 declarations
CenteredGaussEquiv.lean 11 declarations
CenteredGaussLabels.lean 12 declarations
CenteredGrid.lean 5 declarations
CenteredPhysicalThreshold.lean 15 declarations
ClassicalH1.lean 2 declarations
ClassicalResidualPairing.lean 5 declarations
ClassicalSlater.lean 6 declarations
ClassicalSlaterKinetic.lean 3 declarations
ClassicalSlaterSynthesis.lean 11 declarations
ClassicalTensor.lean 3 declarations
CompactCoulombJets.lean 3 declarations
CompactCoulombSmooth.lean 4 declarations
CompactNuclearPairing.lean 2 declarations
CompactOrbitalDensity.lean 7 declarations
CompactOrbitalNuclearError.lean 1 declarations
CompactOrbitalQuadrature.lean 1 declarations
CompactSobolevCore.lean 3 declarations
CompactSourceGrid.lean 2 declarations
CompactSourcePairing.lean 3 declarations
CompactSourceTransport.lean 4 declarations
ComplexFormSplit.lean 9 declarations
ComplexMollification.lean 9 declarations
ContactAdjustment.lean 18 declarations
ContactBaseSeparation.lean 9 declarations
ContactCalibratedGeometry.lean 9 declarations
ContactCalibration.lean 2 declarations
ContactCalibrationScale.lean 1 declarations
ContactCanonicalEdge.lean 3 declarations
ContactClosedCoordinates.lean 8 declarations
ContactDisplacement.lean 8 declarations
ContactEdgeNumber.lean 4 declarations
ContactExtent.lean 9 declarations
ContactGadgetStability.lean 5 declarations
ContactGadgets.lean 12 declarations
ContactGeometryBlockSemantics.lean 20 declarations
ContactGlobal.lean 11 declarations
ContactGlobalSeparation.lean 8 declarations
ContactGrid.lean 28 declarations
ContactHeightBisection.lean 12 declarations
ContactHeightBounds.lean 7 declarations
ContactHeightEvaluation.lean 8 declarations
ContactLattice.lean 4 declarations
ContactMediator.lean 44 declarations
ContactMediatorGeometry.lean 10 declarations
ContactMediatorLinks.lean 16 declarations
ContactPathBounds.lean 7 declarations
ContactPolynomialGeometry.lean 6 declarations
ContactPositionArray.lean 4 declarations
ContactQuotientBounds.lean 5 declarations
ContactRationalCoordinates.lean 9 declarations
ContactRationalGadget.lean 19 declarations
ContactRationalGlobal.lean 12 declarations
ContactRationalLocal.lean 10 declarations
ContactRealization.lean 3 declarations
ContactSourceGrid.lean 7 declarations
ContactSourceInputCorrectness.lean 8 declarations
ContactStrips.lean 9 declarations
ContactTemplates.lean 19 declarations
CoordinateLaplacian.lean 5 declarations
CoreOrbitalCongruence.lean 4 declarations
CoreOrbitalProjection.lean 9 declarations
CoreTensorFiber.lean 9 declarations
CorrectedComplement.lean 4 declarations
CorrectedCrossBound.lean 2 declarations
CorrectedCrossForm.lean 3 declarations
CorrectedDiagonalBound.lean 3 declarations
CorrectedManufacturedResidual.lean 3 declarations
CorrectedNuclearError.lean 3 declarations
CorrectedOneElectronProjection.lean 19 declarations
CorrectedRemainderGap.lean 1 declarations
CorrectedResidualPairing.lean 6 declarations
CorrectedStateCoordinates.lean 4 declarations
CoulombCalibration.lean 6 declarations
CoulombCubeCoordinates.lean 6 declarations
CoulombCubeModulus.lean 4 declarations
CoulombEvaluationError.lean 6 declarations
CoulombEvaluationParameters.lean 22 declarations
CoulombFarCell.lean 2 declarations
CoulombGram.lean 13 declarations
CoulombGramApprox.lean 4 declarations
CoulombInverseFifth.lean 14 declarations
CoulombKernelHomogeneity.lean 2 declarations
CoulombKernelSmooth.lean 3 declarations
CoulombNormalizationError.lean 2 declarations
CoulombPacketCoercivity.lean 2 declarations
CoulombPacketTests.lean 13 declarations
CoulombPackets.lean 13 declarations
CoulombPairEvaluation.lean 12 declarations
CoulombPairSum.lean 12 declarations
CoulombPoisson.lean 6 declarations
CoulombQuadrature.lean 5 declarations
CoulombQuadratureBudget.lean 7 declarations
CoulombRawEvaluation.lean 5 declarations
CoulombSourceCubature.lean 7 declarations
CoulombTargetLipschitz.lean 6 declarations
CoulombTargetRange.lean 3 declarations
CoulombTruncationSchedule.lean 12 declarations
CountertermEvaluation.lean 11 declarations
CubeGeometry.lean 17 declarations
CubeIntegral.lean 7 declarations
CubeMeasure.lean 3 declarations
DiagonalPenalty.lean 11 declarations
DirectionalFourthDerivative.lean 2 declarations
ExceptionalCellVolume.lean 2 declarations
ExplicitVerticalCutoff.lean 7 declarations
FullSpinTensorCoefficients.lean 4 declarations
FullTensorComplement.lean 1 declarations
GaussianFrequency.lean 11 declarations
GaussianJetBounds.lean 9 declarations
GaussianLine.lean 5 declarations
GaussianMollification.lean 2 declarations
GaussianPacket.lean 15 declarations
GaussianPoincare.lean 7 declarations
GaussianScalar.lean 2 declarations
GraphCoefficientStability.lean 4 declarations
GridGroundUpper.lean 3 declarations
GridNodePrecision.lean 2 declarations
GridNuclei.lean 5 declarations
GroundRoundingInterval.lean 3 declarations
H1BoundedForm.lean 11 declarations
H1FiniteProjection.lean 5 declarations
H1GraphCore.lean 9 declarations
H1PairingBound.lean 1 declarations
HeatDensityModulus.lean 4 declarations
HeatKernelModulus.lean 11 declarations
HeatSampleError.lean 4 declarations
HoppingBox.lean 5 declarations
HoppingQuadrature.lean 10 declarations
HoppingSchedule.lean 12 declarations
HydrogenInput.lean 3 declarations
InverseFifthCutoffGrid.lean 2 declarations
InverseFifthGrid.lean 4 declarations
IsolatedForms.lean 13 declarations
IsolatedPerturbation.lean 8 declarations
IsolatedSpectrum.lean 11 declarations
LocalizedCorrectedMatrixError.lean 2 declarations
LocalizedCorrectedOneBody.lean 7 declarations
LocalizedCoulomb.lean 18 declarations
LocalizedCoulombBox.lean 8 declarations
LocalizedCoulombGap.lean 2 declarations
LocalizedCoulombLipschitz.lean 7 declarations
LocalizedCoulombMatrix.lean 5 declarations
LocalizedCoulombNumerics.lean 5 declarations
LocalizedCoulombRadial.lean 9 declarations
LocalizedCoulombSymmetry.lean 4 declarations
LocalizedCoulombTranslation.lean 10 declarations
LocalizedCountertermMatrix.lean 4 declarations
LocalizedCounterterms.lean 10 declarations
LocalizedDensityMoment.lean 7 declarations
LocalizedDualMatrix.lean 10 declarations
LocalizedDuality.lean 9 declarations
LocalizedFockStates.lean 11 declarations
LocalizedFourIndex.lean 16 declarations
LocalizedGradientMoments.lean 5 declarations
LocalizedGram.lean 7 declarations
LocalizedGramConstants.lean 3 declarations
LocalizedGramSpacing.lean 5 declarations
LocalizedGroundUpper.lean 2 declarations
LocalizedHigherMoments.lean 7 declarations
LocalizedHubbard.lean 7 declarations
LocalizedHubbardEntries.lean 1 declarations
LocalizedHubbardForm.lean 5 declarations
LocalizedHubbardTensor.lean 2 declarations
LocalizedLeakage.lean 6 declarations
LocalizedLinearCoulomb.lean 9 declarations
LocalizedLinearOrbitals.lean 6 declarations
LocalizedMatrixDecayBound.lean 3 declarations
LocalizedModeDerivatives.lean 9 declarations
LocalizedModes.lean 12 declarations
LocalizedMomentTail.lean 14 declarations
LocalizedMultiwellResidual.lean 5 declarations
LocalizedNuclearHardy.lean 1 declarations
LocalizedOneBody.lean 9 declarations
LocalizedOneBodyMatrix.lean 4 declarations
LocalizedOrbitalGram.lean 13 declarations
LocalizedOverlapSpacing.lean 3 declarations
LocalizedRawDensity.lean 12 declarations
LocalizedSpinOperator.lean 2 declarations
LocalizedTensorResidual.lean 4 declarations
LocalizedTransition.lean 10 declarations
LocalizedWellMatrix.lean 4 declarations
LocalizedWellResidual.lean 6 declarations
ManufacturedCoercivity.lean 6 declarations
ManufacturedCompactQuadrature.lean 1 declarations
ManufacturedComplement.lean 4 declarations
ManufacturedComplementBudget.lean 3 declarations
ManufacturedEuler.lean 5 declarations
ManufacturedFarGrid.lean 1 declarations
ManufacturedFieldBounds.lean 14 declarations
ManufacturedFieldEvaluation.lean 16 declarations
ManufacturedFrequency.lean 5 declarations
ManufacturedGapScale.lean 4 declarations
ManufacturedGridError.lean 3 declarations
ManufacturedGridGroundComparison.lean 2 declarations
ManufacturedGridParameters.lean 1 declarations
ManufacturedGridWitness.lean 1 declarations
ManufacturedGrowingGap.lean 1 declarations
ManufacturedHubbardComparison.lean 1 declarations
ManufacturedManyElectron.lean 1 declarations
ManufacturedNuclearComparison.lean 1 declarations
ManufacturedNuclearForm.lean 1 declarations
ManufacturedNuclearTensorLower.lean 1 declarations
ManufacturedOneElectronGap.lean 2 declarations
ManufacturedOrbitalNuclearError.lean 1 declarations
ManufacturedOrbitalResidual.lean 8 declarations
ManufacturedPolynomialComparison.lean 1 declarations
ManufacturedPreciseResidual.lean 1 declarations
ManufacturedProjectedLower.lean 1 declarations
ManufacturedResidualGap.lean 2 declarations
ManufacturedResidualMajorant.lean 1 declarations
ManufacturedResidualPairing.lean 2 declarations
ManufacturedResidualParameters.lean 2 declarations
ManufacturedResidualScale.lean 2 declarations
ManufacturedScalarParameters.lean 1 declarations
ManufacturedScaleThreshold.lean 1 declarations
ManufacturedSlabLower.lean 2 declarations
ManufacturedTensorCoercivity.lean 1 declarations
ManufacturedTensorDiagonal.lean 2 declarations
ManufacturedTensorGap.lean 1 declarations
ManufacturedTensorLower.lean 1 declarations
ManufacturedTensorProjection.lean 3 declarations
ManufacturedTransport.lean 2 declarations
ManufacturedUniformComparison.lean 1 declarations
ManufacturedUniformFlow.lean 1 declarations
ManufacturedUniformGap.lean 2 declarations
ManufacturedVelocityEvaluation.lean 11 declarations
ManufacturedWeakResidual.lean 9 declarations
ManufacturedWellField.lean 23 declarations
MixedSlater.lean 12 declarations
MovingWells.lean 5 declarations
NormalizationArithmetic.lean 16 declarations
NormalizationQuadrature.lean 10 declarations
NormalizationSchedule.lean 14 declarations
NumericalGridRounding.lean 3 declarations
NumericalSquare.lean 1 declarations
OneBodyScaleBudget.lean 4 declarations
OneElectronClosure.lean 5 declarations
OneElectronComplexLaplacian.lean 5 declarations
OneElectronCoordinates.lean 13 declarations
OneElectronFormDecomposition.lean 3 declarations
OneElectronProjectedLower.lean 2 declarations
OneElectronTrial.lean 5 declarations
OrbitalBasisExtension.lean 1 declarations
OrbitalCellVolume.lean 1 declarations
OrbitalComplementCount.lean 4 declarations
OrbitalCutoff.lean 9 declarations
OrbitalCutoffTail.lean 13 declarations
OrbitalDerivative.lean 10 declarations
OrbitalGraphBounds.lean 4 declarations
OrbitalJetBounds.lean 3 declarations
OrbitalNuclearTail.lean 1 declarations
OrbitalTensor.lean 14 declarations
PlanarCalibration.lean 3 declarations
PlanarCompactnessEstimates.lean 5 declarations
PlanarCutoffTail.lean 8 declarations
PlanarDistributionAxes.lean 2 declarations
PlanarExponentialEnvelope.lean 5 declarations
PlanarFieldBounds.lean 7 declarations
PlanarForcing.lean 13 declarations
PlanarForcingModulus.lean 3 declarations
PlanarFrameBound.lean 5 declarations
PlanarGapFromUniqueness.lean 3 declarations
PlanarGradientMoments.lean 3 declarations
PlanarGroundDuality.lean 1 declarations
PlanarGroundIdentity.lean 4 declarations
PlanarGroundTransform.lean 16 declarations
PlanarGroundUniqueness.lean 3 declarations
PlanarHeatBoxBounds.lean 10 declarations
PlanarHeatBoxCoordinates.lean 9 declarations
PlanarHeatDifferential.lean 6 declarations
PlanarHeatEvolution.lean 7 declarations
PlanarHeatKernel.lean 10 declarations
PlanarHeatLimit.lean 6 declarations
PlanarHeatTimeModulus.lean 1 declarations
PlanarHeatTruncation.lean 6 declarations
PlanarHopping.lean 16 declarations
PlanarHoppingBounds.lean 9 declarations
PlanarIMS.lean 7 declarations
PlanarIMSBounds.lean 4 declarations
PlanarLaplaceIBP.lean 7 declarations
PlanarLocalization.lean 29 declarations
PlanarLowerTail.lean 10 declarations
PlanarModeDecay.lean 6 declarations
PlanarModeDerivatives.lean 13 declarations
PlanarModeEnergy.lean 4 declarations
PlanarModeH1.lean 36 declarations
PlanarModeJets.lean 4 declarations
PlanarModeProperties.lean 15 declarations
PlanarMultiwellGap.lean 5 declarations
PlanarMultiwellMatrix.lean 4 declarations
PlanarMultiwellProjection.lean 4 declarations
PlanarMultiwellScale.lean 5 declarations
PlanarNearGroundCompactness.lean 2 declarations
PlanarNormalizationBox.lean 3 declarations
PlanarNormalizationTail.lean 7 declarations
PlanarNormalized.lean 8 declarations
PlanarOverlap.lean 11 declarations
PlanarPartition.lean 9 declarations
PlanarPolynomialScale.lean 1 declarations
PlanarProjectionGap.lean 13 declarations
PlanarRadial.lean 11 declarations
PlanarResolvent.lean 12 declarations
PlanarResolventEquation.lean 14 declarations
PlanarResolventModulus.lean 3 declarations
PlanarResolventTails.lean 8 declarations
PlanarScaleChoice.lean 4 declarations
PlanarSharpDecay.lean 7 declarations
PlanarSiteCutoffs.lean 15 declarations
PlanarSliceProjection.lean 5 declarations
PlanarSobolev.lean 27 declarations
PlanarSobolevDuality.lean 10 declarations
PlanarSpectralInput.lean 5 declarations
PlanarTestCauchy.lean 3 declarations
PlanarTranslatedGap.lean 3 declarations
PlanarUniformCalibration.lean 2 declarations
PlanarWeakConstant.lean 6 declarations
PlanarWellBottom.lean 11 declarations
PlanarWellLocalization.lean 9 declarations
PlanarWellMatrix.lean 6 declarations
PlanarWellNumerics.lean 11 declarations
PlanarWellOverlap.lean 2 declarations
PrefactorCalibration.lean 10 declarations
PrefactorSourceCalibration.lean 3 declarations
PrefactorSourceContactCorrectness.lean 6 declarations
PrefactorSpacing.lean 1 declarations
RationalBoxRound.lean 14 declarations
RationalClamp.lean 5 declarations
RationalContactBudget.lean 1 declarations
RationalContactMatrix.lean 1 declarations
RationalExponential.lean 5 declarations
RationalFieldDifferences.lean 12 declarations
RationalGaussNodes.lean 10 declarations
RationalHeatBox.lean 21 declarations
RationalHeatPlaneError.lean 7 declarations
RationalHeatSample.lean 22 declarations
RationalLogScale.lean 5 declarations
RationalResolventError.lean 4 declarations
RationalSixQuadrature.lean 17 declarations
RationalSmoothTransition.lean 12 declarations
RationalSquareRoot.lean 7 declarations
RationalTaylorRegisters.lean 16 declarations
RationalTripleQuadrature.lean 13 declarations
RayleighGround.lean 2 declarations
RealMollification.lean 5 declarations
RealOneElectronState.lean 6 declarations
RealOrbitalResidual.lean 3 declarations
RealSpinOrbitals.lean 10 declarations
RectangleQuadrature.lean 3 declarations
ResolventNumericalBounds.lean 11 declarations
ResolventSchedule.lean 31 declarations
ScalarMollification.lean 8 declarations
ScalarScaleBudgets.lean 4 declarations
ScaledNuclearNear.lean 1 declarations
SeparatedNuclearNear.lean 2 declarations
SharpBlockPerturbation.lean 4 declarations
ShiftedHubbardBounds.lean 6 declarations
ShiftedPhysicalForm.lean 2 declarations
SingleSpinSource.lean 6 declarations
SlowLogarithmicExtent.lean 4 declarations
SmoothCutoffApproximation.lean 6 declarations
SobolevDensity.lean 5 declarations
SobolevDensityInput.lean 4 declarations
SplitCoordinates.lean 12 declarations
SplitFormIdentity.lean 8 declarations
SplitFormIntegrals.lean 8 declarations
SplitFrameBound.lean 1 declarations
SplitIntegratedBounds.lean 3 declarations
SplitProjectionBudget.lean 2 declarations
SplitProjectionPairing.lean 3 declarations
SplitPullback.lean 12 declarations
SplitSpectralBudget.lean 3 declarations
SplitTestFunctions.lean 9 declarations
TM2Composition.lean 1 declarations
ThirdOrderBottom.lean 6 declarations
ThirdOrderPerturbation.lean 7 declarations
ThirdOrderScale.lean 3 declarations
TransformedGauss.lean 5 declarations
TransformedGaussList.lean 15 declarations
TransformedGaussSeparation.lean 3 declarations
TruncatedNuclearForm.lean 2 declarations
UnitBinaryInclusion.lean 7 declarations
UnitProgramGroundInterval.lean 1 declarations
VerticalCappedForm.lean 22 declarations
VerticalCappedGap.lean 7 declarations
VerticalCappedScale.lean 3 declarations
VerticalCutoffTail.lean 7 declarations
VerticalEnergy.lean 4 declarations
VerticalFactorization.lean 3 declarations
VerticalMode.lean 14 declarations
VerticalOscillatorGap.lean 2 declarations
VerticalResidual.lean 9 declarations
VerticalSliceProjection.lean 5 declarations
VerticalSpectralInput.lean 2 declarations
WeakComplexLaplacian.lean 5 declarations
WeakH1Laplacian.lean 4 declarations
WeakH1Pairing.lean 3 declarations
WellCapDerivatives.lean 16 declarations
WellCapRegularity.lean 12 declarations
WellCover.lean 7 declarations
WellFieldOrbitalResidual.lean 7 declarations