OAI/Probability/FreeIsing/Ising/
726 declarations, 0 contain sorry, 0 declared as axioms; 119 files
Files
- ActualVarianceAnalysis.lean 2 declarations
- ArtanhConstruction.lean 1 declarations
- CanonicalArtanh.lean 9 declarations
- CanonicalArtanhDenseIdentification.lean 2 declarations
- CanonicalArtanhIdentification.lean 3 declarations
- CanonicalClippedWeight.lean 7 declarations
- CanonicalContinuousFields.lean 7 declarations
- CanonicalCoordinateIdentification.lean 2 declarations
- CanonicalCovarianceIntegrals.lean 1 declarations
- CanonicalCovariancePullback.lean 6 declarations
- CanonicalDriftRegularity.lean 6 declarations
- CanonicalFieldNaturality.lean 3 declarations
- CanonicalIntegralRepresentation.lean 3 declarations
- CanonicalLocalSquare.lean 4 declarations
- CanonicalMartingales.lean 9 declarations
- CanonicalNormalizedField.lean 2 declarations
- CanonicalPosteriorStops.lean 22 declarations
- CanonicalResponseIntegrals.lean 2 declarations
- CavityTailTransport.lean 5 declarations
- CommonStopBounds.lean 9 declarations
- ConditionalCopyBounds.lean 18 declarations
- ContinuousCopyCoefficients.lean 20 declarations
- ContinuousCopyDensity.lean 17 declarations
- ContinuousCovarianceIntegral.lean 2 declarations
- ContinuousPosterior.lean 3 declarations
- ContinuousResponseAlgebra.lean 11 declarations
- ContinuousResponseEnergy.lean 9 declarations
- ContinuousRootResponse.lean 14 declarations
- CoordinateCompletion.lean 1 declarations
- CoordinateIntegrals.lean 6 declarations
- CopiedDriftDecomposition.lean 2 declarations
- CopyBrownian.lean 8 declarations
- CopyCanonicalStops.lean 10 declarations
- CopyCavityBounds.lean 4 declarations
- CopyCriticalSpatialBounds.lean 3 declarations
- CopyCriticalSpatialEstimates.lean 1 declarations
- CopyEdgeCorrelations.lean 4 declarations
- CopyEdgeVariance.lean 4 declarations
- CopyEnergyIntegrability.lean 13 declarations
- CopyFixedPathBound.lean 6 declarations
- CopyGeodesicCorrelations.lean 11 declarations
- CopyInformationBound.lean 6 declarations
- CopyIntegralLimits.lean 4 declarations
- CopyLinearLongBound.lean 3 declarations
- CopyMartingaleImmersion.lean 7 declarations
- CopyNoiseLongBound.lean 1 declarations
- CopyObservables.lean 12 declarations
- CopyOrbitAverage.lean 5 declarations
- CopyPathBounds.lean 12 declarations
- CopyPathVariance.lean 5 declarations
- CopyPathVector.lean 2 declarations
- CopyPathWeightNaturality.lean 6 declarations
- CopyProductDrift.lean 2 declarations
- CopyProductPathBound.lean 3 declarations
- CopyProductVariance.lean 3 declarations
- CopyResponseIdentification.lean 6 declarations
- CopyResponseRowPaths.lean 7 declarations
- CopyResponseRowSummability.lean 6 declarations
- CopyShellEnergies.lean 10 declarations
- CopySmallLogLoss.lean 8 declarations
- CopySmallTime.lean 8 declarations
- CopySpatialEndpoints.lean 3 declarations
- CopySpectral.lean 11 declarations
- CopySquareDensity.lean 7 declarations
- CopyStationarity.lean 11 declarations
- CopyStoppedEnergy.lean 3 declarations
- CopyStrictComparison.lean 2 declarations
- CopyVarianceContinuity.lean 4 declarations
- CopyVarianceEquation.lean 1 declarations
- CopyVarianceRegularity.lean 2 declarations
- CopyWeightedCut.lean 4 declarations
- CopyWeightedPathCut.lean 1 declarations
- CovarianceTimeL2.lean 6 declarations
- CovarianceTotalEnergy.lean 5 declarations
- CriticalCopyEndgame.lean 2 declarations
- CriticalSmallLogLoss.lean 6 declarations
- CriticalSpatialRecovery.lean 4 declarations
- FiniteCovarianceEnergy.lean 2 declarations
- GaussianPosterior.lean 3 declarations
- Innovation.lean 12 declarations
- InnovationIndependence.lean 8 declarations
- InnovationLaw.lean 5 declarations
- JoinedResponseIntegrals.lean 2 declarations
- LocalizedArtanh.lean 2 declarations
- LogGaussianTail.lean 1 declarations
- LogWeightedOrbitCut.lean 4 declarations
- MixedFiltering.lean 10 declarations
- NoiseTwoTails.lean 1 declarations
- ObservationComparison.lean 4 declarations
- ObservationFactor.lean 12 declarations
- ObservationIndependence.lean 8 declarations
- ObservationInnovation.lean 19 declarations
- ObservationLaw.lean 6 declarations
- ObservationPosteriorMartingale.lean 5 declarations
- ObservationPosteriorTransport.lean 6 declarations
- ObservationRecovery.lean 7 declarations
- ObservationResponseEnergy.lean 10 declarations
- OrientedGaussianTail.lean 15 declarations
- OrientedNoiseSplit.lean 6 declarations
- OrientedPath.lean 6 declarations
- OrientedPathWeights.lean 7 declarations
- OrientedPrefixWeights.lean 8 declarations
- OrientedStemTail.lean 3 declarations
- ParameterRange.lean 3 declarations
- PathReversalTransport.lean 7 declarations
- PosteriorEnergyRegularity.lean 7 declarations
- PosteriorIntegralRepresentation.lean 2 declarations
- PosteriorL2Continuity.lean 4 declarations
- PosteriorRightContinuation.lean 3 declarations
- RootAttenuation.lean 7 declarations
- RootDoubleExponential.lean 5 declarations
- RootGaussianCut.lean 9 declarations
- RootWeightedCut.lean 5 declarations
- SharpVarianceRecovery.lean 4 declarations
- StemRerootAverage.lean 6 declarations
- StoppedDifferenceBounds.lean 2 declarations
- StoppedSquareAssembly.lean 5 declarations
- StrictFactorRecovery.lean 3 declarations
- WalkObstruction.lean 22 declarations