OAI/Probability/InvariantIsing/Gaussian/
410 declarations, 0 contain sorry, 0 declared as axioms; 117 files
Files
- BaseGaussianVariance.lean 4 declarations
- BilinearGaussianComparison.lean 6 declarations
- BilinearGaussianMean.lean 2 declarations
- BilinearGaussianMinmax.lean 1 declarations
- BilinearGaussianMinmaxMean.lean 1 declarations
- CountableGaussianComparison.lean 8 declarations
- CountableGaussianVariance.lean 2 declarations
- DavidsonSzarekInput.lean 1 declarations
- GaussianBaseComparison.lean 3 declarations
- GaussianCenteredSquare.lean 3 declarations
- GaussianClippedStieltjes.lean 1 declarations
- GaussianClippedWeak.lean 1 declarations
- GaussianColumnDeletion.lean 3 declarations
- GaussianColumnDeviation.lean 4 declarations
- GaussianColumnDeviationMean.lean 2 declarations
- GaussianColumnProductLaw.lean 3 declarations
- GaussianColumnResolventContinuity.lean 4 declarations
- GaussianCompactVariance.lean 3 declarations
- GaussianComparisonSign.lean 2 declarations
- GaussianConeCutoff.lean 9 declarations
- GaussianCoordinateNorm.lean 7 declarations
- GaussianDiagonalQuadratic.lean 5 declarations
- GaussianEmpiricalWeak.lean 1 declarations
- GaussianExponentialShift.lean 2 declarations
- GaussianFiniteColumnMinimum.lean 2 declarations
- GaussianFourthMoment.lean 5 declarations
- GaussianGGBounds.lean 4 declarations
- GaussianGramColumns.lean 5 declarations
- GaussianGramEdges.lean 3 declarations
- GaussianGramEmpiricalTransform.lean 4 declarations
- GaussianGramExcessBound.lean 3 declarations
- GaussianGramLowerBound.lean 3 declarations
- GaussianGramNormBound.lean 3 declarations
- GaussianGramQuadraticError.lean 1 declarations
- GaussianGramResidualBound.lean 1 declarations
- GaussianGramResidualIntegrability.lean 3 declarations
- GaussianGramResidualMean.lean 2 declarations
- GaussianGramResolvent.lean 8 declarations
- GaussianGramResolventBounds.lean 4 declarations
- GaussianGramResolventEquation.lean 6 declarations
- GaussianGramTraceGap.lean 1 declarations
- GaussianGramTransformError.lean 2 declarations
- GaussianGramTransformLimit.lean 3 declarations
- GaussianGramTransformProbability.lean 1 declarations
- GaussianGramUniformIntegrability.lean 2 declarations
- GaussianLeaveOneColumn.lean 6 declarations
- GaussianLipschitzIntegrability.lean 2 declarations
- GaussianMaximumComparison.lean 2 declarations
- GaussianMeanInterpolation.lean 7 declarations
- GaussianMedianTail.lean 1 declarations
- GaussianMinmaxComparison.lean 1 declarations
- GaussianNormLowerMean.lean 2 declarations
- GaussianNormMoments.lean 4 declarations
- GaussianOperatorMean.lean 1 declarations
- GaussianPatternAspect.lean 5 declarations
- GaussianPatternCorollary.lean 1 declarations
- GaussianPatternEigenvalueMeasurability.lean 5 declarations
- GaussianPatternEuclideanNorm.lean 7 declarations
- GaussianPatternGroundFinite.lean 7 declarations
- GaussianPatternGroundLimit.lean 2 declarations
- GaussianPatternModel.lean 9 declarations
- GaussianPatternNorms.lean 9 declarations
- GaussianPatternOrbit.lean 5 declarations
- GaussianPatternOrbitLaw.lean 4 declarations
- GaussianPatternPressureLimit.lean 3 declarations
- GaussianPatternPublishedInputs.lean 7 declarations
- GaussianPatternRotation.lean 5 declarations
- GaussianPatternSingularMinimum.lean 3 declarations
- GaussianPatternSingularVariance.lean 3 declarations
- GaussianPatternZeroOrbit.lean 3 declarations
- GaussianQuadraticLaw.lean 3 declarations
- GaussianQuadraticPotential.lean 6 declarations
- GaussianScaledEmpiricalWeak.lean 2 declarations
- GaussianSingularFluctuation.lean 5 declarations
- GaussianSingularLowerMean.lean 1 declarations
- GaussianSingularSquareUI.lean 1 declarations
- GaussianSingularUpperEdge.lean 1 declarations
- GaussianSmoothing.lean 4 declarations
- GaussianTestVariance.lean 1 declarations
- GaussianTiltIncrement.lean 1 declarations
- GaussianTiltLinearGrowth.lean 2 declarations
- GaussianTranspose.lean 4 declarations
- GaussianTransposeLowerEdge.lean 2 declarations
- GaussianVarianceInput.lean 2 declarations
- GaussianZeroUpperExcess.lean 3 declarations
- GordonBounds.lean 10 declarations
- GordonComparison.lean 1 declarations
- GordonCovariance.lean 4 declarations
- GordonCurveMean.lean 3 declarations
- GordonGaussianInsertion.lean 1 declarations
- GordonSlopeSign.lean 1 declarations
- GordonValueBound.lean 3 declarations
- GordonWeights.lean 15 declarations
- HermitianGaussianQuadratic.lean 6 declarations
- HermitianQuadraticCoordinates.lean 1 declarations
- IndexedGaussianIntegrability.lean 3 declarations
- IndexedGaussianMaximum.lean 4 declarations
- IndexedGaussianMinmax.lean 3 declarations
- MPAngularCoordinates.lean 6 declarations
- MPAngularIntegrability.lean 4 declarations
- MPAngularMass.lean 2 declarations
- MPAngularShift.lean 3 declarations
- MPAngularTransform.lean 2 declarations
- MPClippedTransform.lean 2 declarations
- MPDensityIntegrability.lean 3 declarations
- MPDensityProbability.lean 2 declarations
- MPDensitySubstitution.lean 4 declarations
- MPDensitySupport.lean 4 declarations
- MPDensityTransform.lean 2 declarations
- MPEdgeArithmetic.lean 7 declarations
- MPMeasureSupport.lean 4 declarations
- MPTrigonometricCritical.lean 2 declarations
- MPTrigonometricDenominator.lean 5 declarations
- MPTrigonometricIntegral.lean 2 declarations
- MPTrigonometricPrimitive.lean 5 declarations
- MarchenkoPasturInput.lean 1 declarations
- MarchenkoPasturTransform.lean 9 declarations