OAI/Probability/FreeIsing/Trees/
1363 declarations, 0 contain sorry, 0 declared as axioms; 147 files
Files
- ActualCutWeightedAverage.lean 3 declarations
- AutDistance.lean 2 declarations
- BranchFlipGeometry.lean 13 declarations
- BranchingExtinction.lean 9 declarations
- BranchingSurvivalLaw.lean 24 declarations
- BroadcastBlockIndependence.lean 2 declarations
- BroadcastBranchFamily.lean 3 declarations
- BroadcastBranchLabels.lean 6 declarations
- BroadcastConeLocality.lean 9 declarations
- BroadcastConeMarkov.lean 4 declarations
- BroadcastJointLaw.lean 1 declarations
- BroadcastLocality.lean 9 declarations
- BroadcastOutsideCone.lean 8 declarations
- CanonicalPathResponse.lean 9 declarations
- Cardinality.lean 5 declarations
- ClusterColorMarginal.lean 9 declarations
- ClusterComponentCount.lean 34 declarations
- ClusterFactorAssembly.lean 8 declarations
- ClusterFactorEnvironment.lean 3 declarations
- ClusterFactorMap.lean 20 declarations
- ClusterInputSampler.lean 26 declarations
- ClusterRestriction.lean 8 declarations
- CodedPercolation.lean 9 declarations
- ColoredEdgeDecay.lean 3 declarations
- ColoredEdgeLifts.lean 21 declarations
- ColoredPathAverage.lean 10 declarations
- ColoredPathCoefficients.lean 5 declarations
- ColoredPathCount.lean 5 declarations
- ColoredPathEndpoints.lean 7 declarations
- ConeCoding.lean 23 declarations
- ConeComplementField.lean 1 declarations
- ConeComplementFusion.lean 5 declarations
- ConeComponentAttenuation.lean 3 declarations
- ConePercolation.lean 7 declarations
- ConeSelectedFieldAttenuation.lean 1 declarations
- ConeSelectedFusion.lean 2 declarations
- ConeSubsetFusion.lean 5 declarations
- ConeSurvival.lean 4 declarations
- ConnectedExhaustion.lean 8 declarations
- ConnectedHull.lean 13 declarations
- ConnectedPercolation.lean 13 declarations
- CoordinateResponse.lean 5 declarations
- CoupledPathDrift.lean 4 declarations
- CoupledPathProducts.lean 13 declarations
- CoupledPathVariance.lean 3 declarations
- CutContinuationChannels.lean 18 declarations
- CutContinuations.lean 25 declarations
- CutLevelBranchIndependence.lean 15 declarations
- CutLevelConcentration.lean 4 declarations
- EdgeCylinders.lean 8 declarations
- EdgeIIDLaw.lean 20 declarations
- EdgeLabelCoding.lean 24 declarations
- EdgePercolationLaw.lean 12 declarations
- EncodedClusterLaw.lean 18 declarations
- EndpointFromPaths.lean 10 declarations
- Escape.lean 14 declarations
- FiniteClusterLaw.lean 12 declarations
- FiniteClusterSelector.lean 22 declarations
- FiniteClusterSelectorLaw.lean 1 declarations
- FinitePathCutCost.lean 2 declarations
- FinitePathGibbs.lean 40 declarations
- FreeIsingBranchFamily.lean 3 declarations
- FreeLawConeMarkov.lean 2 declarations
- GeodesicPrefix.lean 4 declarations
- GibbsAutomorphism.lean 12 declarations
- GibbsCovariance.lean 2 declarations
- GibbsField.lean 7 declarations
- GibbsMarginal.lean 2 declarations
- HalfPathDecay.lean 7 declarations
- IncidentEdges.lean 1 declarations
- IndexedPathVariance.lean 7 declarations
- InfiniteCanonicalPathResponse.lean 8 declarations
- InfiniteConeCavity.lean 2 declarations
- InfiniteInwardCavity.lean 2 declarations
- InnovationPathMap.lean 14 declarations
- InwardCutChannels.lean 5 declarations
- InwardCutCost.lean 3 declarations
- InwardCutFields.lean 13 declarations
- InwardCutProducts.lean 1 declarations
- Koopman.lean 14 declarations
- LawDecay.lean 4 declarations
- LawSpectral.lean 17 declarations
- LeafCovariance.lean 5 declarations
- LeafMarginal.lean 3 declarations
- NoisyBranchIndependence.lean 8 declarations
- NoisyBranchSeparation.lean 6 declarations
- NoisyBranchTransport.lean 3 declarations
- NoisyConeSeparation.lean 10 declarations
- NoisyCutLevelIndependence.lean 6 declarations
- NoisyEdgeDecay.lean 6 declarations
- NoisyPathLocality.lean 12 declarations
- NoisyRootIndependence.lean 4 declarations
- OpenClusterGeometry.lean 16 declarations
- OrbitAverage.lean 13 declarations
- Parents.lean 15 declarations
- PathAverageWeight.lean 3 declarations
- PathCutCost.lean 6 declarations
- PathCutoff.lean 6 declarations
- PathCylinders.lean 24 declarations
- PathGibbs.lean 9 declarations
- PathHomogeneity.lean 4 declarations
- PathPrefix.lean 8 declarations
- PathRerooting.lean 10 declarations
- PathResponse.lean 10 declarations
- PathReverseRerooting.lean 3 declarations
- PathSideBranches.lean 24 declarations
- PathSideInwardLocality.lean 6 declarations
- PathSideLocality.lean 7 declarations
- PathSideReroot.lean 5 declarations
- PathSplit.lean 9 declarations
- PathSums.lean 14 declarations
- PathVariance.lean 14 declarations
- PercolationFiniteness.lean 9 declarations
- PercolationSurvival.lean 9 declarations
- RadialEnergy.lean 12 declarations
- Regularity.lean 14 declarations
- ResponseAutomorphism.lean 9 declarations
- ResponseFieldBound.lean 5 declarations
- ResponseLeaf.lean 5 declarations
- ResponseRowEnergy.lean 12 declarations
- ResponseSourceInvariance.lean 4 declarations
- RestrictedCutCardinality.lean 11 declarations
- RootComponentAttenuation.lean 3 declarations
- RootCorrelation.lean 3 declarations
- RootCovariance.lean 1 declarations
- RootRegression.lean 4 declarations
- RootedBroadcast.lean 34 declarations
- RootedBroadcastLaw.lean 18 declarations
- RootedGeometry.lean 6 declarations
- RootedProjectivity.lean 3 declarations
- RootedTransitivity.lean 5 declarations
- RowEnergyCutoff.lean 3 declarations
- SelectedInwardPathAttenuation.lean 10 declarations
- SelectedPathAttenuation.lean 5 declarations
- SelectedPathLocality.lean 12 declarations
- SelectedPathSegmentAttenuation.lean 2 declarations
- Shells.lean 34 declarations
- SpinEncoding.lean 13 declarations
- StemRerootAverage.lean 10 declarations
- SubcriticalClusters.lean 14 declarations
- SubcriticalPathSums.lean 9 declarations
- Transitivity.lean 15 declarations
- WeightEncoding.lean 8 declarations
- WeightedPathSummation.lean 6 declarations
- WeightedShellSummation.lean 3 declarations
- WordAction.lean 13 declarations
- WordCancellation.lean 10 declarations