OAI/Probability/ClassicalON/
1193 declarations, 0 contain sorry, 0 declared as axioms; 117 files
Files
- AmplitudeLaw.lean 23 declarations
- AmplitudeModular.lean 2 declarations
- AmplitudePartition.lean 11 declarations
- AmplitudeSplit.lean 6 declarations
- AnnulusBlocks.lean 5 declarations
- AnnulusCrossing.lean 8 declarations
- AnnulusCut.lean 7 declarations
- AnnulusLabels.lean 15 declarations
- AnnulusPartition.lean 6 declarations
- AnnulusResponse.lean 6 declarations
- AnnulusSmall.lean 4 declarations
- AssociationCore.lean 9 declarations
- AxisRotation.lean 10 declarations
- BlockGeometry.lean 24 declarations
- BlockKernel.lean 9 declarations
- BlockLocal.lean 1 declarations
- BlockOrbit.lean 11 declarations
- BlockReduction.lean 1 declarations
- BondAssociation.lean 1 declarations
- BondConnectivity.lean 3 declarations
- BondExpansion.lean 6 declarations
- BondLaw.lean 15 declarations
- BondMeanOrder.lean 6 declarations
- BondMoments.lean 2 declarations
- BondPin.lean 9 declarations
- BondSigns.lean 16 declarations
- BondSubspace.lean 10 declarations
- CenteredAnnulus.lean 2 declarations
- CoarseCodes.lean 13 declarations
- CoarseExponential.lean 4 declarations
- CoarseGeometry.lean 11 declarations
- CoarsePaths.lean 8 declarations
- CoarseTail.lean 6 declarations
- ComplexWard.lean 56 declarations
- CylindricalConfiguration.lean 11 declarations
- CylindricalFiber.lean 7 declarations
- CylindricalGeometry.lean 12 declarations
- CylindricalLaw.lean 10 declarations
- DiscreteReference.lean 2 declarations
- DyadicFourier.lean 11 declarations
- DyadicModes.lean 9 declarations
- DyadicSine.lean 11 declarations
- DyadicSums.lean 5 declarations
- EdgeOperators.lean 2 declarations
- ExpMoments.lean 4 declarations
- FamilyAlgebra.lean 12 declarations
- FamilyBound.lean 6 declarations
- FamilyEstimate.lean 4 declarations
- FamilyKernel.lean 17 declarations
- FamilyLower.lean 4 declarations
- FerromagneticMean.lean 8 declarations
- FinFKG.lean 5 declarations
- FiniteVolume.lean 161 declarations
- FourierOperator.lean 5 declarations
- GibbsCovariance.lean 2 declarations
- GibbsDerivative.lean 4 declarations
- GradientComplex.lean 21 declarations
- IsingGinibre.lean 12 declarations
- IsingPositive.lean 3 declarations
- IsingReference.lean 9 declarations
- JointBond.lean 10 declarations
- LatticeGeometry.lean 14 declarations
- LatticeModes.lean 9 declarations
- LatticeRadius.lean 19 declarations
- LatticeRestriction.lean 15 declarations
- Main.lean 2 declarations
- MatrixSquare.lean 6 declarations
- MixedWard.lean 32 declarations
- ModeBounds.lean 3 declarations
- ModeCommutator.lean 8 declarations
- ModeCosts.lean 9 declarations
- Model.lean 12 declarations
- MomentCone.lean 7 declarations
- ObservableBounds.lean 9 declarations
- OrthogonalAverage.lean 15 declarations
- PeriodicODE.lean 2 declarations
- PeriodicPartition.lean 1 declarations
- PinComparison.lean 6 declarations
- PinnedBlocks.lean 14 declarations
- PinnedBonds.lean 12 declarations
- PinnedCylinder.lean 7 declarations
- PinnedReference.lean 11 declarations
- PinnedSigns.lean 4 declarations
- PlanarAlgebra.lean 15 declarations
- PlanarGinibre.lean 5 declarations
- PlanarPositive.lean 4 declarations
- PoleCrossing.lean 8 declarations
- PositiveKernel.lean 1 declarations
- PotentialRotation.lean 10 declarations
- ProductFKG.lean 6 declarations
- ProductGrouping.lean 6 declarations
- ProductMoments.lean 3 declarations
- ProfileEstimates.lean 7 declarations
- RawBond.lean 9 declarations
- ReindexIntegral.lean 2 declarations
- ResponseTransfer.lean 11 declarations
- RotationInequality.lean 9 declarations
- RotationWork.lean 24 declarations
- SecondBound.lean 6 declarations
- SecondGauge.lean 9 declarations
- SeparatedAnnuli.lean 6 declarations
- SignedSigns.lean 14 declarations
- SmoothBounds.lean 7 declarations
- SmoothProfiles.lean 26 declarations
- SpinBondKernel.lean 10 declarations
- SpinBonds.lean 5 declarations
- SpinCorrelation.lean 8 declarations
- SpinIsotropy.lean 8 declarations
- SpinReindex.lean 7 declarations
- SquareEstimates.lean 5 declarations
- ThetaEstimates.lean 4 declarations
- TorusDouble.lean 11 declarations
- TorusFourier.lean 14 declarations
- UpperEndpoint.lean 9 declarations
- WeightedLinear.lean 6 declarations
- WeightedProduct.lean 1 declarations
- WeightedTilt.lean 7 declarations