`OAI/Probability/InvariantIsing/Cavity/`

2536 declarations, 0 contain sorry, 0 declared as axioms; 773 files

Files

CavityActualCovariance.lean 7 declarations
CavityActualDiagonal.lean 5 declarations
CavityActualErrorRates.lean 3 declarations
CavityActualFactorLimit.lean 1 declarations
CavityActualGoodCompression.lean 1 declarations
CavityAffineCounts.lean 12 declarations
CavityAffineFamily.lean 7 declarations
CavityAffineMinimumLower.lean 1 declarations
CavityAffinePressureLimit.lean 1 declarations
CavityAffinePressureLower.lean 1 declarations
CavityAffineRetained.lean 9 declarations
CavityAffineWindows.lean 6 declarations
CavityAmplitudePenalty.lean 3 declarations
CavityAsymptoticSelfConsistency.lean 2 declarations
CavityBaseAmplitude.lean 4 declarations
CavityBaseCutoffFactor.lean 3 declarations
CavityBaseCutoffLaw.lean 1 declarations
CavityBaseCutoffProduct.lean 1 declarations
CavityBaseEigenspaces.lean 4 declarations
CavityBaseExhaustion.lean 3 declarations
CavityBaseGroupLimits.lean 4 declarations
CavityBaseGroups.lean 7 declarations
CavityBaseHaarFactorization.lean 5 declarations
CavityBaseOverlap.lean 3 declarations
CavityBasePerturbedLaw.lean 2 declarations
CavityBaseReplacement.lean 6 declarations
CavityBaseRestrictedLaw.lean 4 declarations
CavityBaseSpecialHaar.lean 4 declarations
CavityBaseSpectralSum.lean 4 declarations
CavityBaseWardLimit.lean 1 declarations
CavityBlockFactor.lean 10 declarations
CavityBlockMarkedLaw.lean 2 declarations
CavityBoundaryCutoff.lean 8 declarations
CavityBoundedRegularizationError.lean 1 declarations
CavityBoundedReweighting.lean 10 declarations
CavityBoundedSecant.lean 3 declarations
CavityCanonicalBlockLimit.lean 5 declarations
CavityCanonicalCappedLog.lean 1 declarations
CavityCanonicalContinuity.lean 2 declarations
CavityCanonicalGroupAverage.lean 5 declarations
CavityCanonicalGrowingLimit.lean 1 declarations
CavityCanonicalHaarLog.lean 4 declarations
CavityCanonicalLabels.lean 8 declarations
CavityCanonicalLogCoefficients.lean 1 declarations
CavityCanonicalLogIntegrability.lean 4 declarations
CavityCanonicalLogLaw.lean 1 declarations
CavityCanonicalLogLimit.lean 1 declarations
CavityCanonicalMass.lean 1 declarations
CavityCanonicalRestrictedLaw.lean 1 declarations
CavityCanonicalSynchronization.lean 1 declarations
CavityCanonicalTreeLogLaw.lean 1 declarations
CavityCapTailAverage.lean 1 declarations
CavityCappedBlockLog.lean 1 declarations
CavityCappedIncrement.lean 2 declarations
CavityCappedLog.lean 3 declarations
CavityCappedLogIntegrable.lean 1 declarations
CavityCappedLogLimit.lean 2 declarations
CavityCappedSpinTest.lean 4 declarations
CavityCascadeBlockLimit.lean 1 declarations
CavityCascadeCovariance.lean 2 declarations
CavityCascadeCovarianceLaw.lean 1 declarations
CavityCascadeMarkedLimit.lean 1 declarations
CavityCascadeSpectralLimit.lean 3 declarations
CavityCoefficientError.lean 4 declarations
CavityCoefficientLimit.lean 1 declarations
CavityCoefficientMean.lean 5 declarations
CavityCoefficientProbability.lean 6 declarations
CavityCoefficientReplacement.lean 1 declarations
CavityCoefficientSampling.lean 3 declarations
CavityCoefficientValueLimit.lean 1 declarations
CavityComparisonRates.lean 8 declarations
CavityComplement.lean 8 declarations
CavityCompletion.lean 1 declarations
CavityCompressionBlocks.lean 7 declarations
CavityCompressionCappedLog.lean 1 declarations
CavityCompressionFactorBound.lean 5 declarations
CavityCompressionFactors.lean 8 declarations
CavityCompressionLimitGeometry.lean 5 declarations
CavityCompressionLogLimit.lean 1 declarations
CavityCompressionRank.lean 4 declarations
CavityConcreteBase.lean 1 declarations
CavityConcreteComplement.lean 6 declarations
CavityConcreteFrameOrbit.lean 5 declarations
CavityConcreteHaar.lean 1 declarations
CavityConditionedFrame.lean 11 declarations
CavityConditionedProjection.lean 1 declarations
CavityConditioning.lean 4 declarations
CavityConstantHaarLog.lean 1 declarations
CavityContinuousCutoff.lean 16 declarations
CavityContinuousReplicaTilt.lean 3 declarations
CavityCountablePenalty.lean 1 declarations
CavityCountableTest.lean 1 declarations
CavityCoupledEnergy.lean 1 declarations
CavityCoupledOverlap.lean 1 declarations
CavityCoupledProjectors.lean 1 declarations
CavityCouplingAlgebra.lean 14 declarations
CavityCovariancePartitionBound.lean 2 declarations
CavityCutoffEnergyComparison.lean 1 declarations
CavityCutoffFloorLimit.lean 2 declarations
CavityCutoffLimit.lean 1 declarations
CavityCutoffMap.lean 3 declarations
CavityCutoffNormalizer.lean 3 declarations
CavityCutoffRadii.lean 2 declarations
CavityCutoffSubtype.lean 2 declarations
CavityCutoffTests.lean 3 declarations
CavityCutoffTightness.lean 4 declarations
CavityCutoffTotalBound.lean 1 declarations
CavityCutoffWeight.lean 2 declarations
CavityCutoffZero.lean 2 declarations
CavityCylinderPenalty.lean 3 declarations
CavityDeficitGap.lean 5 declarations
CavityDepthRatePair.lean 1 declarations
CavityDepthTestEvaluation.lean 1 declarations
CavityDeterminantDerivative.lean 5 declarations
CavityDiagonalFullMoment.lean 2 declarations
CavityDiagonalGap.lean 2 declarations
CavityDiagonalGaussian.lean 3 declarations
CavityDiagonalSpectralPrecision.lean 4 declarations
CavityDiracAverage.lean 2 declarations
CavityDisorderLimit.lean 2 declarations
CavityDisorderMean.lean 5 declarations
CavityDisorderPrefix.lean 3 declarations
CavityDisorderTest.lean 3 declarations
CavityDisorderTestComparison.lean 3 declarations
CavityEntropyMaximum.lean 3 declarations
CavityEnvelopeTelescoping.lean 1 declarations
CavityExtraLogAverage.lean 2 declarations
CavityExtraReplicaPrefix.lean 5 declarations
CavityExtraReplicas.lean 1 declarations
CavityFactorBlockProjection.lean 5 declarations
CavityFactorBound.lean 6 declarations
CavityFactorScaling.lean 3 declarations
CavityFiberFactor.lean 7 declarations
CavityFieldBound.lean 2 declarations
CavityFieldIncrement.lean 3 declarations
CavityFieldModulus.lean 5 declarations
CavityFieldPath.lean 9 declarations
CavityFieldResidual.lean 3 declarations
CavityFieldSelfConsistency.lean 2 declarations
CavityFiniteCappedComparison.lean 1 declarations
CavityFiniteCappedIncrement.lean 1 declarations
CavityFiniteCappedLog.lean 1 declarations
CavityFiniteCappedNumerator.lean 1 declarations
CavityFiniteCascadeBlock.lean 2 declarations
CavityFiniteCascadeGaussianAverage.lean 1 declarations
CavityFiniteCascadeSpinAverage.lean 1 declarations
CavityFiniteCovariance.lean 10 declarations
CavityFiniteCovarianceBound.lean 1 declarations
CavityFiniteCovariancePath.lean 9 declarations
CavityFiniteDeficit.lean 7 declarations
CavityFiniteDeficitPath.lean 13 declarations
CavityFiniteDepthTest.lean 1 declarations
CavityFiniteEvaluation.lean 1 declarations
CavityFiniteExponentLaw.lean 4 declarations
CavityFiniteField.lean 2 declarations
CavityFiniteFieldVariance.lean 3 declarations
CavityFiniteFullComparison.lean 1 declarations
CavityFiniteGaussian.lean 4 declarations
CavityFiniteGroupSelection.lean 5 declarations
CavityFiniteHeightContinuity.lean 3 declarations
CavityFiniteHeightLimit.lean 2 declarations
CavityFiniteIncrement.lean 2 declarations
CavityFiniteInnovation.lean 3 declarations
CavityFiniteLabeledLog.lean 1 declarations
CavityFiniteLabeledMoment.lean 1 declarations
CavityFiniteLogCap.lean 1 declarations
CavityFiniteLogDet.lean 4 declarations
CavityFiniteLogEvaluation.lean 1 declarations
CavityFiniteMeasurableAverage.lean 2 declarations
CavityFiniteModelDepth.lean 1 declarations
CavityFiniteModelNumerator.lean 1 declarations
CavityFiniteModelSpinTest.lean 1 declarations
CavityFiniteNormalizedSpin.lean 1 declarations
CavityFiniteNormalizer.lean 3 declarations
CavityFiniteOriginalIntegrability.lean 1 declarations
CavityFiniteOriginalMoment.lean 1 declarations
CavityFinitePressureLimit.lean 1 declarations
CavityFinitePriorBound.lean 3 declarations
CavityFinitePriorMoment.lean 1 declarations
CavityFiniteReplicaCovariance.lean 2 declarations
CavityFiniteReplicaLaw.lean 3 declarations
CavityFiniteRestrictedAverage.lean 1 declarations
CavityFiniteRestrictedComparison.lean 1 declarations
CavityFiniteRestrictedError.lean 1 declarations
CavityFiniteRestrictedModel.lean 1 declarations
CavityFiniteRestrictedNumerator.lean 1 declarations
CavityFiniteRoot.lean 5 declarations
CavityFiniteSpectralEntries.lean 3 declarations
CavityFiniteSpectralIntegral.lean 4 declarations
CavityFiniteSpinTest.lean 1 declarations
CavityFiniteTest.lean 2 declarations
CavityFiniteTestComparison.lean 1 declarations
CavityFiniteTiltedTail.lean 2 declarations
CavityFiniteTrialLower.lean 1 declarations
CavityFirstEnergyMoment.lean 2 declarations
CavityFixedMinimumLimit.lean 1 declarations
CavityFrameAlgebra.lean 6 declarations
CavityFrameHaar.lean 1 declarations
CavityFrameLimit.lean 4 declarations
CavityFrameLogBound.lean 6 declarations
CavityFrameMeasurable.lean 2 declarations
CavityFrameMoments.lean 8 declarations
CavityFrameOrbit.lean 5 declarations
CavityFrameRotation.lean 2 declarations
CavityFrameTails.lean 2 declarations
CavityFrameTransitive.lean 1 declarations
CavityFullCutoff.lean 5 declarations
CavityFullCutoffSequence.lean 1 declarations
CavityFullGibbs.lean 3 declarations
CavityFullGibbsMoment.lean 1 declarations
CavityFullLogEvaluation.lean 1 declarations
CavityFullMoment.lean 1 declarations
CavityFullProjectionMoment.lean 4 declarations
CavityFullSiteIdentity.lean 7 declarations
CavityFullSymmetry.lean 2 declarations
CavityFullTail.lean 10 declarations
CavityFullTightness.lean 2 declarations
CavityFullTilt.lean 13 declarations
CavityFullTreeCutoff.lean 1 declarations
CavityGaussianAffine.lean 8 declarations
CavityGaussianAffineImage.lean 1 declarations
CavityGaussianBasis.lean 4 declarations
CavityGaussianCappedNumerator.lean 1 declarations
CavityGaussianContinuity.lean 4 declarations
CavityGaussianCoordinateMap.lean 4 declarations
CavityGaussianCurveMean.lean 5 declarations
CavityGaussianEnvelope.lean 3 declarations
CavityGaussianFactor.lean 9 declarations
CavityGaussianFactorAlgebra.lean 5 declarations
CavityGaussianForestLaw.lean 2 declarations
CavityGaussianImage.lean 2 declarations
CavityGaussianInnovation.lean 2 declarations
CavityGaussianIntegral.lean 9 declarations
CavityGaussianJointTest.lean 3 declarations
CavityGaussianKernel.lean 2 declarations
CavityGaussianMarkDepth.lean 2 declarations
CavityGaussianMarkedLaw.lean 5 declarations
CavityGaussianNodeCovariance.lean 3 declarations
CavityGaussianNodeLaw.lean 8 declarations
CavityGaussianNodePrior.lean 6 declarations
CavityGaussianPenalty.lean 2 declarations
CavityGaussianPenaltyAlgebra.lean 2 declarations
CavityGaussianProjection.lean 5 declarations
CavityGaussianRadialMoments.lean 7 declarations
CavityGaussianRank.lean 6 declarations
CavityGaussianRankGram.lean 9 declarations
CavityGaussianRecursion.lean 6 declarations
CavityGaussianRestrictedNumerator.lean 1 declarations
CavityGaussianRoot.lean 6 declarations
CavityGaussianRotation.lean 11 declarations
CavityGaussianRotationCurve.lean 10 declarations
CavityGaussianRows.lean 9 declarations
CavityGaussianSpectral.lean 11 declarations
CavityGaussianSum.lean 2 declarations
CavityGaussianTestLaw.lean 3 declarations
CavityGaussianTiltLaw.lean 1 declarations
CavityGeometricIncrement.lean 1 declarations
CavityGeometricMean.lean 3 declarations
CavityGeometricTail.lean 2 declarations
CavityGeometricTest.lean 3 declarations
CavityGeometricWeightedTest.lean 1 declarations
CavityGibbsMeasureCovariance.lean 1 declarations
CavityGibbsProjection.lean 1 declarations
CavityGoodCompression.lean 1 declarations
CavityGoodEventMean.lean 1 declarations
CavityGram.lean 5 declarations
CavityGramProbability.lean 6 declarations
CavityGroupBlockGaussian.lean 5 declarations
CavityGroupCovariance.lean 4 declarations
CavityGroupCovariancePositive.lean 6 declarations
CavityGroupGaussian.lean 8 declarations
CavityGroupGibbsAverage.lean 2 declarations
CavityGroupGibbsInvariant.lean 4 declarations
CavityGroupGibbsProjection.lean 1 declarations
CavityGroupHaarProjection.lean 12 declarations
CavityGroupOverlapInvariant.lean 4 declarations
CavityGroupPartition.lean 3 declarations
CavityGroupProjection.lean 13 declarations
CavityGroupProjectionUniform.lean 3 declarations
CavityGroupedCappedLog.lean 1 declarations
CavityGroupedCoordinates.lean 7 declarations
CavityGroupedCutoffAverage.lean 1 declarations
CavityGroupedGram.lean 6 declarations
CavityGroupedWeightedAverage.lean 1 declarations
CavityGrowingGeometricLimit.lean 1 declarations
CavityHaarBoundedLimit.lean 1 declarations
CavityHaarCascadeMatch.lean 4 declarations
CavityHaarCoefficientFamily.lean 1 declarations
CavityHaarCoefficientProbability.lean 1 declarations
CavityHaarCompression.lean 2 declarations
CavityHaarCorrection.lean 2 declarations
CavityHaarCutoffComparison.lean 1 declarations
CavityHaarCutoffFamily.lean 1 declarations
CavityHaarCutoffLimit.lean 1 declarations
CavityHaarFactorCoefficients.lean 1 declarations
CavityHaarFiniteCutoff.lean 1 declarations
CavityHaarFiniteOverlap.lean 1 declarations
CavityHaarFiniteSpin.lean 1 declarations
CavityHaarGibbsCappedLog.lean 1 declarations
CavityHaarGibbsCappedReplica.lean 1 declarations
CavityHaarGibbsNumerator.lean 1 declarations
CavityHaarJointLaw.lean 1 declarations
CavityHaarJointTest.lean 1 declarations
CavityHaarJointUniform.lean 2 declarations
CavityHaarLogCoefficients.lean 1 declarations
CavityHaarLogIncrement.lean 1 declarations
CavityHaarLogObservable.lean 4 declarations
CavityHaarMarkedLaw.lean 4 declarations
CavityHaarMarkedLimit.lean 2 declarations
CavityHaarModelNumerator.lean 1 declarations
CavityHaarNormalizedCoefficients.lean 1 declarations
CavityHaarNumeratorAverage.lean 3 declarations
CavityHaarPenalizedLimit.lean 1 declarations
CavityHaarPenalty.lean 1 declarations
CavityHaarPriorMoment.lean 3 declarations
CavityHaarProjection.lean 4 declarations
CavityHaarRank.lean 1 declarations
CavityHaarRestrictedFloor.lean 1 declarations
CavityHaarRestrictedGibbs.lean 1 declarations
CavityHaarRestrictedModel.lean 1 declarations
CavityHaarRestrictedNumerator.lean 2 declarations
CavityHaarRestrictedRegularized.lean 1 declarations
CavityHaarRestrictedSpinMatch.lean 1 declarations
CavityHaarRestrictedWeight.lean 3 declarations
CavityHaarSides.lean 7 declarations
CavityHaarSpectralLabels.lean 7 declarations
CavityHaarSpinModel.lean 8 declarations
CavityHaarSpinNumerator.lean 3 declarations
CavityHaarStrictCascade.lean 1 declarations
CavityHaarVariablePenalty.lean 1 declarations
CavityIncrementComparison.lean 3 declarations
CavityInnovationAtomless.lean 2 declarations
CavityInnovationCovariancePositive.lean 1 declarations
CavityInnovationKernel.lean 3 declarations
CavityInnovationLeaves.lean 7 declarations
CavityInnovationPrefix.lean 6 declarations
CavityInnovationTree.lean 4 declarations
CavityLabeledCappedNumerator.lean 1 declarations
CavityLabeledDepthMean.lean 3 declarations
CavityLabeledDepthPair.lean 1 declarations
CavityLabeledDisorderLaw.lean 5 declarations
CavityLabeledLog.lean 2 declarations
CavityLabeledModel.lean 15 declarations
CavityLabeledModelIntegrability.lean 1 declarations
CavityLabeledModelNumerator.lean 7 declarations
CavityLabeledModelSpinMean.lean 3 declarations
CavityLabeledPriorLaw.lean 2 declarations
CavityLabeledPriorMoment.lean 3 declarations
CavityLabeledPriorTransport.lean 6 declarations
CavityLabeledProjectors.lean 9 declarations
CavityLabeledRestrictedModel.lean 8 declarations
CavityLabeledRestrictedNumerator.lean 1 declarations
CavityLabeledRoot.lean 3 declarations
CavityLabeledRootPair.lean 1 declarations
CavityLabeledSpin.lean 5 declarations
CavityLabeledSpinObservable.lean 1 declarations
CavityLabeledTiltMoment.lean 2 declarations
CavityLimitingComplement.lean 1 declarations
CavityLinearDepthEvaluation.lean 3 declarations
CavityLinearEnvelope.lean 5 declarations
CavityLinearGaussianMoment.lean 3 declarations
CavityLinearIntegrability.lean 3 declarations
CavityLinearLogEvaluation.lean 2 declarations
CavityLinearNoiseDepth.lean 2 declarations
CavityLinearNoiseEvaluation.lean 3 declarations
CavityLinearSpinEvaluation.lean 4 declarations
CavityLinearTiltMoment.lean 1 declarations
CavityLogCap.lean 3 declarations
CavityLogCapIntegrable.lean 3 declarations
CavityLogCovariance.lean 2 declarations
CavityLogDetPotential.lean 7 declarations
CavityLogFloor.lean 3 declarations
CavityLogL1.lean 2 declarations
CavityLogMap.lean 4 declarations
CavityLogMeanBound.lean 2 declarations
CavityLogNormalizerTransport.lean 6 declarations
CavityLogProbability.lean 1 declarations
CavityMagneticBlockModulus.lean 3 declarations
CavityMagneticDiagonal.lean 2 declarations
CavityMarkDepthLaw.lean 4 declarations
CavityMarkedTopology.lean 1 declarations
CavityMatrixResolventBound.lean 8 declarations
CavityMeasurableComplement.lean 15 declarations
CavityMeasurableTests.lean 2 declarations
CavityMinimumIncrement.lean 1 declarations
CavityMovingCappedLog.lean 1 declarations
CavityMovingCappedLogAE.lean 1 declarations
CavityMovingCappedReplica.lean 2 declarations
CavityMovingFullLog.lean 1 declarations
CavityMovingFullReplica.lean 1 declarations
CavityMovingFullReplicaFirst.lean 1 declarations
CavityMovingFullReplicaTight.lean 1 declarations
CavityMovingGroupMass.lean 3 declarations
CavityMovingLog.lean 2 declarations
CavityMovingMoments.lean 2 declarations
CavityMovingRatio.lean 2 declarations
CavityMovingReplicaTest.lean 1 declarations
CavityMovingRestrictedMoments.lean 1 declarations
CavityMovingReweighting.lean 1 declarations
CavityMultiplicityTransport.lean 2 declarations
CavityMultivariateGaussian.lean 4 declarations
CavityNormalizedCoefficientLimit.lean 1 declarations
CavityNormalizerIntegral.lean 7 declarations
CavityNormalizerProbability.lean 1 declarations
CavityNormalizerRegularization.lean 6 declarations
CavityOneReplicaGaussian.lean 2 declarations
CavityOneReplicaPath.lean 6 declarations
CavityOrbitAverage.lean 1 declarations
CavityOrbitFactorization.lean 1 declarations
CavityOrbitFactorizationAE.lean 2 declarations
CavityOrbitJointAE.lean 1 declarations
CavityOrderedBase.lean 5 declarations
CavityOrderedGroups.lean 8 declarations
CavityOrientation.lean 9 declarations
CavityOrientationArrayLaw.lean 5 declarations
CavityOrientationLog.lean 2 declarations
CavityOrientationOverlap.lean 5 declarations
CavityOrientationProbability.lean 3 declarations
CavityOrientedCoefficients.lean 3 declarations
CavityOrientedFamily.lean 5 declarations
CavityOrientedProjectors.lean 6 declarations
CavityOriginalComparison.lean 1 declarations
CavityOriginalCutoff.lean 2 declarations
CavityOriginalEntropyLimit.lean 1 declarations
CavityOriginalFactor.lean 5 declarations
CavityOriginalFullComparison.lean 1 declarations
CavityOriginalFullOverlap.lean 1 declarations
CavityOriginalFullSpin.lean 1 declarations
CavityOriginalGroupCutoffLimit.lean 2 declarations
CavityOriginalGroupFamily.lean 1 declarations
CavityOriginalOverlapLimit.lean 1 declarations
CavityOriginalRadialCutoff.lean 1 declarations
CavityOriginalRestrictedFamily.lean 1 declarations
CavityOriginalRestrictedHaar.lean 1 declarations
CavityOriginalSelfConsistency.lean 1 declarations
CavityOriginalSpinLimit.lean 1 declarations
CavityOriginalTreeLimit.lean 1 declarations
CavityOriginalTreeRegular.lean 1 declarations
CavityOriginalWeightedComparison.lean 1 declarations
CavityOverlapError.lean 9 declarations
CavityOverlapObservable.lean 3 declarations
CavityOverlapWeightedTest.lean 3 declarations
CavityPenaltyRate.lean 2 declarations
CavityPerturbationComparison.lean 3 declarations
CavityPerturbationKernel.lean 5 declarations
CavityPerturbationRates.lean 6 declarations
CavityPhysicalBase.lean 9 declarations
CavityPhysicalCavityHaar.lean 1 declarations
CavityPhysicalCoordinates.lean 2 declarations
CavityPhysicalCutoffComparison.lean 1 declarations
CavityPhysicalEnergy.lean 1 declarations
CavityPhysicalFactor.lean 7 declarations
CavityPhysicalFrameOrbit.lean 4 declarations
CavityPhysicalGibbsHaar.lean 1 declarations
CavityPhysicalGibbsSplit.lean 5 declarations
CavityPhysicalGram.lean 3 declarations
CavityPhysicalLogCoefficients.lean 1 declarations
CavityPhysicalLogIncrement.lean 1 declarations
CavityPhysicalLogLimit.lean 1 declarations
CavityPhysicalOverlapCutoff.lean 2 declarations
CavityPhysicalProjection.lean 8 declarations
CavityPhysicalProjectorIncrement.lean 1 declarations
CavityPhysicalSpinCutoff.lean 1 declarations
CavityPhysicalSpinObservable.lean 2 declarations
CavityPhysicalTrialLower.lean 1 declarations
CavityPhysicalVariationalLower.lean 1 declarations
CavityPosteriorPair.lean 3 declarations
CavityPrecisionPath.lean 3 declarations
CavityPrecisionTiltLaw.lean 3 declarations
CavityPrecisionTiltMoments.lean 6 declarations
CavityPrefixAffineFamily.lean 11 declarations
CavityPrefixOverlap.lean 1 declarations
CavityPreliminaryLower.lean 2 declarations
CavityPressureIncrement.lean 1 declarations
CavityPriorEndpointLaw.lean 3 declarations
CavityPriorFourthTail.lean 3 declarations
CavityProbabilityCovariance.lean 1 declarations
CavityProductDisorder.lean 2 declarations
CavityProductDisorderWeighted.lean 4 declarations
CavityProjectedForest.lean 7 declarations
CavityProjectedInnovation.lean 3 declarations
CavityProjectedLog.lean 1 declarations
CavityProjectedPair.lean 3 declarations
CavityProjectedRestrictedNumerator.lean 1 declarations
CavityProjectedSpin.lean 4 declarations
CavityProjectedSpinNumerator.lean 5 declarations
CavityProjectionControl.lean 4 declarations
CavityProjectionGeometry.lean 5 declarations
CavityProjectionLimit.lean 13 declarations
CavityProjectionUniform.lean 3 declarations
CavityProjectorCavity.lean 6 declarations
CavityProjectorCoefficientError.lean 1 declarations
CavityProjectorCoordinates.lean 6 declarations
CavityProjectorCutoffLaw.lean 2 declarations
CavityProjectorGibbsHaar.lean 4 declarations
CavityProjectorHaar.lean 1 declarations
CavityProjectorHaarMean.lean 4 declarations
CavityProjectorHamiltonian.lean 6 declarations
CavityProjectorJointHaar.lean 1 declarations
CavityProjectorJointLaw.lean 2 declarations
CavityProjectorLog.lean 3 declarations
CavityProjectorLogAverage.lean 1 declarations
CavityProjectorMeasurability.lean 9 declarations
CavityProjectorPartition.lean 3 declarations
CavityProjectorStabilizer.lean 2 declarations
CavityProjectorTensor.lean 7 declarations
CavityQuadraticAlgebra.lean 10 declarations
CavityQuadraticCompression.lean 7 declarations
CavityQuadraticCovariance.lean 3 declarations
CavityQuadraticNormalizer.lean 9 declarations
CavityQuadraticOneReplica.lean 5 declarations
CavityQuadraticReplica.lean 4 declarations
CavityQuadraticStepWeight.lean 5 declarations
CavityQuadraticTree.lean 4 declarations
CavityRDerivative.lean 7 declarations
CavityRRightDerivative.lean 2 declarations
CavityRadiusRemoval.lean 3 declarations
CavityRandomCutoff.lean 2 declarations
CavityRandomHaarLog.lean 3 declarations
CavityRandomPressureIncrement.lean 1 declarations
CavityRandomPriorCutoff.lean 1 declarations
CavityRandomTiltMoment.lean 1 declarations
CavityRandomTreeLogLaw.lean 1 declarations
CavityRationalAllSizes.lean 1 declarations
CavityRationalAuxiliary.lean 1 declarations
CavityRationalBaseCounts.lean 3 declarations
CavityRationalBaseOrder.lean 1 declarations
CavityRationalCounts.lean 9 declarations
CavityRationalFamily.lean 3 declarations
CavityRationalLabelIdentities.lean 4 declarations
CavityRationalMass.lean 7 declarations
CavityRationalMinimumLower.lean 1 declarations
CavityRationalMultiplicityLimit.lean 1 declarations
CavityRationalPressureLimit.lean 1 declarations
CavityRationalPressureLower.lean 1 declarations
CavityRationalRetained.lean 8 declarations
CavityRationalWindows.lean 9 declarations
CavityRecalculatedFiniteCascade.lean 1 declarations
CavityRecalculatedGaussian.lean 1 declarations
CavityRecalculatedLabels.lean 2 declarations
CavityRegularizedKernel.lean 2 declarations
CavityRegularizedMoments.lean 2 declarations
CavityRegularizedReweighting.lean 3 declarations
CavityReplicaCap.lean 3 declarations
CavityReplicaCapFirstMoment.lean 4 declarations
CavityReplicaCapIntegral.lean 2 declarations
CavityReplicaCapTail.lean 2 declarations
CavityReplicaComparison.lean 1 declarations
CavityReplicaCovarianceLaw.lean 3 declarations
CavityReplicaCutoff.lean 5 declarations
CavityReplicaDisorderTransport.lean 2 declarations
CavityReplicaFloor.lean 3 declarations
CavityReplicaGaussianAverage.lean 4 declarations
CavityReplicaLinearity.lean 2 declarations
CavityReplicaLogTilt.lean 3 declarations
CavityReplicaNodeCovariance.lean 4 declarations
CavityReplicaNodeProjection.lean 9 declarations
CavityReplicaProbabilityLaw.lean 2 declarations
CavityReplicaProductIntegral.lean 1 declarations
CavityReplicaRadius.lean 4 declarations
CavityReplicaSecant.lean 4 declarations
CavityReplicaTest.lean 4 declarations
CavityReplicaUpper.lean 2 declarations
CavityReservoirFrame.lean 11 declarations
CavityReservoirRotation.lean 6 declarations
CavityResidual.lean 3 declarations
CavityResidualFinite.lean 4 declarations
CavityResidualInnovation.lean 6 declarations
CavityResidualIntegrability.lean 1 declarations
CavityResidualKernel.lean 4 declarations
CavityResidualLeafLaw.lean 1 declarations
CavityResidualMarginal.lean 2 declarations
CavityResidualNormalizer.lean 3 declarations
CavityResidualPartition.lean 7 declarations
CavityResidualReplica.lean 5 declarations
CavityResidualSpinLaw.lean 2 declarations
CavityResidualSpinMarginal.lean 4 declarations
CavityResidualSpinSampling.lean 4 declarations
CavityResidueConvergence.lean 1 declarations
CavityResidueFamily.lean 6 declarations
CavityResolvent.lean 7 declarations
CavityResolventDerivative.lean 4 declarations
CavityRestrictedAverage.lean 4 declarations
CavityRestrictedFactor.lean 6 declarations
CavityRestrictedFactorIndicator.lean 1 declarations
CavityRestrictedSpinLimit.lean 1 declarations
CavityRestrictedSpinTest.lean 5 declarations
CavityRestrictedTilt.lean 3 declarations
CavityRetainedFrame.lean 11 declarations
CavityRetainedNorm.lean 5 declarations
CavityRetainedPairing.lean 4 declarations
CavityRetainedStack.lean 5 declarations
CavityRetainedWeight.lean 2 declarations
CavityRootInnovationLaw.lean 2 declarations
CavityRootIntegration.lean 2 declarations
CavityRootedDepthMean.lean 6 declarations
CavityRootedDepthTransport.lean 4 declarations
CavityRootedGaussian.lean 1 declarations
CavityRootedReplicaTransport.lean 3 declarations
CavityRootedResidual.lean 12 declarations
CavityRootedSpinChange.lean 3 declarations
CavityRootedSpinTestTransport.lean 6 declarations
CavityRootedSpinTransport.lean 6 declarations
CavityRootedTestMean.lean 6 declarations
CavityRotationArray.lean 7 declarations
CavityRotationCutoffWeight.lean 1 declarations
CavityRotationLogMean.lean 4 declarations
CavityRotationMeasurability.lean 4 declarations
CavityRotationProbability.lean 6 declarations
CavityRotationRestrictedIntegral.lean 1 declarations
CavityRotationVectorNorm.lean 1 declarations
CavityRotationVectors.lean 4 declarations
CavityRoundedSelfConsistency.lean 3 declarations
CavitySampledBlocks.lean 6 declarations
CavityScalarFieldLaw.lean 3 declarations
CavityScalarRecursion.lean 3 declarations
CavityScalarResolventBound.lean 7 declarations
CavityScalarRoot.lean 4 declarations
CavityScalarSpin.lean 7 declarations
CavitySchurDerivative.lean 2 declarations
CavitySchurDeterminant.lean 3 declarations
CavitySchurEvaluation.lean 5 declarations
CavitySchurFiniteR.lean 4 declarations
CavitySchurLogDeterminant.lean 4 declarations
CavitySchurMultiplicity.lean 6 declarations
CavitySchurSpectrum.lean 7 declarations
CavitySelectedCappedAverage.lean 2 declarations
CavitySelectedCappedSpin.lean 4 declarations
CavitySelectedDimensions.lean 1 declarations
CavitySelectedGroupFrames.lean 6 declarations
CavitySelectedHaarMoment.lean 4 declarations
CavitySelectedReplicaTest.lean 3 declarations
CavitySelectedRestrictedAverage.lean 1 declarations
CavitySelectedRestrictedSpin.lean 4 declarations
CavitySelfConsistencyLimit.lean 2 declarations
CavitySimultaneousFrame.lean 2 declarations
CavitySiteSymmetry.lean 4 declarations
CavitySlowDepth.lean 5 declarations
CavitySoftCutoff.lean 8 declarations
CavitySpecialBlocks.lean 7 declarations
CavitySpecialPythagoras.lean 4 declarations
CavitySpectralCap.lean 1 declarations
CavitySpectralCovariance.lean 1 declarations
CavitySpectralCutoffRadii.lean 1 declarations
CavitySpectralDensityIntegral.lean 3 declarations
CavitySpectralDensitySquare.lean 1 declarations
CavitySpectralGap.lean 4 declarations
CavitySpectralGaussianTest.lean 1 declarations
CavitySpectralHaarLimit.lean 1 declarations
CavitySpectralImages.lean 7 declarations
CavitySpectralMarkedLimit.lean 1 declarations
CavitySpectralMoment.lean 1 declarations
CavitySpectralRadius.lean 1 declarations
CavitySpectralSqueeze.lean 1 declarations
CavitySpectralStabilizer.lean 8 declarations
CavitySpectralStack.lean 4 declarations
CavitySpectralTransform.lean 5 declarations
CavitySpectralUpperEigenvalues.lean 3 declarations
CavitySphereAverage.lean 5 declarations
CavitySphereMoments.lean 2 declarations
CavitySpinFullLaw.lean 4 declarations
CavitySpinIntegrability.lean 2 declarations
CavitySpinIsometry.lean 12 declarations
CavitySpinLinearMoment.lean 2 declarations
CavitySpinObservable.lean 3 declarations
CavitySpinPrior.lean 2 declarations
CavitySpinProduct.lean 1 declarations
CavitySpinReplicaMatch.lean 1 declarations
CavitySpinSplit.lean 6 declarations
CavitySpinSplitOverlap.lean 4 declarations
CavitySpinTestEvaluation.lean 1 declarations
CavitySpinTiltTransport.lean 3 declarations
CavitySplitOverlapTest.lean 4 declarations
CavitySplitSpinTest.lean 3 declarations
CavitySplitTestContinuity.lean 1 declarations
CavitySplitTreeSpinTest.lean 2 declarations
CavityStabilizerAverage.lean 2 declarations
CavityStepPrecision.lean 2 declarations
CavityStrictCascadeLimit.lean 2 declarations
CavityStrictFiniteOverlap.lean 2 declarations
CavityStrictFiniteSpin.lean 2 declarations
CavityStrictGaussianLimit.lean 2 declarations
CavityStrictLevels.lean 7 declarations
CavityStrictMarkedLaw.lean 4 declarations
CavityStrictMarkedLimit.lean 1 declarations
CavityStrictUniformPath.lean 12 declarations
CavitySubsequenceLower.lean 1 declarations
CavityTailIntegral.lean 5 declarations
CavityTelescoping.lean 1 declarations
CavityTensorLogLaw.lean 2 declarations
CavityTensorPressureMean.lean 2 declarations
CavityTensorProbabilityLaw.lean 2 declarations
CavityTestExhaustion.lean 4 declarations
CavityTestLimit.lean 2 declarations
CavityTiltCovariance.lean 3 declarations
CavityTiltTransport.lean 2 declarations
CavityTiltedCap.lean 2 declarations
CavityTiltedTail.lean 3 declarations
CavityTreeCutoffMeasurability.lean 1 declarations
CavityTreeFullRegular.lean 2 declarations
CavityTreeLogIntegrability.lean 1 declarations
CavityTreeLogMeasurability.lean 3 declarations
CavityTreePressureIncrement.lean 1 declarations
CavityTreeRestrictedAverage.lean 1 declarations
CavityTreeRestrictedRegular.lean 1 declarations
CavityTruncation.lean 4 declarations
CavityUnflooredLog.lean 4 declarations
CavityUniformComparison.lean 3 declarations
CavityUniformMomentConstants.lean 4 declarations
CavityUniformTreeLimit.lean 2 declarations
CavityValueFubini.lean 4 declarations
CavityValueIdentity.lean 3 declarations
CavityValuePrimitive.lean 1 declarations
CavityVanishingPenalty.lean 3 declarations
CavityVariationalTrialLower.lean 1 declarations
CavityWeakApproximation.lean 2 declarations
CavityWeakRadialCutoff.lean 2 declarations
CavityWeightedMoments.lean 5 declarations
CavityWindowGram.lean 14 declarations
CavityWindowInputs.lean 3 declarations
CavityWindowMinimumLower.lean 1 declarations
CavityWindowVariationalLower.lean 1 declarations
ConsecutiveBlockPrior.lean 9 declarations
ConsecutiveBlockProjection.lean 1 declarations
ConsecutiveBlockSplit.lean 3 declarations
ConsecutiveBlockTransport.lean 6 declarations
ConsecutiveEnvelopeLower.lean 3 declarations
ConsecutiveFieldPressure.lean 5 declarations
ConsecutiveGroupProfile.lean 5 declarations
ConsecutiveMinimumIncrement.lean 1 declarations
ConsecutiveMinimumSequence.lean 2 declarations
ConsecutivePhysicalIncrement.lean 4 declarations
ConsecutiveProductMinimumConsistency.lean 1 declarations
ConsecutiveProductPrior.lean 9 declarations
ConsecutiveProductProjection.lean 3 declarations
ConsecutiveProductSpin.lean 1 declarations
ConsecutiveProductTreeSpin.lean 1 declarations
ConsecutiveProductTrialWitness.lean 1 declarations
ConsecutiveProductWeakConsistency.lean 1 declarations
ConsecutiveRationalConsistency.lean 1 declarations
ConsecutiveRationalMinimumConsistency.lean 1 declarations
ConsecutiveRationalSubsequenceTrial.lean 1 declarations
ConsecutiveRationalTrialWitness.lean 2 declarations
ConsecutiveWindowMinimumConsistency.lean 1 declarations
ConsecutiveWindowTrialWitness.lean 1 declarations
OffsetAffineIncrement.lean 1 declarations
OffsetAffineSubsequenceTrial.lean 1 declarations
OffsetBlockPrior.lean 9 declarations
OffsetBlockProjection.lean 1 declarations
OffsetBlockSpin.lean 5 declarations
OffsetBlockSymmetry.lean 5 declarations
OffsetEnvelopeLower.lean 3 declarations
OffsetFieldPopulation.lean 6 declarations
OffsetFieldPressure.lean 5 declarations
OffsetMinimumIncrement.lean 1 declarations
OffsetMinimumSequence.lean 2 declarations
OffsetPhysicalIncrement.lean 2 declarations
OffsetProductMinimumConsistency.lean 1 declarations
OffsetProductProjection.lean 2 declarations
OffsetProductSpin.lean 1 declarations
OffsetProductTreeSpin.lean 1 declarations
OffsetProductTrialWitness.lean 1 declarations
OffsetProductWeakConsistency.lean 1 declarations
OffsetWindowTrialWitness.lean 1 declarations
RepeatedBlockPrior.lean 10 declarations
RepeatedBlockProjection.lean 1 declarations
RepeatedBlockRemainderLimit.lean 2 declarations
RepeatedBlockRemainderPrior.lean 6 declarations
RepeatedBlockRemainderProjection.lean 1 declarations
RepeatedBlockRemainderSpin.lean 5 declarations
RepeatedBlockRemainderTail.lean 3 declarations
RepeatedBlockSpinIdentity.lean 2 declarations
RepeatedBlockTail.lean 3 declarations