`OAI/Probability/InvariantIsing/Arrays/`

1007 declarations, 0 contain sorry, 0 declared as axioms; 188 files

Files

BlockWard.lean 6 declarations
CoordinatePairData.lean 2 declarations
CoordinateReplicaAncestry.lean 1 declarations
CoordinateWard.lean 11 declarations
CountableReplicaRestriction.lean 3 declarations
CountableWardFunctional.lean 3 declarations
CountableWardMixture.lean 4 declarations
CountableWardSubtype.lean 1 declarations
DiagonalCovariance.lean 3 declarations
FullPerturbationCost.lean 4 declarations
FullPerturbationMinima.lean 3 declarations
FullPerturbationVariance.lean 1 declarations
MonomialEnumeration.lean 9 declarations
NSpinCascade.lean 13 declarations
NSpinCascadeFluctuation.lean 1 declarations
NSpinComparison.lean 3 declarations
NSpinConcentration.lean 4 declarations
NSpinFactorization.lean 6 declarations
NSpinTensorAncestorInput.lean 8 declarations
NSpinTensorBackwardDerivative.lean 13 declarations
NSpinTensorBackwardPaths.lean 11 declarations
NSpinTensorCascade.lean 24 declarations
NSpinTensorComparison.lean 3 declarations
NSpinTensorFlatLaw.lean 9 declarations
NSpinTensorFlatMean.lean 9 declarations
NSpinTensorFluctuation.lean 4 declarations
NSpinTensorFrozen.lean 22 declarations
NSpinTensorFrozenCGF.lean 14 declarations
NSpinTensorFrozenFluctuation.lean 13 declarations
NSpinTensorGaussianLaw.lean 17 declarations
NSpinTensorHaar.lean 1 declarations
NSpinTensorHaarFluctuation.lean 7 declarations
NSpinTensorLabeled.lean 28 declarations
NSpinTensorPairConditioning.lean 17 declarations
NSpinTensorPairPaths.lean 19 declarations
NSpinTensorProjectedBackward.lean 21 declarations
NSpinTensorRetained.lean 20 declarations
NSpinTensorRootVariance.lean 12 declarations
NSpinTensorTerminalDerivative.lean 13 declarations
NSpinVariance.lean 3 declarations
OffDiagonalWard.lean 5 declarations
OverlapBounds.lean 5 declarations
OverlapPathCompact.lean 8 declarations
OverlapTestDiagonal.lean 5 declarations
OverlapTestSeparation.lean 1 declarations
OverlapTestTransport.lean 3 declarations
Overlaps.lean 6 declarations
PathSymbolAEUniqueness.lean 3 declarations
PathSymbolCongruence.lean 2 declarations
PathSymbolUniqueness.lean 2 declarations
PerturbationFeatures.lean 17 declarations
PerturbationMeasurability.lean 8 declarations
PerturbationMinimumRates.lean 3 declarations
PerturbationWeights.lean 9 declarations
QuantileProductKernel.lean 3 declarations
QuantileProductPath.lean 4 declarations
QuantileReplicaProduct.lean 2 declarations
QuantizedFieldPressure.lean 1 declarations
ReplicaContractions.lean 9 declarations
ReplicaCovariance.lean 1 declarations
ReplicaPairLaw.lean 3 declarations
ReplicaProductContinuity.lean 11 declarations
ReplicaProductPrimitives.lean 5 declarations
ReplicaProductRoots.lean 2 declarations
ReplicaProductSymbols.lean 1 declarations
ReplicaPushforward.lean 1 declarations
ReplicaWardPaths.lean 8 declarations
TensorAmplitudeComparison.lean 5 declarations
TensorAncestorRandomization.lean 1 declarations
TensorArrayDiagonal.lean 5 declarations
TensorArrayDiagonalWard.lean 7 declarations
TensorArrayGeometry.lean 3 declarations
TensorArrayLaw.lean 9 declarations
TensorArrayResidual.lean 3 declarations
TensorArrayWard.lean 5 declarations
TensorCascadeDiagonalWard.lean 2 declarations
TensorCascadeReplicaAverage.lean 4 declarations
TensorCascadeWard.lean 1 declarations
TensorCoefficientDerivative.lean 31 declarations
TensorContactAsymptotic.lean 1 declarations
TensorContactBoundary.lean 2 declarations
TensorContactCap.lean 3 declarations
TensorContactContinuity.lean 4 declarations
TensorContactContradiction.lean 1 declarations
TensorContactField.lean 3 declarations
TensorContactGG.lean 1 declarations
TensorContactMinimum.lean 5 declarations
TensorContactNoSequence.lean 1 declarations
TensorContactRegion.lean 6 declarations
TensorContactStep.lean 5 declarations
TensorContactTailOrder.lean 1 declarations
TensorContactTemperature.lean 2 declarations
TensorContactZeroBoundary.lean 1 declarations
TensorCoordinateMinimum.lean 4 declarations
TensorCountableDiagonalWard.lean 2 declarations
TensorCountableHamiltonian.lean 1 declarations
TensorCountableWard.lean 2 declarations
TensorDiagonalCGF.lean 9 declarations
TensorDiagonalError.lean 3 declarations
TensorDiagonalMinimum.lean 1 declarations
TensorDiagonalPrincipalObservables.lean 16 declarations
TensorDiagonalPrincipalWard.lean 8 declarations
TensorDiagonalWardCorrectionBound.lean 4 declarations
TensorDiagonalWardLimit.lean 2 declarations
TensorDiagonalWardMeasurability.lean 7 declarations
TensorEnergyLimit.lean 1 declarations
TensorEnvelopeLower.lean 1 declarations
TensorFieldDerivative.lean 10 declarations
TensorFieldDerivativeIntegrability.lean 9 declarations
TensorFieldDerivativeLaw.lean 8 declarations
TensorFieldDerivativeMean.lean 3 declarations
TensorFieldModulus.lean 2 declarations
TensorFieldTailBridge.lean 4 declarations
TensorFiniteGG.lean 6 declarations
TensorFiniteWard.lean 10 declarations
TensorFixedMinimumLimit.lean 1 declarations
TensorFrozenGibbs.lean 2 declarations
TensorGGExistence.lean 1 declarations
TensorGGMinimum.lean 1 declarations
TensorGGRate.lean 2 declarations
TensorGaussianMean.lean 3 declarations
TensorGrowingDepthDiagonal.lean 1 declarations
TensorGrowingDepthGG.lean 1 declarations
TensorGrowingDepthSelection.lean 1 declarations
TensorGrowingDiagonalWard.lean 1 declarations
TensorGrowingGeometricLimit.lean 1 declarations
TensorGrowingPerturbedWard.lean 1 declarations
TensorGrowingWard.lean 1 declarations
TensorHaarWard.lean 7 declarations
TensorKernelDiagonalError.lean 3 declarations
TensorLabeledAncestry.lean 1 declarations
TensorLabeledNoiseTransport.lean 2 declarations
TensorLabeledSeedTransport.lean 1 declarations
TensorLabeledTerminal.lean 5 declarations
TensorLeafCoefficients.lean 5 declarations
TensorLeafTail.lean 6 declarations
TensorLimitExistence.lean 1 declarations
TensorLimitingDiagonal.lean 2 declarations
TensorLimitingGG.lean 3 declarations
TensorMarkPairRecursion.lean 1 declarations
TensorMinimizerArrayGG.lean 1 declarations
TensorMinimizerDiagonal.lean 1 declarations
TensorMinimumFluctuations.lean 1 declarations
TensorMinimumIncrement.lean 1 declarations
TensorMinimumPenalty.lean 5 declarations
TensorMinimumPressure.lean 2 declarations
TensorMinimumSequence.lean 1 declarations
TensorObjectiveContinuity.lean 7 declarations
TensorObservableAverageLaw.lean 5 declarations
TensorPairInput.lean 1 declarations
TensorPerturbationBaseComparison.lean 1 declarations
TensorPerturbationCGF.lean 1 declarations
TensorPerturbationComparison.lean 2 declarations
TensorPerturbationCost.lean 6 declarations
TensorPerturbationObjective.lean 4 declarations
TensorPerturbationVariance.lean 2 declarations
TensorPerturbedWardLimit.lean 1 declarations
TensorPrincipalBlock.lean 7 declarations
TensorPrincipalObservables.lean 14 declarations
TensorPrincipalWard.lean 10 declarations
TensorProfiles.lean 10 declarations
TensorReplicaAverageLaw.lean 4 declarations
TensorRetainedSeedLaw.lean 1 declarations
TensorRotationCovariance.lean 2 declarations
TensorSeedPairLaw.lean 1 declarations
TensorSeedReplicaTransport.lean 1 declarations
TensorSingleObservable.lean 2 declarations
TensorSiteComparison.lean 2 declarations
TensorSiteMean.lean 1 declarations
TensorSpectralGGExistence.lean 1 declarations
TensorSpectralIdentification.lean 1 declarations
TensorTemperatureCGF.lean 4 declarations
TensorTemperatureDerivative.lean 1 declarations
TensorTemperatureModulus.lean 4 declarations
TensorTerminalReplicaTransport.lean 3 declarations
TensorTiltedPairIntegral.lean 1 declarations
TensorTreeLevels.lean 5 declarations
TensorTruncatedDiagonalWard.lean 9 declarations
TensorTruncatedWard.lean 12 declarations
TensorWardCorrectionBound.lean 15 declarations
TensorWardError.lean 21 declarations
TensorWardLimit.lean 1 declarations
TensorWardMeasurability.lean 13 declarations
TensorWardReplica.lean 9 declarations
TensorZeroAmplitude.lean 12 declarations
TensorZeroFieldPressure.lean 10 declarations
TripleContractions.lean 7 declarations
UltrametricProduct.lean 8 declarations