`OAI/Probability/InvariantIsing/Fields/`

1607 declarations, 0 contain sorry, 0 declared as axioms; 394 files

Files

CanonicalOrthogonalLaw.lean 11 declarations
CanonicalPairRootLaw.lean 5 declarations
CanonicalRootReconstruction.lean 5 declarations
CanonicalSpinWeights.lean 3 declarations
CascadeKeepUpdate.lean 1 declarations
CascadeMarking.lean 6 declarations
CascadeSeedCoupling.lean 1 declarations
CascadeSeedLeaf.lean 3 declarations
CascadeSeedLeafLaw.lean 1 declarations
CascadeSeedPairCoordinates.lean 1 declarations
CascadeSeedPath.lean 3 declarations
CascadeSeedRegular.lean 6 declarations
CascadeSeedReplicaLaw.lean 1 declarations
CascadeSeedRetainedLaw.lean 1 declarations
CascadeSeedTree.lean 4 declarations
CascadeTilt.lean 11 declarations
CascadeUnweightedAncestry.lean 2 declarations
Field.lean 20 declarations
FieldAdjacentDerivative.lean 3 declarations
FieldAdjacentOrder.lean 8 declarations
FieldAdjacentScalarLaw.lean 5 declarations
FieldAffineAverageDerivative.lean 3 declarations
FieldAffineMoments.lean 11 declarations
FieldAffineNeighborhood.lean 1 declarations
FieldAffineRecursion.lean 6 declarations
FieldAffineScalarBridge.lean 4 declarations
FieldAffineSecondDerivative.lean 4 declarations
FieldAffineShape.lean 1 declarations
FieldBounds.lean 9 declarations
FieldCanonicalEndpoint.lean 7 declarations
FieldCanonicalRootLaw.lean 3 declarations
FieldCanonicalVectorMoments.lean 5 declarations
FieldCapEstimate.lean 10 declarations
FieldCascade.lean 5 declarations
FieldCommonDepthLaw.lean 3 declarations
FieldCommonRefinement.lean 13 declarations
FieldCompensatedTangent.lean 4 declarations
FieldConstantPrefix.lean 4 declarations
FieldCoordinateDerivative.lean 12 declarations
FieldCouplingExtension.lean 3 declarations
FieldCovarianceScaling.lean 2 declarations
FieldDepthPair.lean 7 declarations
FieldEndpointIntegrability.lean 3 declarations
FieldEndpointMoment.lean 4 declarations
FieldEndpointProduct.lean 3 declarations
FieldEndpointSampling.lean 9 declarations
FieldEnergyCoordinates.lean 9 declarations
FieldEntropySequence.lean 2 declarations
FieldEvenTransition.lean 3 declarations
FieldFiniteAverageDerivative.lean 3 declarations
FieldFiniteCoordinateAverage.lean 1 declarations
FieldFiniteCoordinates.lean 6 declarations
FieldFiniteCovariance.lean 2 declarations
FieldFiniteDirections.lean 4 declarations
FieldFiniteDomain.lean 18 declarations
FieldFiniteFamily.lean 9 declarations
FieldFiniteLocal.lean 1 declarations
FieldFiniteMeasurable.lean 10 declarations
FieldFiniteMoments.lean 13 declarations
FieldFiniteNeighborhood.lean 5 declarations
FieldFiniteRecursion.lean 6 declarations
FieldFiniteShift.lean 4 declarations
FieldFiniteShiftBounds.lean 3 declarations
FieldFiniteShiftData.lean 10 declarations
FieldFiniteSupport.lean 2 declarations
FieldFiniteTiltDerivative.lean 6 declarations
FieldFiniteTransformBounds.lean 10 declarations
FieldFiniteTransformData.lean 11 declarations
FieldFiniteTransformDerivative.lean 3 declarations
FieldFoldedDensity.lean 3 declarations
FieldFoldedKernel.lean 13 declarations
FieldGaussianAmplitude.lean 4 declarations
FieldGaussianContinuity.lean 5 declarations
FieldGaussianFamilyEnvelope.lean 1 declarations
FieldGaussianFamilyGenerator.lean 1 declarations
FieldGaussianFamilyLocal.lean 1 declarations
FieldGaussianFamilyRaw.lean 1 declarations
FieldGaussianFolding.lean 7 declarations
FieldGaussianIntegrability.lean 2 declarations
FieldGaussianOrder.lean 3 declarations
FieldGaussianOrdinaryOrder.lean 2 declarations
FieldGaussianPairDerivative.lean 2 declarations
FieldGaussianProduct.lean 1 declarations
FieldGaussianQuadraticEnvelope.lean 2 declarations
FieldGaussianRecursionOrder.lean 5 declarations
FieldGaussianSemigroup.lean 4 declarations
FieldGaussianTerminal.lean 4 declarations
FieldGaussianTiltMoments.lean 3 declarations
FieldGaussianTransformLaw.lean 9 declarations
FieldGaussianVarianceDerivative.lean 1 declarations
FieldHeightBoundaryContinuity.lean 5 declarations
FieldHeightBox.lean 6 declarations
FieldHeightChart.lean 16 declarations
FieldHeightClosedSupport.lean 1 declarations
FieldHeightCone.lean 10 declarations
FieldHeightFinalOrder.lean 6 declarations
FieldHeightGradient.lean 2 declarations
FieldHeightHessianSign.lean 3 declarations
FieldHeightInteriorLaw.lean 7 declarations
FieldHeightInteriorOrder.lean 2 declarations
FieldHeightJoint.lean 9 declarations
FieldHeightLists.lean 4 declarations
FieldHeightLocal.lean 1 declarations
FieldHeightRadialHessian.lean 3 declarations
FieldHeightRegularization.lean 16 declarations
FieldHeightSupport.lean 1 declarations
FieldHeightUpdate.lean 14 declarations
FieldHessianAlgebra.lean 2 declarations
FieldIncrementMgf.lean 4 declarations
FieldL1.lean 3 declarations
FieldLevelPath.lean 5 declarations
FieldLikelihoodRatio.lean 1 declarations
FieldLipschitzTransport.lean 4 declarations
FieldLogMean.lean 2 declarations
FieldLogNormalizer.lean 7 declarations
FieldMagnetization.lean 12 declarations
FieldMagnetizationFiber.lean 3 declarations
FieldMagnetizationModulus.lean 3 declarations
FieldMagnetizationTies.lean 1 declarations
FieldMajorant.lean 11 declarations
FieldMajorantFold.lean 9 declarations
FieldMajorantGaussian.lean 5 declarations
FieldOverlapIncrement.lean 3 declarations
FieldPairInput.lean 2 declarations
FieldPairProductLaw.lean 3 declarations
FieldPairingContinuity.lean 2 declarations
FieldPairingError.lean 2 declarations
FieldPairingPathError.lean 2 declarations
FieldParameterGrowth.lean 2 declarations
FieldParameterOrder.lean 1 declarations
FieldPartitionSupport.lean 7 declarations
FieldProductSpinAveraging.lean 3 declarations
FieldProjectionLoss.lean 5 declarations
FieldProjectionMean.lean 5 declarations
FieldPublishedEvaluation.lean 9 declarations
FieldPublishedPairInput.lean 8 declarations
FieldQuantizer.lean 5 declarations
FieldQuantizerError.lean 2 declarations
FieldRadialBackward.lean 3 declarations
FieldRadialCovariance.lean 5 declarations
FieldRadialOverlap.lean 1 declarations
FieldRawTangent.lean 2 declarations
FieldRealVariance.lean 6 declarations
FieldRefineCut.lean 12 declarations
FieldRefineIncrements.lean 8 declarations
FieldRefineMagnetization.lean 4 declarations
FieldRefinePaths.lean 3 declarations
FieldResidualSpinEvaluation.lean 3 declarations
FieldRootOrder.lean 3 declarations
FieldRootPrefixLaw.lean 1 declarations
FieldScalarChain.lean 7 declarations
FieldScalarComposition.lean 8 declarations
FieldScalarDerivative.lean 2 declarations
FieldScalarLogCoshSecond.lean 4 declarations
FieldScalarOrder.lean 4 declarations
FieldScalarOverlap.lean 6 declarations
FieldScalarSampling.lean 8 declarations
FieldScalarScaling.lean 10 declarations
FieldScalarSecondDerivative.lean 4 declarations
FieldScalarSquareOrder.lean 2 declarations
FieldSecondBounds.lean 5 declarations
FieldSecondCovariance.lean 1 declarations
FieldSecondFamily.lean 9 declarations
FieldSecondMeanBounds.lean 5 declarations
FieldSecondMeanDerivative.lean 5 declarations
FieldSecondMeasurable.lean 7 declarations
FieldSecondRecursion.lean 3 declarations
FieldSecondTangentDerivative.lean 3 declarations
FieldShiftMoments.lean 2 declarations
FieldSimpleApproximation.lean 3 declarations
FieldSmoothFamily.lean 17 declarations
FieldSpatialParameterOrder.lean 3 declarations
FieldSpinDerivative.lean 3 declarations
FieldSpinEvaluation.lean 3 declarations
FieldSpinFolding.lean 3 declarations
FieldSpinKernelOrder.lean 6 declarations
FieldSpinLinear.lean 4 declarations
FieldSpinLipschitz.lean 1 declarations
FieldSpinMeasurability.lean 5 declarations
FieldSpinPairConditioning.lean 2 declarations
FieldSpinProduct.lean 4 declarations
FieldSpinProductLaw.lean 2 declarations
FieldSpinProjectionEnergy.lean 2 declarations
FieldSpinSampling.lean 11 declarations
FieldSpinSecondDerivative.lean 2 declarations
FieldSpinTransition.lean 10 declarations
FieldSpinVariance.lean 5 declarations
FieldSquarePrefix.lean 2 declarations
FieldTail.lean 6 declarations
FieldTailMgf.lean 3 declarations
FieldTangentOrder.lean 5 declarations
FieldTerminalGenerator.lean 3 declarations
FieldTerminalOne.lean 6 declarations
FieldTerminalOrder.lean 7 declarations
FieldTiltAverageDerivative.lean 2 declarations
FieldTiltDerivative.lean 1 declarations
FieldTiltedFamilyDerivative.lean 3 declarations
FieldTiltedPairDerivative.lean 2 declarations
FieldVaryingContinuity.lean 5 declarations
FieldVaryingRecursion.lean 12 declarations
FieldVectorPairSampling.lean 8 declarations
FieldVectorSampling.lean 10 declarations
FieldWasserstein.lean 7 declarations
FieldZeroIncrement.lean 5 declarations
LabeledAncestrySampling.lean 2 declarations
LabeledReplicaAncestry.lean 3 declarations
LabeledScaledAncestry.lean 4 declarations
MarkEndpointIntegral.lean 7 declarations
MarkEndpointKernel.lean 7 declarations
MarkForestRootLaw.lean 2 declarations
MarkPairRecursion.lean 1 declarations
NoiseLeafAncestry.lean 3 declarations
NoiseReplicaPairData.lean 3 declarations
PhysicalFieldComparison.lean 3 declarations
PhysicalFieldPermutation.lean 4 declarations
PhysicalFieldPopulationComparison.lean 1 declarations
PhysicalFieldPopulationLimit.lean 2 declarations
PoissonLabeledWeights.lean 3 declarations
PoissonScaledWeights.lean 5 declarations
PositiveFieldApproximation.lean 6 declarations
PriorArrayDiagonal.lean 5 declarations
PriorArrayDiagonalWard.lean 2 declarations
PriorArrayLaw.lean 2 declarations
PriorArrayResidual.lean 1 declarations
PriorArrayResidualBound.lean 1 declarations
PriorArrayWard.lean 3 declarations
PriorContactContinuity.lean 5 declarations
PriorContactField.lean 4 declarations
PriorContactGG.lean 1 declarations
PriorContactMinimum.lean 5 declarations
PriorContactTemperature.lean 2 declarations
PriorDiagonalMinimum.lean 1 declarations
PriorDiagonalStatistics.lean 2 declarations
PriorEnergyLimit.lean 3 declarations
PriorFieldDerivative.lean 8 declarations
PriorFieldInsertionLaw.lean 7 declarations
PriorFieldLogNormalizer.lean 7 declarations
PriorFiniteGG.lean 6 declarations
PriorFixedGeometricLimit.lean 1 declarations
PriorFixedMinimumLimit.lean 1 declarations
PriorFrozenCGF.lean 3 declarations
PriorFrozenGibbs.lean 2 declarations
PriorFrozenReference.lean 11 declarations
PriorFullLogEvaluation.lean 1 declarations
PriorGGExistence.lean 3 declarations
PriorGGMinimum.lean 1 declarations
PriorGGWardExistence.lean 2 declarations
PriorGaussianMinimum.lean 2 declarations
PriorKernelDiagonal.lean 2 declarations
PriorLabeledDepthMean.lean 3 declarations
PriorLabeledDepthPair.lean 1 declarations
PriorLabeledModelSpin.lean 3 declarations
PriorLabeledOverlapObservable.lean 1 declarations
PriorLabeledRootPair.lean 1 declarations
PriorLabeledSpinObservable.lean 1 declarations
PriorLimitingDiagonal.lean 1 declarations
PriorLimitingGG.lean 2 declarations
PriorLinearIntegrability.lean 1 declarations
PriorLinearLogEvaluation.lean 2 declarations
PriorMinimumBounds.lean 1 declarations
PriorMinimumCoordinates.lean 4 declarations
PriorMinimumEnvelope.lean 2 declarations
PriorMinimumFluctuations.lean 2 declarations
PriorMinimumIncrement.lean 1 declarations
PriorNamespacedVariance.lean 1 declarations
PriorPerturbationCost.lean 2 declarations
PriorPerturbationVariance.lean 1 declarations
PriorPerturbedWardLimits.lean 1 declarations
PriorPosteriorPair.lean 1 declarations
PriorPrincipalWard.lean 3 declarations
PriorProjectedLog.lean 1 declarations
PriorProjectedPair.lean 3 declarations
PriorReplicaAverage.lean 8 declarations
PriorResidualIntegrability.lean 1 declarations
PriorResidualSpinMarginal.lean 2 declarations
PriorSiteModulus.lean 2 declarations
PriorSpinLeafConditioning.lean 11 declarations
PriorTemperatureCGF.lean 6 declarations
PriorTemperatureDerivative.lean 1 declarations
PriorTemperatureModulus.lean 1 declarations
PriorTensorMinimum.lean 7 declarations
PriorTensorNamespace.lean 7 declarations
PriorTensorPressure.lean 5 declarations
PriorTensorReference.lean 8 declarations
PriorZeroFieldPressure.lean 4 declarations
RationalFieldApproximation.lean 1 declarations
RationalFieldLaw.lean 10 declarations
SeedForestPairData.lean 2 declarations
SeedIndependentKernel.lean 1 declarations
SeedIndependentPairEvaluation.lean 2 declarations
SeedPairIntegral.lean 1 declarations
SeedPairRecursion.lean 5 declarations
SeedPairStep.lean 3 declarations
SeedSharedKernel.lean 1 declarations
SeedSharedPairEvaluation.lean 1 declarations
SimpleFieldComparison.lean 3 declarations
SimpleFieldData.lean 13 declarations
SimpleFieldTransport.lean 2 declarations
SpinCountMagnetization.lean 4 declarations
SpinCoverError.lean 2 declarations
SpinCoverParameters.lean 1 declarations
SpinFactorization.lean 3 declarations
SpinFiniteCover.lean 3 declarations
SpinFiniteCoverMean.lean 1 declarations
SpinGroupCountVariance.lean 7 declarations
SpinGroupFieldPressure.lean 2 declarations
SpinGroupProjection.lean 5 declarations
SpinGroupProjectionMoment.lean 4 declarations
SpinGroupSlice.lean 9 declarations
SpinGroupSliceComparison.lean 4 declarations
SpinHammingBall.lean 5 declarations
SpinHammingEnergy.lean 4 declarations
SpinPairSubGaussian.lean 5 declarations
SpinPriorArrayDiagonal.lean 5 declarations
SpinPriorArrayDiagonalWard.lean 2 declarations
SpinPriorArrayLaw.lean 2 declarations
SpinPriorArrayResidual.lean 1 declarations
SpinPriorArrayResidualBound.lean 1 declarations
SpinPriorArrayWard.lean 3 declarations
SpinPriorCascadeAverage.lean 3 declarations
SpinPriorCascadePressure.lean 9 declarations
SpinPriorContact.lean 4 declarations
SpinPriorContactContradiction.lean 1 declarations
SpinPriorContactField.lean 3 declarations
SpinPriorContactGG.lean 1 declarations
SpinPriorContactMinimum.lean 7 declarations
SpinPriorContactNoSequence.lean 1 declarations
SpinPriorContactTailOrder.lean 1 declarations
SpinPriorContactTemperature.lean 2 declarations
SpinPriorDiagonalMinimum.lean 1 declarations
SpinPriorDiagonalStatistics.lean 3 declarations
SpinPriorEnergyLimit.lean 4 declarations
SpinPriorExponential.lean 1 declarations
SpinPriorFieldDerivative.lean 4 declarations
SpinPriorFieldDerivativeMean.lean 3 declarations
SpinPriorFieldInsertionLaw.lean 5 declarations
SpinPriorFieldMean.lean 2 declarations
SpinPriorFieldRecursion.lean 3 declarations
SpinPriorFieldTailBridge.lean 1 declarations
SpinPriorFiniteGG.lean 6 declarations
SpinPriorFlatLaw.lean 5 declarations
SpinPriorFlatVariance.lean 4 declarations
SpinPriorFrozenCGF.lean 3 declarations
SpinPriorFrozenGibbs.lean 2 declarations
SpinPriorFrozenReference.lean 4 declarations
SpinPriorGGMinimum.lean 1 declarations
SpinPriorGaussianMinimum.lean 2 declarations
SpinPriorGeometricLimit.lean 3 declarations
SpinPriorHaarMean.lean 1 declarations
SpinPriorHaarVariance.lean 1 declarations
SpinPriorKernelDiagonal.lean 2 declarations
SpinPriorLabeledMoments.lean 5 declarations
SpinPriorLeafTail.lean 8 declarations
SpinPriorLimitingDiagonal.lean 1 declarations
SpinPriorLimitingGG.lean 2 declarations
SpinPriorMinimumBounds.lean 1 declarations
SpinPriorMinimumCoordinates.lean 4 declarations
SpinPriorMinimumFluctuations.lean 1 declarations
SpinPriorObservableAverageLaw.lean 4 declarations
SpinPriorPerturbationCost.lean 3 declarations
SpinPriorPerturbationVariance.lean 1 declarations
SpinPriorPhysicalPressure.lean 3 declarations
SpinPriorPrincipalWard.lean 2 declarations
SpinPriorProfileVariance.lean 1 declarations
SpinPriorReplicaAverage.lean 3 declarations
SpinPriorReplicaMixture.lean 1 declarations
SpinPriorRestrictedAsymptotic.lean 1 declarations
SpinPriorRestrictedBoundary.lean 2 declarations
SpinPriorRestrictedCap.lean 4 declarations
SpinPriorRestrictedEntropyLimit.lean 1 declarations
SpinPriorRootVariance.lean 2 declarations
SpinPriorTemperatureCGF.lean 2 declarations
SpinPriorTemperatureDerivative.lean 2 declarations
SpinPriorTreeGeometry.lean 5 declarations
SpinPriorWardLimits.lean 1 declarations
SpinProjectionEntropy.lean 3 declarations
SpinProjectionTrial.lean 1 declarations
SpinSliceComparison.lean 3 declarations
SpinSliceProjection.lean 12 declarations
VectorGaussianTransition.lean 8 declarations
VectorLabeledNoiseTransport.lean 1 declarations
VectorLabeledPairLaw.lean 1 declarations
VectorLabeledSeedTransport.lean 1 declarations
VectorPairIntegral.lean 3 declarations
VectorTerminalCascade.lean 10 declarations
VectorTerminalLabeled.lean 7 declarations
VectorTerminalNoise.lean 8 declarations
VectorTerminalSeed.lean 1 declarations
VectorTerminalShift.lean 3 declarations
VectorTerminalTransition.lean 3 declarations
VectorTransitionEntropy.lean 1 declarations
VectorTransitionShift.lean 2 declarations
VectorTransitionZero.lean 1 declarations
ZeroFieldPopulations.lean 5 declarations