OAI/Probability/InvariantIsing/Core/
253 declarations, 0 contain sorry, 0 declared as axioms; 58 files
Files
- AffineTemplateComparison.lean 1 declarations
- BoundedObservableMinimum.lean 3 declarations
- ConditionalRelativeEntropy.lean 1 declarations
- ContactModulus.lean 4 declarations
- CubeOperatorNorm.lean 3 declarations
- DenseFiniteMaximum.lean 7 declarations
- DenseFiniteMinimum.lean 7 declarations
- FiniteAlphabetPressure.lean 1 declarations
- FiniteFieldAtomMass.lean 5 declarations
- FiniteFieldLabels.lean 5 declarations
- FiniteFieldLawCoupling.lean 5 declarations
- FiniteFieldMatching.lean 3 declarations
- FiniteFieldMatchingBound.lean 2 declarations
- FiniteFieldTransport.lean 9 declarations
- FiniteGaussianMaximum.lean 3 declarations
- FiniteGaussianVariance.lean 4 declarations
- FiniteIndexCoupling.lean 4 declarations
- FiniteIndexDistribution.lean 5 declarations
- FiniteIndexMagnetic.lean 1 declarations
- FiniteMinmax.lean 6 declarations
- FiniteMinmaxBasic.lean 5 declarations
- FiniteOperatorDuality.lean 1 declarations
- FinitePopulationCoupling.lean 5 declarations
- FiniteProjectionTrial.lean 1 declarations
- FinitePushforwardEntropy.lean 6 declarations
- FiniteSpectrumStepUpper.lean 1 declarations
- FiniteSpectrumUpper.lean 1 declarations
- FiniteSpectrumVariationalUpper.lean 1 declarations
- FiniteSpinEntropy.lean 8 declarations
- FiniteSquareExtrema.lean 2 declarations
- FiniteTailOrder.lean 5 declarations
- FiniteTypePressure.lean 2 declarations
- FiniteVariationalBounds.lean 4 declarations
- FiniteWeightedCauchy.lean 3 declarations
- GGErrorAlgebra.lean 1 declarations
- InvariantOrbitLaw.lean 3 declarations
- KernelExponentialBound.lean 1 declarations
- KernelProductEntropy.lean 3 declarations
- KernelRelativeEntropy.lean 6 declarations
- LevyMapDistance.lean 1 declarations
- LogMeanLoss.lean 2 declarations
- MixedSpectralFeatures.lean 6 declarations
- Model.lean 22 declarations
- MultiplicityContinuity.lean 3 declarations
- PairGibbs.lean 10 declarations
- PairProductShuffle.lean 3 declarations
- PositiveRationalApproximation.lean 9 declarations
- ProductKernelSampling.lean 1 declarations
- ReferenceInfiniteReplicas.lean 1 declarations
- TailOrder.lean 6 declarations
- TiltedRelativeEntropy.lean 3 declarations
- TrialGridApproximation.lean 7 declarations
- UnitBilinearNorm.lean 5 declarations
- UnitInnerMaximum.lean 2 declarations
- UnitIntervalMomentUniqueness.lean 1 declarations
- UnrestrictedEndpointKernel.lean 4 declarations
- Variational.lean 23 declarations
- Ward.lean 6 declarations