OAI/Probability/FreeIsing/Estimates/
1005 declarations, 0 contain sorry, 0 declared as axioms; 129 files
Files
- AEModification.lean 3 declarations
- AbsoluteContinuity.lean 4 declarations
- ArrayInnovationLaw.lean 4 declarations
- ArrayInnovationProjection.lean 2 declarations
- ArtanhTaylor.lean 16 declarations
- BalancedLatentMean.lean 4 declarations
- BoundedAverageConcentration.lean 6 declarations
- BoundedInnovationDrift.lean 16 declarations
- CenteredLocalDensity.lean 1 declarations
- CenteredWordAction.lean 7 declarations
- ChainMarginals.lean 7 declarations
- CharacteristicRecurrence.lean 8 declarations
- ClippedArtanhWeight.lean 13 declarations
- CoefficientTerminalCompletion.lean 3 declarations
- ColorAutomorphisms.lean 20 declarations
- CompensatedSquareLimit.lean 5 declarations
- ComponentFieldConsequences.lean 2 declarations
- ComponentFieldRecursion.lean 1 declarations
- ComponentFusionRecurrence.lean 5 declarations
- ComponentGibbsLimit.lean 6 declarations
- ComponentPairCount.lean 17 declarations
- ConstructedArtanhFormula.lean 1 declarations
- ContinuousCoefficientModulus.lean 8 declarations
- ContinuousHorizonGluing.lean 7 declarations
- ContinuousModification.lean 20 declarations
- ContinuousOptionalStopping.lean 11 declarations
- CountableProjective.lean 6 declarations
- CoupledCriticalComparison.lean 2 declarations
- CoupledSmallLogLoss.lean 9 declarations
- CylinderAutomorphism.lean 19 declarations
- CylinderBasics.lean 4 declarations
- DependentInfinitePiPair.lean 4 declarations
- DependentWeight.lean 5 declarations
- DiscrepancyDensityModification.lean 3 declarations
- DyadicContinuity.lean 14 declarations
- DyadicIncrementControl.lean 5 declarations
- EndpointScale.lean 11 declarations
- EndpointSums.lean 5 declarations
- EndpointTimeScale.lean 10 declarations
- ExponentialTaylor.lean 4 declarations
- FairSpin.lean 12 declarations
- FilteredFutureIndependence.lean 6 declarations
- FiniteBondMask.lean 7 declarations
- FiniteCavity.lean 8 declarations
- FiniteCavityComponents.lean 3 declarations
- FiniteChain.lean 15 declarations
- FiniteComponentFields.lean 3 declarations
- FiniteComponentGeometry.lean 24 declarations
- FiniteCoordinateApproximation.lean 3 declarations
- FiniteCoordinateRepresentation.lean 3 declarations
- FiniteGibbsField.lean 6 declarations
- FiniteIsingCompensatedSquare.lean 6 declarations
- FiniteIsingInnovation.lean 16 declarations
- FiniteIsingSplit.lean 17 declarations
- FiniteIsingZeroField.lean 4 declarations
- FiniteMarginals.lean 6 declarations
- FiniteMarkerRank.lean 7 declarations
- FiniteSpinCoupling.lean 14 declarations
- FiniteWeightNormalization.lean 10 declarations
- FreeIsingMeasure.lean 5 declarations
- FreeLawStationarity.lean 4 declarations
- FreeLawSymmetry.lean 5 declarations
- FreeLawUnique.lean 2 declarations
- IndependentEnlargement.lean 1 declarations
- IndependentLabelSampler.lean 5 declarations
- IndependentOwnFamily.lean 1 declarations
- InfiniteBlockIndependence.lean 9 declarations
- InfiniteComponentCavity.lean 2 declarations
- InfinitePiPair.lean 2 declarations
- InhomogeneousSpinChain.lean 28 declarations
- InnovationCharacteristic.lean 8 declarations
- IntegrableTimePrimitive.lean 4 declarations
- IntervalSumIntegrable.lean 3 declarations
- KernelCompatibility.lean 16 declarations
- LabelDecomposition.lean 6 declarations
- LatentFamilyIndependence.lean 2 declarations
- LatentProductIndependence.lean 3 declarations
- LawUniqueness.lean 3 declarations
- LeafDeletion.lean 7 declarations
- LeafWeights.lean 7 declarations
- LiftGram.lean 12 declarations
- LinearEstimator.lean 5 declarations
- LocalColorAutomorphisms.lean 19 declarations
- LocalCorrelation.lean 3 declarations
- LocalizedArtanhFormula.lean 3 declarations
- LogInterpolation.lean 3 declarations
- MeanSquareContinuity.lean 6 declarations
- MeasurableConnectivity.lean 6 declarations
- MessageFunction.lean 14 declarations
- NNRealArtanhFormula.lean 5 declarations
- NonbacktrackingAssembly.lean 5 declarations
- NonbacktrackingComplement.lean 9 declarations
- NonbacktrackingDecay.lean 21 declarations
- NonbacktrackingLiftBound.lean 3 declarations
- NonbacktrackingOperator.lean 16 declarations
- NonnegativeSeriesL1.lean 2 declarations
- NormalizedCriticalRowConvergence.lean 7 declarations
- NormalizedPositiveWindowRow.lean 10 declarations
- NormalizedSubcriticalRowConvergence.lean 7 declarations
- NormalizedThresholdRowConvergence.lean 2 declarations
- ObservableDisintegration.lean 14 declarations
- Osgood.lean 22 declarations
- OsgoodIntegration.lean 5 declarations
- PairCorrelation.lean 10 declarations
- PairedFiniteField.lean 13 declarations
- PastCompatibility.lean 4 declarations
- ProgressiveArrayInnovation.lean 3 declarations
- ProgressivePrimitive.lean 8 declarations
- ProgressivePrimitiveFubini.lean 5 declarations
- ProgressiveTimePrimitive.lean 1 declarations
- ProgressiveVersionPushforward.lean 14 declarations
- ProjectiveExtension.lean 11 declarations
- RadialRepresentation.lean 7 declarations
- RadialSummability.lean 11 declarations
- RadialWalk.lean 23 declarations
- RandomIndexSampling.lean 12 declarations
- RelabelMeasure.lean 3 declarations
- RoundedStoppingTimes.lean 17 declarations
- SelectedComponentFusion.lean 2 declarations
- SeparatedLocalSupports.lean 6 declarations
- SharedInnovationBounds.lean 5 declarations
- SupercriticalProfile.lean 21 declarations
- TerminalSufficiency.lean 5 declarations
- ThresholdArithmetic.lean 7 declarations
- TwoSeparatorRegression.lean 3 declarations
- UniformSampler.lean 2 declarations
- UniformTwist.lean 2 declarations
- WeightedOrbitAverage.lean 8 declarations
- WeightedPrimitiveApproximation.lean 12 declarations