`OAI/Probability/InvariantIsing/Magnetic/`

1210 declarations, 0 contain sorry, 0 declared as axioms; 390 files

Files

ConstrainedBlockBias.lean 4 declarations
ConstrainedBlockMagneticEstimate.lean 5 declarations
MagneticAdjacentCurvature.lean 3 declarations
MagneticAdjacentSquare.lean 1 declarations
MagneticAffineFieldLower.lean 1 declarations
MagneticAffineIncrementLower.lean 2 declarations
MagneticAffinePressureLower.lean 1 declarations
MagneticAffineTemplateLower.lean 1 declarations
MagneticBiasEndpoint.lean 5 declarations
MagneticBlockConvergence.lean 1 declarations
MagneticBlockDiagonalLower.lean 1 declarations
MagneticBlockError.lean 5 declarations
MagneticBlockL1Consistency.lean 1 declarations
MagneticBlockModulus.lean 2 declarations
MagneticBlockPath.lean 6 declarations
MagneticBlockPathConvergence.lean 1 declarations
MagneticBlockTerminalLoss.lean 4 declarations
MagneticBlockTrialLower.lean 1 declarations
MagneticBoundaryContinuity.lean 7 declarations
MagneticBoundedInverseComparison.lean 1 declarations
MagneticCanonicalSpin.lean 7 declarations
MagneticCenteredMoments.lean 14 declarations
MagneticClosedLipschitz.lean 1 declarations
MagneticClosedSupport.lean 1 declarations
MagneticCoerciveRoot.lean 1 declarations
MagneticCompactPartition.lean 2 declarations
MagneticCompactSpectrum.lean 1 declarations
MagneticConstrainedPressureLower.lean 1 declarations
MagneticConstrainedUpper.lean 1 declarations
MagneticConstrainedVariationalUpper.lean 1 declarations
MagneticContinuationClosed.lean 5 declarations
MagneticContinuationClosedPDE.lean 7 declarations
MagneticContinuationComparison.lean 1 declarations
MagneticContinuationEndpoint.lean 11 declarations
MagneticContinuationGenerator.lean 5 declarations
MagneticContinuationIBP.lean 1 declarations
MagneticContinuationInverse.lean 9 declarations
MagneticContinuationJet.lean 3 declarations
MagneticContinuationPDE.lean 6 declarations
MagneticContinuationRegular.lean 11 declarations
MagneticContinuationSpatial.lean 4 declarations
MagneticContinuationTime.lean 3 declarations
MagneticContinuationTwoJet.lean 3 declarations
MagneticConvergingFieldUpper.lean 1 declarations
MagneticConvergingUpper.lean 1 declarations
MagneticConvergingVariationalUpper.lean 1 declarations
MagneticCountTemplateLower.lean 1 declarations
MagneticCouplingField.lean 2 declarations
MagneticCoverDistance.lean 1 declarations
MagneticCurvatureBound.lean 5 declarations
MagneticCurvatureEndpoint.lean 6 declarations
MagneticCurvatureLower.lean 9 declarations
MagneticDerivativeLimit.lean 2 declarations
MagneticDiagonalL1Consistency.lean 1 declarations
MagneticDiagonalSelection.lean 1 declarations
MagneticEntropyMaximum.lean 3 declarations
MagneticEntropySequence.lean 2 declarations
MagneticFamilyDerivative.lean 2 declarations
MagneticFieldBias.lean 5 declarations
MagneticFieldBounds.lean 6 declarations
MagneticFieldCurvature.lean 8 declarations
MagneticFieldExtension.lean 3 declarations
MagneticFieldFamily.lean 7 declarations
MagneticFieldGradient.lean 7 declarations
MagneticFieldHeightDerivative.lean 5 declarations
MagneticFieldHeightHessian.lean 3 declarations
MagneticFieldInverse.lean 7 declarations
MagneticFieldInverseConvex.lean 5 declarations
MagneticFieldLevels.lean 13 declarations
MagneticFieldLowerBound.lean 4 declarations
MagneticFieldMinimum.lean 12 declarations
MagneticFieldParameter.lean 5 declarations
MagneticFieldPopulationLower.lean 1 declarations
MagneticFieldRadial.lean 3 declarations
MagneticFieldSubsequenceLower.lean 1 declarations
MagneticFieldSymmetry.lean 7 declarations
MagneticFiniteAlphabet.lean 1 declarations
MagneticFiniteFourth.lean 5 declarations
MagneticFiniteLawExtension.lean 3 declarations
MagneticFinitePopulationLimit.lean 1 declarations
MagneticFiniteTemplateLimit.lean 1 declarations
MagneticFiniteTemplateLower.lean 1 declarations
MagneticFiniteTrial.lean 1 declarations
MagneticFiniteType.lean 1 declarations
MagneticFourJet.lean 9 declarations
MagneticFourthCumulant.lean 1 declarations
MagneticFullFieldUpper.lean 1 declarations
MagneticGaussianCovariance.lean 4 declarations
MagneticGaussianLaplace.lean 6 declarations
MagneticGaussianMoments.lean 3 declarations
MagneticGaussianSmoothing.lean 3 declarations
MagneticGeneralSpectrum.lean 1 declarations
MagneticGridProjection.lean 3 declarations
MagneticGroupAverage.lean 5 declarations
MagneticGroupConsistency.lean 1 declarations
MagneticGroupEntropyLimit.lean 1 declarations
MagneticGroupInterior.lean 1 declarations
MagneticGroupParameterBound.lean 3 declarations
MagneticGroupPath.lean 6 declarations
MagneticGroupRounding.lean 2 declarations
MagneticGroupSupport.lean 3 declarations
MagneticHeatContinuity.lean 5 declarations
MagneticHeatCurvature.lean 3 declarations
MagneticHeatInverse.lean 3 declarations
MagneticHeatJetContinuity.lean 3 declarations
MagneticHeatMean.lean 4 declarations
MagneticHeatSecond.lean 3 declarations
MagneticHeatSpatial.lean 3 declarations
MagneticHeatWeighted.lean 3 declarations
MagneticHeightConcavity.lean 1 declarations
MagneticHeightLipschitz.lean 3 declarations
MagneticHeightLists.lean 8 declarations
MagneticHeightOrder.lean 5 declarations
MagneticHeightSupport.lean 2 declarations
MagneticImplicitBias.lean 3 declarations
MagneticInverseComparison.lean 1 declarations
MagneticInverseCurvature.lean 15 declarations
MagneticInverseGenerator.lean 3 declarations
MagneticInverseVariation.lean 5 declarations
MagneticInwardApproximation.lean 5 declarations
MagneticJetProduct.lean 2 declarations
MagneticL1.lean 4 declarations
MagneticLevelDerivative.lean 5 declarations
MagneticLevelModulus.lean 4 declarations
MagneticLimitingPressure.lean 1 declarations
MagneticMainPressure.lean 1 declarations
MagneticMeanShift.lean 3 declarations
MagneticMinimumCalculus.lean 3 declarations
MagneticOffDiagonalHessian.lean 6 declarations
MagneticPairComparison.lean 2 declarations
MagneticPairConvergence.lean 2 declarations
MagneticParabolicComparison.lean 1 declarations
MagneticParabolicMinimum.lean 1 declarations
MagneticParabolicNegative.lean 2 declarations
MagneticPartitionContinuity.lean 1 declarations
MagneticPartitionSupport.lean 7 declarations
MagneticPhysicalFieldUpper.lean 1 declarations
MagneticPhysicalIncrementLower.lean 1 declarations
MagneticPhysicalMean.lean 1 declarations
MagneticPopulationContinuity.lean 2 declarations
MagneticPopulationCoupling.lean 4 declarations
MagneticPrefixComparison.lean 4 declarations
MagneticRadialHessian.lean 2 declarations
MagneticRationalBlockLower.lean 1 declarations
MagneticRationalCover.lean 2 declarations
MagneticRationalIncrementLower.lean 2 declarations
MagneticRationalTemplateLower.lean 1 declarations
MagneticRealProfile.lean 1 declarations
MagneticRefinement.lean 9 declarations
MagneticRelativeFourth.lean 3 declarations
MagneticRelativeThird.lean 8 declarations
MagneticResidueSelection.lean 2 declarations
MagneticRoundedCount.lean 6 declarations
MagneticRoundedFieldUpper.lean 1 declarations
MagneticScalarContinuation.lean 3 declarations
MagneticScalarFourJet.lean 5 declarations
MagneticScalarFourth.lean 7 declarations
MagneticScalarInverse.lean 5 declarations
MagneticScalarSlab.lean 10 declarations
MagneticScalarSlabEndpoint.lean 7 declarations
MagneticScalarThird.lean 7 declarations
MagneticScalarWeightedPDE.lean 8 declarations
MagneticScaledBounds.lean 3 declarations
MagneticScaledContinuation.lean 10 declarations
MagneticScaledCurvatureOrder.lean 2 declarations
MagneticScaledInitial.lean 3 declarations
MagneticScaledSlab.lean 15 declarations
MagneticScaledSquareOrder.lean 2 declarations
MagneticSlabBoundary.lean 7 declarations
MagneticSlabClosedDerivatives.lean 10 declarations
MagneticSlabCoefficient.lean 3 declarations
MagneticSlabContinuation.lean 9 declarations
MagneticSlabEndpoint.lean 2 declarations
MagneticSlabExponentOrder.lean 1 declarations
MagneticSlabInitial.lean 4 declarations
MagneticSlabPDE.lean 10 declarations
MagneticSlabZero.lean 3 declarations
MagneticSliceFieldBound.lean 2 declarations
MagneticSpatialFourth.lean 11 declarations
MagneticSpatialThird.lean 6 declarations
MagneticSpectralClipping.lean 1 declarations
MagneticSpectralContinuity.lean 3 declarations
MagneticSpectralPartition.lean 1 declarations
MagneticSpectralPopulationLower.lean 1 declarations
MagneticSquareInitial.lean 4 declarations
MagneticSquareInverseConvex.lean 4 declarations
MagneticSquareJet.lean 4 declarations
MagneticSquareSlabConvex.lean 2 declarations
MagneticStationaryFamily.lean 1 declarations
MagneticTailComparison.lean 2 declarations
MagneticTailCongruence.lean 7 declarations
MagneticTemplateFullLower.lean 1 declarations
MagneticTemplateLower.lean 1 declarations
MagneticTerminalCongruence.lean 6 declarations
MagneticTerminalOrder.lean 2 declarations
MagneticThresholdDiagonal.lean 1 declarations
MagneticTrialApproximation.lean 3 declarations
MagneticTrialBarrier.lean 1 declarations
MagneticTrialLimit.lean 2 declarations
MagneticTwoJetSpatial.lean 2 declarations
MagneticUniformSlabBounds.lean 11 declarations
MagneticVariational.lean 14 declarations
MagneticVariationalBounds.lean 3 declarations
MagneticVariationalContinuity.lean 4 declarations
MagneticVariationalTransport.lean 1 declarations
MagneticWassersteinMain.lean 1 declarations
MagneticWassersteinMean.lean 1 declarations
MagneticWassersteinPhysical.lean 1 declarations
MagneticWassersteinPressure.lean 1 declarations
MagneticWeightedBoundary.lean 4 declarations
MagneticWeightedClosed.lean 8 declarations
MagneticWeightedGenerator.lean 4 declarations
MagneticWeightedInitial.lean 5 declarations
MagneticWeightedJet.lean 8 declarations
MagneticWeightedNonnegative.lean 2 declarations
MagneticWeightedPosition.lean 3 declarations
MagneticWeightedSpatial.lean 11 declarations
MagneticZeroPopulationLimit.lean 1 declarations
RationalConstrainedMinima.lean 1 declarations
RationalMagnetizationCounts.lean 1 declarations
RestrictedAncestorEndpoint.lean 3 declarations
RestrictedBaseCutoffLaw.lean 1 declarations
RestrictedBaseCutoffProduct.lean 1 declarations
RestrictedBaseRawCutoff.lean 1 declarations
RestrictedBlockConsistency.lean 5 declarations
RestrictedBlockMeasurability.lean 2 declarations
RestrictedBlockOverlap.lean 4 declarations
RestrictedBlockSpinEvaluation.lean 6 declarations
RestrictedCanonicalCappedLog.lean 1 declarations
RestrictedCanonicalGroupCutoff.lean 1 declarations
RestrictedCanonicalHaarLog.lean 3 declarations
RestrictedCanonicalLaw.lean 1 declarations
RestrictedCanonicalLogCoefficients.lean 1 declarations
RestrictedCanonicalLogIntegrability.lean 4 declarations
RestrictedCanonicalLogLaw.lean 1 declarations
RestrictedCanonicalLogLimit.lean 1 declarations
RestrictedCanonicalTreeLogLaw.lean 1 declarations
RestrictedCanonicalWeighted.lean 1 declarations
RestrictedCompressionCappedLog.lean 1 declarations
RestrictedCompressionLogLimit.lean 1 declarations
RestrictedConcentration.lean 1 declarations
RestrictedConstantHaarLog.lean 1 declarations
RestrictedCoordinateAverage.lean 2 declarations
RestrictedCoordinateOverlap.lean 5 declarations
RestrictedCubeIncrement.lean 1 declarations
RestrictedCutoffMap.lean 1 declarations
RestrictedDepthPair.lean 7 declarations
RestrictedDepthTestEvaluation.lean 1 declarations
RestrictedDisorderTest.lean 5 declarations
RestrictedEndpointKernel.lean 6 declarations
RestrictedEndpointTest.lean 8 declarations
RestrictedEnvelopeLower.lean 1 declarations
RestrictedFieldEndpointLoss.lean 3 declarations
RestrictedFieldFactorization.lean 4 declarations
RestrictedFieldLogNormalizer.lean 7 declarations
RestrictedFieldOrder.lean 3 declarations
RestrictedFieldPairInput.lean 3 declarations
RestrictedFieldPublishedInput.lean 4 declarations
RestrictedFieldRecursion.lean 7 declarations
RestrictedFieldRootLoss.lean 3 declarations
RestrictedFieldStepEntropy.lean 1 declarations
RestrictedFieldStepLoss.lean 3 declarations
RestrictedFieldTerminal.lean 11 declarations
RestrictedFiniteBlockSpin.lean 1 declarations
RestrictedFiniteDepthTest.lean 1 declarations
RestrictedFiniteLabeledLog.lean 1 declarations
RestrictedFiniteLogEvaluation.lean 1 declarations
RestrictedFiniteModelDepth.lean 1 declarations
RestrictedFiniteModelSpin.lean 1 declarations
RestrictedFiniteNormalizedSpin.lean 1 declarations
RestrictedFiniteSpinTest.lean 1 declarations
RestrictedFiniteTrialLower.lean 1 declarations
RestrictedFixedMinimumLimit.lean 1 declarations
RestrictedFrameLogBound.lean 1 declarations
RestrictedFullSpinAverage.lean 2 declarations
RestrictedFullSpinTest.lean 1 declarations
RestrictedFullTail.lean 4 declarations
RestrictedFullTest.lean 1 declarations
RestrictedFullTreeCutoff.lean 1 declarations
RestrictedGeometricMean.lean 3 declarations
RestrictedGeometricTail.lean 1 declarations
RestrictedGeometricWeightedTest.lean 1 declarations
RestrictedGroupedCappedLog.lean 1 declarations
RestrictedGroupedCutoff.lean 1 declarations
RestrictedGroupedWeighted.lean 1 declarations
RestrictedHaarCoefficients.lean 1 declarations
RestrictedHaarCutoffComparison.lean 1 declarations
RestrictedHaarCutoffLimit.lean 1 declarations
RestrictedHaarFiniteOverlap.lean 1 declarations
RestrictedHaarFiniteSpin.lean 1 declarations
RestrictedHaarLogIncrement.lean 1 declarations
RestrictedHaarLogObservable.lean 3 declarations
RestrictedHaarSymmetry.lean 1 declarations
RestrictedKernelFactorization.lean 3 declarations
RestrictedKernelShift.lean 2 declarations
RestrictedLeafConditioning.lean 3 declarations
RestrictedLinearCoordinate.lean 3 declarations
RestrictedLinearDepthEvaluation.lean 3 declarations
RestrictedLinearNoiseDepth.lean 2 declarations
RestrictedLinearNoiseEvaluation.lean 2 declarations
RestrictedLinearSpinEvaluation.lean 3 declarations
RestrictedLogMap.lean 4 declarations
RestrictedMinimumPressure.lean 2 declarations
RestrictedOrientationLog.lean 2 declarations
RestrictedOriginalComparison.lean 1 declarations
RestrictedOriginalCutoff.lean 1 declarations
RestrictedOriginalFullComparison.lean 1 declarations
RestrictedOriginalFullOverlap.lean 1 declarations
RestrictedOriginalFullSpin.lean 1 declarations
RestrictedOriginalGroupLimit.lean 1 declarations
RestrictedOriginalHaarLimit.lean 1 declarations
RestrictedOriginalOverlapLimit.lean 1 declarations
RestrictedOriginalRadialCutoff.lean 1 declarations
RestrictedOriginalSpinLimit.lean 1 declarations
RestrictedOriginalTreeLimit.lean 1 declarations
RestrictedOriginalTreeRegular.lean 1 declarations
RestrictedOriginalWeightedComparison.lean 1 declarations
RestrictedPairEntropy.lean 1 declarations
RestrictedPairFactorization.lean 3 declarations
RestrictedPairMoments.lean 8 declarations
RestrictedPairOrder.lean 2 declarations
RestrictedPairRecursion.lean 4 declarations
RestrictedPairRootEntropy.lean 3 declarations
RestrictedPairSpinKernel.lean 2 declarations
RestrictedPairTies.lean 3 declarations
RestrictedPhysicalCavityHaar.lean 1 declarations
RestrictedPhysicalCutoff.lean 3 declarations
RestrictedPhysicalCutoffComparison.lean 1 declarations
RestrictedPhysicalGG.lean 1 declarations
RestrictedPhysicalGibbsSplit.lean 3 declarations
RestrictedPhysicalIncrement.lean 1 declarations
RestrictedPhysicalLogCoefficients.lean 1 declarations
RestrictedPhysicalLogLimit.lean 1 declarations
RestrictedPhysicalLogSplit.lean 1 declarations
RestrictedPhysicalOverlapCutoff.lean 1 declarations
RestrictedPhysicalProjectorIncrement.lean 1 declarations
RestrictedPhysicalSpinCutoff.lean 1 declarations
RestrictedPhysicalTrialLower.lean 1 declarations
RestrictedPressure.lean 7 declarations
RestrictedPressureFluctuation.lean 2 declarations
RestrictedPressureIncrement.lean 1 declarations
RestrictedPressureMean.lean 3 declarations
RestrictedPriorGaussianLaw.lean 4 declarations
RestrictedPriorIntegrability.lean 3 declarations
RestrictedPriorPressure.lean 2 declarations
RestrictedProductPrior.lean 7 declarations
RestrictedProjectorCavity.lean 3 declarations
RestrictedProjectorCoefficientError.lean 1 declarations
RestrictedProjectorCutoffLaw.lean 2 declarations
RestrictedProjectorHaarMean.lean 3 declarations
RestrictedProjectorLog.lean 3 declarations
RestrictedProjectorLogAverage.lean 1 declarations
RestrictedProjectorPartition.lean 3 declarations
RestrictedRandomHaarLog.lean 3 declarations
RestrictedRandomPressureIncrement.lean 1 declarations
RestrictedRandomTreeLogLaw.lean 1 declarations
RestrictedRootEvaluation.lean 2 declarations
RestrictedRootShift.lean 4 declarations
RestrictedRootedBlock.lean 4 declarations
RestrictedRotationArray.lean 2 declarations
RestrictedRotationCutoffWeight.lean 1 declarations
RestrictedRotationLogMean.lean 4 declarations
RestrictedRotationProbability.lean 5 declarations
RestrictedSpecialCutoffError.lean 1 declarations
RestrictedSpectrumEntropyUpper.lean 1 declarations
RestrictedSpectrumStepUpper.lean 1 declarations
RestrictedSpinBias.lean 3 declarations
RestrictedSpinEvaluation.lean 8 declarations
RestrictedSpinKernel.lean 4 declarations
RestrictedSpinLaw.lean 5 declarations
RestrictedSpinLog.lean 7 declarations
RestrictedSpinPrior.lean 6 declarations
RestrictedSpinReplacement.lean 2 declarations
RestrictedSpinSymmetry.lean 2 declarations
RestrictedSplitOverlapTest.lean 2 declarations
RestrictedSplitSpinTest.lean 1 declarations
RestrictedSplitTreeSpinTest.lean 1 declarations
RestrictedStrictFiniteOverlap.lean 2 declarations
RestrictedStrictFiniteSpin.lean 1 declarations
RestrictedTailEntropy.lean 1 declarations
RestrictedTailSpinKernel.lean 2 declarations
RestrictedTerminalIntegrability.lean 1 declarations
RestrictedTreeAverage.lean 1 declarations
RestrictedTreeCutoffMeasurability.lean 1 declarations
RestrictedTreeFullRegular.lean 2 declarations
RestrictedTreeLogIntegrability.lean 1 declarations
RestrictedTreeLogMeasurability.lean 3 declarations
RestrictedTreePressureIncrement.lean 1 declarations
RestrictedTreeRegular.lean 1 declarations
RestrictedZeroTreeArrayLaw.lean 4 declarations