IsingModel.lean

import IsingModel.Basic
import IsingModel.Combinatorics.AntidiagonalTupleCard
import IsingModel.Hamiltonian
import IsingModel.GibbsMeasure
import IsingModel.PartitionFunctionIso
import IsingModel.SumGraph
import IsingModel.SumModel
import IsingModel.Inequalities.NonnegCorrelations
import IsingModel.Inequalities.GKS
import IsingModel.Inequalities.Lebowitz
import IsingModel.Inequalities.FKG
import IsingModel.Inequalities.WeightedExpectation
import IsingModel.Inequalities.FKGGeneral
import IsingModel.Inequalities.FKGInhomogeneous
import IsingModel.Inequalities.FKGBoundaryCondition
import IsingModel.Inequalities.MonotonicityField
import IsingModel.Inequalities.MonotonicityBoundary
import IsingModel.Inequalities.MonotonicityExtremal
import IsingModel.Inequalities.VolumeMonotonicity
import IsingModel.Asano
import IsingModel.AmbientLattice
import IsingModel.AmbientLattice.SpecialCases.InteractingFreeEnergyMayerHighTemp
import IsingModel.AmbientLattice.GibbsExpectationHighTempExpansion
import IsingModel.AmbientLattice.SpecialCases.HighTemperatureBoundsDecayCapstonesAlphaFerro
import IsingModel.AmbientLattice.SpecialCases.HighTemperatureBoundsRatioLogFeNonemptyZ
import IsingModel.AmbientLattice.SpecialCases.Magnetization
import IsingModel.AmbientLatticeSum
import IsingModel.RandomCurrent
import IsingModel.RandomCurrent.BoundedExpansion.FiniteSums
import IsingModel.RandomCurrent.Switching.SwitchingIdentities
import IsingModel.Inequalities.SimonLieb
import IsingModel.Inequalities.CurrentConnectivityRepresentation
import IsingModel.Inequalities.SourcefreeConnectionRepresentation
import IsingModel.Inequalities.SourcefreeConnectionCurrentDeriv
import IsingModel.Inequalities.SourcefreeConnectionUnconditional
import IsingModel.Inequalities.SourcefreeConnectionRatioDerivative
import IsingModel.Inequalities.SourcefreeConnectionExcessEdgeSum
import IsingModel.Inequalities.SourcefreeConnectionEdgePivotal
import IsingModel.Inequalities.SourcefreeConnectionEdgeEmptyLeg
import IsingModel.Inequalities.SourcefreeConnectionEdgeReachableLeg
import IsingModel.Inequalities.SourcefreeConnectionTruncatedFourPointMass
import IsingModel.Inequalities.SourcefreeConnectionLebowitzConvolutionBound
import IsingModel.Inequalities.SourcefreeConnectionLebowitzConvolutionDegenerateBound
import IsingModel.Inequalities.ClusterConditioningPivotal
import IsingModel.Inequalities.ClusterConditioningFiberSplit
import IsingModel.Inequalities.ClusterConditioningFiberFubini
import IsingModel.Inequalities.ClusterConditioningFiberDecouple
import IsingModel.Inequalities.ClusterConditioningFiberFubiniSum
import IsingModel.Inequalities.SimonLiebKernel
import IsingModel.Inequalities.SharpSimonLiebNeighbor
import IsingModel.Inequalities.WalkSum
import IsingModel.Inequalities.SimonLiebIterate
import IsingModel.Inequalities.SimonLiebIterateHighTemp
import IsingModel.Inequalities.SimonLiebIterateDecay
import IsingModel.Inequalities.WalkSumRepresentation
import IsingModel.Inequalities.WalkSumTsum
import IsingModel.Inequalities.WalkSumDistanceDecay
import IsingModel.Concrete.LatticeGraphCorrelation.SimonLiebDecayLatticeGraph
import IsingModel.Concrete.LatticeGraphCorrelation.SimonLiebDecayLatticeDistance
import IsingModel.Concrete.LatticeGraphCorrelation.Truncated2GeneralFieldFiniteVolumeMajorant
import IsingModel.Concrete.LatticeGraphCorrelation.Truncated2FieldDerivativeUniformBound
import IsingModel.Concrete.LatticeGraphCorrelation.Truncated3FieldDerivCollarTail
import IsingModel.Concrete.LatticeGraphCorrelation.Truncated3FieldDerivInfiniteMajorant
import IsingModel.Concrete.LatticeGraphCorrelation.SimonLiebDecayInfiniteVolume
import IsingModel.Concrete.LatticeGraphCorrelation.WalkSumTsumLatticeGraph
import IsingModel.Concrete.LatticeGraphCorrelation.WalkSumTsumInfiniteVolume
import IsingModel.Concrete.LatticeGraphCorrelation.SharpLatticeMassLowerBound
import IsingModel.Concrete.LatticeGraphCorrelation.Thm1721LatticeGraph
import IsingModel.Concrete.LatticeGraphCorrelation.CubicBoxPlusState
import IsingModel.Concrete.LatticeGraphCorrelation.CubicBoxPlusStateBounds
import IsingModel.Concrete.LatticeGraphCorrelation.CubicBoxScreening
import IsingModel.Concrete.LatticeGraphCorrelation.CubicBoxScreeningDecomp
import IsingModel.Concrete.LatticeGraphCorrelation.CubicBoxScreeningCapstone
import IsingModel.Concrete.LatticeGraphCorrelation.CubicBoxScreeningLimit
import IsingModel.Concrete.LatticeGraphCorrelation.InfiniteVolumePlusState
import IsingModel.Concrete.LatticeGraphCorrelation.LocalObservableLimit
import IsingModel.Concrete.LatticeGraphCorrelation.LocalObservableState
import IsingModel.Concrete.LatticeGraphCorrelation.MinusStateExtremal
import IsingModel.Concrete.LatticeGraphCorrelation.CubicBoxExtremalCoincidence
import IsingModel.Concrete.LatticeGraphCorrelation.CubicBoxFreeLimit
import IsingModel.Concrete.LatticeGraphCorrelation.LocalObservableExtremalCoincidence
import IsingModel.Concrete.LatticeGraphCorrelation.LocalObservableFreeLimit
import IsingModel.Concrete.LatticeGraphCorrelation.LocalObservableUnion
import IsingModel.Concrete.LatticeGraphCorrelation.PlusStateTranslation
import IsingModel.Concrete.LatticeGraphCorrelation.CubicBoxInterlacing
import IsingModel.AmbientLattice.Monotonicity.PlusScreening
import IsingModel.Concrete.LatticeGraphCorrelation.PlusStateTranslationInvariance
import IsingModel.Concrete.LatticeGraphCorrelation.PlusStateTranslationCapstone
import IsingModel.Concrete.LatticeGraphCorrelation.PlusStateTranslationFinal
import IsingModel.Concrete.LatticeGraphCorrelation.PlusStateTranslationHeadline
import IsingModel.Concrete.LatticeGraphCorrelation.PlusStateTranslationGeneral
import IsingModel.Concrete.LatticeGraphCorrelation.PlusStateTranslationGeneralHeadline
import IsingModel.Concrete.LatticeGraphCorrelation.MinusStateTranslation
import IsingModel.Concrete.LatticeGraphCorrelation.PlusStateExhaustion
import IsingModel.Concrete.LatticeGraphCorrelation.PlusStateAmbientCubic
import IsingModel.Concrete.LatticeGraphCorrelation.PlusStateAmbientIndep
import IsingModel.Concrete.LatticeGraphCorrelation.PlusRegionExpectation
import IsingModel.Concrete.LatticeGraphCorrelation.PlusRegionCubicConvergence
import IsingModel.Concrete.LatticeGraphCorrelation.PlusRegionExhaustion
import IsingModel.Concrete.LatticeGraphCorrelation.PlusRegionObsExhaustion
import IsingModel.Concrete.LatticeGraphCorrelation.InfiniteVolumeMagnetization
import IsingModel.Concrete.LatticeGraphCorrelation.MagnetizationFlipSymmetry
import IsingModel.Concrete.LatticeGraphCorrelation.MagnetizationFieldMonotone
import IsingModel.Concrete.LatticeGraphCorrelation.SpontaneousMagnetization
import IsingModel.Concrete.LatticeGraphCorrelation.MagnetizationSign
import IsingModel.Concrete.LatticeGraphCorrelation.MagnetizationBetaMonotone
import IsingModel.Concrete.LatticeGraphCorrelation.PlusStateCongrN
import IsingModel.Concrete.LatticeGraphCorrelation.MagnetizationSiteIndependence
import IsingModel.Concrete.LatticeGraphCorrelation.PlusTwoPoint
import IsingModel.Concrete.LatticeGraphCorrelation.CorrelationPairSymmetryBundle
import IsingModel.Concrete.LatticeGraphCorrelation.Lemma_17_5_2.ChebyshevRateBridge
import IsingModel.Concrete.LatticeGraphCorrelation.Lemma_17_5_2.HasExponentialDecayChebyshev
import IsingModel.Concrete.LatticeGraphCorrelation.Truncated2GeneralFieldCluster
import IsingModel.Concrete.LatticeGraphCorrelation.Truncated2GeneralFieldDecay
import IsingModel.Inequalities.GKSBoundaryCondition
import IsingModel.Inequalities.GKSBoundaryConditionII
import IsingModel.Inequalities.MonotonicityJBoundaryCondition
import IsingModel.Inequalities.MonotonicityBetaBoundaryCondition
import IsingModel.Inequalities.GKSBoundaryConditionTwoPoint
import IsingModel.Concrete.LatticeGraphCorrelation.SpontaneousMagnetizationTwoPoint
import IsingModel.Conditioning.PlusHighTempRepresentation
import IsingModel.Conditioning.PlusOnePointRepresentation
import IsingModel.Conditioning.PlusOnePointConnectedBound
import IsingModel.Conditioning.EdgeSetDistance
import IsingModel.Conditioning.EdgeSetHandshake
import IsingModel.Conditioning.InduceDistanceTransfer
import IsingModel.Conditioning.CubicBoxComponentSize
import IsingModel.Conditioning.WalkCountDegreeBound
import IsingModel.Conditioning.GeometricTail
import IsingModel.Conditioning.CountGeometricCapstone
import IsingModel.Conditioning.EdgeWalkExistence
import IsingModel.Conditioning.EdgeWalkCounting
import IsingModel.Conditioning.CubicBoxMagnetizationDecay
import IsingModel.Conditioning.HighTempZeroMagnetization
import IsingModel.Conditioning
import IsingModel.Conditioning.CorrelationClosed
import IsingModel.Conditioning.CorrelationClosed.TruncatedGeneralField
import IsingModel.Inequalities.HighTemp
import IsingModel.BetaDerivative
import IsingModel.FieldDerivative
import IsingModel.JDerivative
import IsingModel.PseudoMass
import IsingModel.PseudoMass.Composition
import IsingModel.LatticeExpSum
import IsingModel.ComplexAnalyticity
import IsingModel.Peierls.ConnectedDroplet
import IsingModel.Peierls.DropletInjective
import IsingModel.Peierls.CutCrossingParity
import IsingModel.Peierls.PlanarBondParityCore
import IsingModel.Peierls.PlanarBondSeparationBridge
import IsingModel.Peierls.EdgeSideComponent
import IsingModel.Peierls.DartDualComponentImage
import IsingModel.Peierls.PlanarBondAssembly
import IsingModel.Peierls.DartDualComponentEulerian
import IsingModel.Peierls.DartDualCutEven
import IsingModel.Peierls.DualComponentSeparatesOfStokes
import IsingModel.Peierls.DartDualComponentBoxEulerian
import IsingModel.Peierls.DartDualComponentBoxIncidentEven
import IsingModel.Peierls.PrimalSquareBoundary
import IsingModel.Peierls.RightRayParity
import IsingModel.Peierls.RightRayVerticalSquare
import IsingModel.Peierls.RightRayVerticalXor
import IsingModel.Peierls.RightRayVerticalStep
import IsingModel.Peierls.RightRayVerticalParity
import IsingModel.Peierls.FixedRayRegion
import IsingModel.Peierls.PlanarBondDischarge
import IsingModel.Peierls.BondConnectivityBridge
import IsingModel.Peierls.BondFilledEdgeConnected
import IsingModel.Peierls.PeierlsContourCountFilled
import IsingModel.Peierls.PeierlsMagnetizationPosFilled
import IsingModel.Peierls.CubicBoxPreconnected
import IsingModel.Peierls.CubicBoxBoundaryShell
import IsingModel.Peierls.CubicBoxShellConnected
import IsingModel.Peierls.FilledRegion
import IsingModel.Peierls.FilledRegionIdempotent
import IsingModel.Peierls.FilledRegionConnected
import IsingModel.Peierls.FilledConnectedBound
import IsingModel.Peierls.ComplConnected
import IsingModel.Peierls.SameOrbit
import IsingModel.Peierls.OrbitDualEdges
import IsingModel.Peierls.DualCutConnected
import IsingModel.Peierls.DartDualCutCard
import IsingModel.Peierls.DualSupport
import IsingModel.Peierls.DualCutSubConnected
import IsingModel.Peierls.DualCutInBox
import IsingModel.Peierls.PlanarBondReduction
import IsingModel.Peierls.ContourCount
import IsingModel.Peierls.DualToPrimal
import IsingModel.Peierls.DartPrimalCut
import IsingModel.Peierls.DualCutInBoxInjective
import IsingModel.Peierls.DartOfCut
import IsingModel.Peierls.DartCutChar
import IsingModel.Peierls.DartPrimalCutCard
import IsingModel.Peierls.LiftBoxCutChar
import IsingModel.Peierls.BoxBridge
import IsingModel.Peierls.LiftBoxCutInjective
import IsingModel.Peierls.ContourInjective
import IsingModel.Peierls.DualCutCardBridge
import IsingModel.Peierls.RayExit
import IsingModel.Peierls.RayAnchorDart
import IsingModel.Peierls.RayAnchorBox
import IsingModel.Peierls.RayExitAnchorDart
import IsingModel.Peierls.RayExitAnchorPrefix
import IsingModel.Peierls.RayExitAnchorStep
import IsingModel.Peierls.RayExitBound
import IsingModel.Peierls.RayAnchorBound
import IsingModel.Peierls.RayAnchorSet
import IsingModel.Peierls.ContourCountCover
import IsingModel.Peierls.ContourCountAssembly
import IsingModel.Peierls.PeierlsContourCount
import IsingModel.Peierls.PeierlsContourCountPow
import IsingModel.Peierls.PeierlsSum
import IsingModel.Peierls.PeierlsPlusGibbs
import IsingModel.Peierls.PeierlsTendsto
import IsingModel.Peierls.CutDeterminesRegion
import IsingModel.Peierls.GridEdge2
import IsingModel.Peierls.GridEdge2Cut
import IsingModel.Peierls.DualCut
import IsingModel.Peierls.LiftBoxCut
import IsingModel.Peierls.ContourEven
import IsingModel.Peierls.SingleOrbitFaceDart
import IsingModel.Peierls.SingleOrbitFaceCard
import IsingModel.Peierls.SingleOrbitEulerian
import IsingModel.Peierls.SingleOrbitCutDirDart
import IsingModel.Peierls.SingleOrbitDegTwoPairing
import IsingModel.Peierls.DualCutEdgeAdjacency
import IsingModel.Peierls.DartDualReachable
import IsingModel.Peierls.DartReachableFPath
import IsingModel.Peierls.SingleOrbitEdgeValid
import IsingModel.Peierls.Dir2
import IsingModel.Peierls.BoundaryDart
import IsingModel.Peierls.NextDart
import IsingModel.Peierls.DartFinite
import IsingModel.Peierls.DartStepReverse
import IsingModel.Peierls.PrevDart
import IsingModel.Peierls.DartBijection
import IsingModel.Peierls.DartBijective
import IsingModel.Peierls.DartOrbit
import IsingModel.Peierls.LowTempTail
import IsingModel.Peierls.PeierlsLiminf
import IsingModel.Peierls.PeierlsMagnetizationPos
import IsingModel.PeierlsInfinite
import IsingModel.TranslationInvariance
import IsingModel.Concrete.IntLattice
import IsingModel.Concrete.CubicExhaustion
import IsingModel.Concrete.CubicTiling
import IsingModel.Concrete.CubicFreeEnergy
import IsingModel.Concrete.CubicFreeEnergyAnalyticity
import IsingModel.Concrete.CubicBoxConnectivity
import IsingModel.Concrete.CubicBoxAdjacencyGeometry
import IsingModel.Concrete.LatticeGraphBED
import IsingModel.Concrete.LatticeGraphFreeEnergy
import IsingModel.Concrete.LatticeGraphCorrelation
import IsingModel.Concrete.LinearBrick
import IsingModel.Concrete.StripeBrick2D
import IsingModel.Concrete.SlabBrick
import IsingModel.Concrete.CenteredSlab
import IsingModel.Concrete.CenteredSlab.InfiniteVolumeMonotone
import IsingModel.ContinuousSpin.Measure
import IsingModel.ContinuousSpin.MvPolynomialNonnegCoeffs
import IsingModel.ContinuousSpin.Phi4
import IsingModel.ContinuousSpin.Phi4AllOdd
import IsingModel.ContinuousSpin.Phi4Averaging
import IsingModel.ContinuousSpin.Phi4Reflection
import IsingModel.ContinuousSpin.Phi4Symmetrization
import IsingModel.ContinuousSpin.TwoComponent
import IsingModel.ContinuousSpin.TwoComponentChangeOfVariables
import IsingModel.ContinuousSpin.TwoComponentDoubledWeight
import IsingModel.ContinuousSpin.TwoComponentDoubling
import IsingModel.ContinuousSpin.TwoComponentGriffiths
import IsingModel.ContinuousSpin.TwoComponentGriffithsI
import IsingModel.ContinuousSpin.TwoComponentGriffithsII
import IsingModel.ContinuousSpin.TwoComponentGriffithsIII
import IsingModel.ContinuousSpin.TwoComponentGriffithsIV
import IsingModel.ContinuousSpin.TwoComponentGriffithsV
import IsingModel.ContinuousSpin.TwoComponentGriffithsVI
import IsingModel.ContinuousSpin.TwoComponentGriffithsVII
import IsingModel.ContinuousSpin.TwoComponentIntegrable
import IsingModel.ContinuousSpin.TwoComponentLebowitz
import IsingModel.ContinuousSpin.TwoComponentMonomialIntegrable
import IsingModel.ContinuousSpin.TwoComponentMultiIntegrable
import IsingModel.ContinuousSpin.TwoComponentRotation
import IsingModel.ContinuousSpin.TwoComponentRotationAlgebra
import IsingModel.ContinuousSpin.TwoComponentSystem
import IsingModel.ClusterExpansion
import IsingModel.ClusterExpansion.Penrose
import IsingModel.ClusterExpansion.SourceGeneratingFunction
import IsingModel.ClusterExpansion.SourceLogCoefficient
import IsingModel.ClusterExpansion.TwoPointNumeratorFactorization
import IsingModel.ClusterExpansion.TwoPointNumeratorBound
import IsingModel.ClusterExpansion.AnchoredPeel
import IsingModel.ClusterExpansion.FieldSourceAvoidFactor
import IsingModel.ClusterExpansion.TwoPointAnchoredCount
import IsingModel.ClusterExpansion.TwoPointNumeratorEquality
import IsingModel.ClusterExpansion.TwoPointRatioBound
import IsingModel.ClusterExpansion.AnchoredComponentRatio
import IsingModel.ClusterExpansion.AvoidingPolymerGas
import IsingModel.ClusterExpansion.AvoidingDeleteEdges
import IsingModel.ClusterExpansion.AvoidingRatioExp
import IsingModel.ClusterExpansion.TouchingClusterDecomp
import IsingModel.ClusterExpansion.FixedVertexTouchingUnion
import IsingModel.ClusterExpansion.FixedVertexPeelBound
import IsingModel.ClusterExpansion.FixedVertexChainEnds
import IsingModel.ClusterExpansion.FixedVertexChainMid
import IsingModel.ClusterExpansion.FixedVertexTouchingPerOrder
import IsingModel.ClusterExpansion.MayerSumDiffSupportBound
import IsingModel.ClusterExpansion.MayerSumDiffSupportBoundComplex
import IsingModel.ClusterExpansion.TwoPointCapstonePrereqs
import IsingModel.ClusterExpansion.TwoPointCorrelationHTBound
import IsingModel.ClusterExpansion.GeneralRatioBound
import IsingModel.ClusterExpansion.TwoPointCorrelationInfiniteAnalytic
import IsingModel.ClusterExpansion.Families.FieldConnectedPolymers
import IsingModel.Conditioning.HighTempClosed.ClosedFormFieldPolymer
import IsingModel.ClusterExpansion.TwoPointCorrelationInfiniteBetaDeriv
import IsingModel.ClusterExpansion.TwoPointConvergenceRegion
import IsingModel.ClusterExpansion.TwoPointDerivativeConvergenceRegion
import IsingModel.ClusterExpansion.TwoPointConvergenceWindow
import IsingModel.ClusterExpansion.GeometricMoment
import IsingModel.ClusterExpansion.GeometricFiberSum
import IsingModel.ClusterExpansion.PiFinsetSeparation
import IsingModel.ClusterExpansion.PiFinsetSeparationPivot
import IsingModel.ClusterExpansion.PolymerCounting
import IsingModel.ClusterExpansion.PolymerActivity
import IsingModel.ClusterExpansion.FieldPolymerActivity
import IsingModel.ClusterExpansion.FieldMayerTerm
import IsingModel.ClusterExpansion.FieldMayerIdentity
import IsingModel.Conditioning.CorrelationClosed.GeneralFieldClosed
import IsingModel.Conditioning.CorrelationClosed.GeneralFieldClosedComplex
import IsingModel.ClusterExpansion.FieldPolymerExpNonvanishing
import IsingModel.ClusterExpansion.FieldPolymerComplexNonvanishing
import IsingModel.ClusterExpansion.FieldMayerCouplingTower
import IsingModel.ClusterExpansion.FieldExpIdentityDegreeWindow
import IsingModel.ClusterExpansion.FieldMayerTermPerOrderBound
import IsingModel.ClusterExpansion.FieldAvoidingRatio
import IsingModel.ClusterExpansion.FieldVertexAvoidingRatio
import IsingModel.ClusterExpansion.FieldSourceCount
import IsingModel.ClusterExpansion.FieldSourcePeel
import IsingModel.ClusterExpansion.FieldSourceRoot
import IsingModel.ClusterExpansion.FieldSourceWeightBound
import IsingModel.ClusterExpansion.FieldCorrelationUniformBound
import IsingModel.ClusterExpansion.FieldCorrelationAlongExhaustion
import IsingModel.ClusterExpansion.FieldCorrelationBallUniform
import IsingModel.ClusterExpansion.FieldCorrelationVitali
import IsingModel.ClusterExpansion.FieldTwoPointCorrelationInfiniteAnalytic
import IsingModel.ClusterExpansion.FieldCorrelationInfiniteFieldDeriv
import IsingModel.ClusterExpansion.FieldVolumeUniformZNonvanishing
import IsingModel.ClusterExpansion.PolymerActivityKP
import IsingModel.ClusterExpansion.PolymerActivityMoment
import IsingModel.ClusterExpansion.PolymerActivityTailMoment
import IsingModel.ClusterExpansion.RootMomentBound
import IsingModel.ClusterExpansion.RootedParentActivePeelBoundFactorial
import IsingModel.ClusterExpansion.PolymerActivityKPMoment
import IsingModel.ClusterExpansion.PolymerActivityKPMomentTail
import IsingModel.ClusterExpansion.RootedParentActive
import IsingModel.ClusterExpansion.RootedParentLeafExistence
import IsingModel.ClusterExpansion.RootedParentActiveSum
import IsingModel.ClusterExpansion.RootedParentActiveSplit
import IsingModel.ClusterExpansion.RootedParentActiveLeafPeel
import IsingModel.ClusterExpansion.RootedParentActiveSplitApply
import IsingModel.ClusterExpansion.RootedParentActiveLeafColumn
import IsingModel.ClusterExpansion.RootedParentActiveLeafColumnTail
import IsingModel.ClusterExpansion.RootedParentActiveLeafPeelTailBound
import IsingModel.ClusterExpansion.RootedParentActiveLeafInner
import IsingModel.ClusterExpansion.RootedParentActiveLeafPeelStep
import IsingModel.ClusterExpansion.RootedParentActiveLeafPeelBound
import IsingModel.ClusterExpansion.RootedParentActiveLeafPeelInduction
import IsingModel.ClusterExpansion.RootedParentActiveLeafPeelTailInduction
import IsingModel.ClusterExpansion.Penrose.FiberFactorialSum
import IsingModel.ClusterExpansion.Penrose.ParentCodeFactorialSum
import IsingModel.ClusterExpansion.Penrose.TreeChildCountFactorialBound
import IsingModel.ClusterExpansion.RootedParentActiveLeafPeelTree
import IsingModel.ClusterExpansion.RootedParentActiveLeafPeelTailTree
import IsingModel.ClusterExpansion.RootedParentActiveUnivReindex
import IsingModel.ClusterExpansion.RootedParentActiveUnivForm
import IsingModel.ClusterExpansion.RootedParentActiveTreeBridge
import IsingModel.ClusterExpansion.RootedParentActiveTreePeelBound
import IsingModel.ClusterExpansion.RootedParentActiveTreePeelBoundTail
import IsingModel.ClusterExpansion.MayerTermPeelBound
import IsingModel.ClusterExpansion.MayerTermPeelBoundTail
import IsingModel.ClusterExpansion.MayerTermTailSummability
import IsingModel.ClusterExpansion.MayerSeriesConvergence
import IsingModel.ClusterExpansion.MayerTsumBound
import IsingModel.ClusterExpansion.MayerTsumPerSite
import IsingModel.ClusterExpansion.MayerTsumPerSiteAmbient
import IsingModel.ClusterExpansion.HighTempKoteckyPreiss
import IsingModel.ClusterExpansion.HighTempKoteckyPreissRegularity
import IsingModel.ClusterExpansion.HighTempAnalyticityCapstone
import IsingModel.ClusterExpansion.Penrose.PolymerSeqTreeOrientation
import IsingModel.ClusterExpansion.Penrose.PolymerSeqTreeKP
import IsingModel.ClusterExpansion.Penrose.CompleteTreePolymerConstraint
import IsingModel.ClusterExpansion.UrsellTreeBound
import IsingModel.ClusterExpansion.AlternatingFinThree
import IsingModel.ClusterExpansion.PathGraphAlternatingSum
import IsingModel.ClusterExpansion.CycleGraphAlternatingSum
import IsingModel.ClusterExpansion.Families
import IsingModel.ClusterExpansion.MayerCompleteContribution
import IsingModel.ClusterExpansion.UrsellFinThree
import IsingModel.ClusterExpansion.MayerCore.UrsellMajorant
import IsingModel.ClusterExpansion.MayerCore.MayerTreeSumActivity
import IsingModel.ClusterExpansion.MayerCore.MayerTreeSumExpActivity
import IsingModel.ClusterExpansion.MayerCore.MayerTanhConvergence
import IsingModel.ClusterExpansion.MayerCore.InteractingFreeEnergyMayer
import IsingModel.ClusterExpansion.MayerCore.InteractingFreeEnergyMayerHighTemp
import IsingModel.ClusterExpansion.MayerCore.TermsComplex
import IsingModel.ClusterExpansion.MayerCore.TermsComplexHolomorphic
import IsingModel.ClusterExpansion.MayerCore.TermsComplexPerSiteBound
import IsingModel.ClusterExpansion.MayerCore.CubicMayerClusterFreeEnergyComplex
import IsingModel.ClusterExpansion.MayerCore.CubicMayerClusterMontel
import IsingModel.ClusterExpansion.MayerCore.MayerIdentityPersiteKP
import IsingModel.ClusterExpansion.MayerCore.ComplexMayerMontroll
import IsingModel.ClusterExpansion.MayerCore.MayerMontroll
import IsingModel.ClusterExpansion.MayerCore.CubicMayerClusterRealAxis
import IsingModel.ClusterExpansion.MayerCore.CubicMayerClusterLimit
import IsingModel.ClusterExpansion.MayerCore.CubicMayerCouplingAnalyticity
import IsingModel.ClusterExpansion.MayerCore.CubicMayerCouplingDirectionAnalyticity
import IsingModel.ClusterExpansion.MayerCore.CubicMayerHighTempIntervalAnalyticity
import IsingModel.ClusterExpansion.MayerCore.LatticeFreeEnergyKPBound
import IsingModel.ClusterExpansion.MayerCore.LatticeFreeEnergyInfiniteKPBound
import IsingModel.ClusterExpansion.MayerCore.IndependentCapstone
import IsingModel.ClusterExpansion.MayerCore.IndependentFreeEnergyMayer
import IsingModel.ClusterExpansion.MayerCore.IndependentMayerTerm
import IsingModel.ClusterExpansion.MayerCore.IndependentPolymer
import IsingModel.ClusterExpansion.MayerCore.IndependentVanishing
import IsingModel.TransferMatrix.OneDim
import IsingModel.TransferMatrix.OneDimField
import IsingModel.TransferMatrix.OneDimFieldPower
import IsingModel.TransferMatrix.OneDimFieldMagnetization
import IsingModel.TransferMatrix.OneDimFieldSusceptibility
import IsingModel.TransferMatrix.OneDimPower
import IsingModel.TransferMatrix.OneDimFreeEnergy
import IsingModel.TransferMatrix.TraceSum
import IsingModel.TransferMatrix.TraceSum1D
import IsingModel.TransferMatrix.OneDimTwoPoint
import IsingModel.TransferMatrix.CycleGraphLink
import IsingModel.TransferMatrix.CycleGraphZ
import IsingModel.TransferMatrix.OneDimCorrelationLength
import IsingModel.TransferMatrix.OneDimSusceptibility
import IsingModel.TransferMatrix.OneDimGibbsFreeEnergy
import IsingModel.TransferMatrix.MarkedTrace
import IsingModel.TransferMatrix.MarkedTraceClosedWalk
import IsingModel.TransferMatrix.MarkedTrace1D
import IsingModel.TransferMatrix.GibbsTwoPoint
import IsingModel.TransferMatrix.GibbsTwoPointDecay
import IsingModel.TransferMatrix.LayerTransfer
import IsingModel.TransferMatrix.LayerGibbs
import IsingModel.TransferMatrix.LayerCylinder
import IsingModel.TransferMatrix.LayerCylinderGraph
import IsingModel.TransferMatrix.CubicLayerCylinder
import IsingModel.TransferMatrix.LayerSpectral
import IsingModel.TransferMatrix.LayerPerron
import IsingModel.TransferMatrix.LayerPerronExistence
import IsingModel.TransferMatrix.LayerCardinalitySmallRatio
import IsingModel.TransferMatrix.CubicLayerCardinalitySmallRatio
import IsingModel.TransferMatrix.LayerSpectralWindowSmallRatio
import IsingModel.TransferMatrix.OneSiteLayerSpectralWindow
import IsingModel.TransferMatrix.TwoSiteFreeLayerSpectralWindow
import IsingModel.TransferMatrix.FreeLayerWalshSpectralWindow
import IsingModel.TransferMatrix.LayerOpenSlab
import IsingModel.TransferMatrix.LayerOpenSpectral
import IsingModel.TransferMatrix.LayerOpenSpectralDenominator
import IsingModel.TransferMatrix.LayerOpenSlabGraph
import IsingModel.TransferMatrix.LayerOpenSpectralDecay
import IsingModel.TransferMatrix.LayerOpenTwoMarkedSpectralDecay
import IsingModel.TransferMatrix.LayerOpenPerron
import IsingModel.TransferMatrix.LayerOpenBoundaryWindow
import IsingModel.TransferMatrix.LayerOpenSubdominantWindow
import IsingModel.TransferMatrix.LayerOpenBoundaryNormWindow
import IsingModel.TransferMatrix.LayerOpenPhysicalNormWindow
import IsingModel.TransferMatrix.LayerOpenParitySimple
import IsingModel.TransferMatrix.LayerOpenBoundaryWindowSimple
import IsingModel.TransferMatrix.LayerOpenSimpleSpectrum
import IsingModel.TransferMatrix.OneSiteLayerOpenBoundaryWindow
import IsingModel.TransferMatrix.TwoSiteInteractingLayerSpectralData
import IsingModel.TransferMatrix.TwoSiteInteractingLayerSpectralWindow
import IsingModel.TransferMatrix.TwoSiteInteractingLayerOpenBoundaryWindow
import IsingModel.TransferMatrix.TwoSiteInteractingLayerOpenCrossBoundaryWindow
import IsingModel.TransferMatrix.TwoSiteInteractingLayerOpenDecay
import IsingModel.TransferMatrix.TwoSiteInteractingOpenStripTransport
import IsingModel.TransferMatrix.TwoSiteInteractingOpenStripDecay
import IsingModel.TransferMatrix.TwoSiteInteractingOpenStripCrossInfiniteVolume
import IsingModel.TransferMatrix.TwoSiteInteractingOpenStripInfiniteVolume
import IsingModel.TransferMatrix.TwoSiteInteractingOpenStripInfiniteVolumeClustering
import IsingModel.TransferMatrix.TwoSiteInteractingOpenStripClusterProperty
import IsingModel.TransferMatrix.LayerOpenFiniteTransverseHermitian
import IsingModel.TransferMatrix.CubicLayerOpenBoxTransport
import IsingModel.TransferMatrix.CubicLayerOpenBoxMass
import IsingModel.TransferMatrix.CubicLayerOpenBoxExplicitMass
import IsingModel.TransferMatrix.LayerOpenExplicitSubdominantRatio
import IsingModel.TransferMatrix.FreeLayerWalshOpenPerron
import IsingModel.TransferMatrix.FreeLayerWalshOpenDecay
import IsingModel.TransferMatrix.FreeLayerWalshOpenInfiniteVolume
import IsingModel.TransferMatrix.FreeLayerWalshOpenAxisDecay
import IsingModel.TransferMatrix.FreeLayerWalshOpenAxisInfiniteVolume
import IsingModel.TransferMatrix.PathGraphEdges
import IsingModel.TransferMatrix.PathGraphTwoPoint
import IsingModel.TransferMatrix.PathGraphPairTwoPoint
import IsingModel.TransferMatrix.InfiniteVolumeOneD
import IsingModel.TransferMatrix.InfiniteVolumeOneDSusceptibility
import IsingModel.TransferMatrix.InfiniteVolumeOneDMass
import IsingModel.TransferMatrix.ClusterExpansionSupersession
import IsingModel.PhaseTransition.FieldResponseHighTemp

import IsingModel.Analysis.HolomorphicEquicontinuity
import IsingModel.AmbientComplexAnalyticity.AscoliData.Constructors.AnalyticSideConditions
import IsingModel.AmbientComplexAnalyticity.AscoliData.Structures
import IsingModel.AmbientComplexAnalyticity.Basic.BranchBounds
import IsingModel.AmbientComplexAnalyticity.Vitali.BranchUniformBounds
import IsingModel.AmbientComplexAnalyticity.Vitali.CorrelationBridge
import IsingModel.AmbientComplexAnalyticity.Vitali.CorrelationPerStageHolomorphic
import IsingModel.ComplexAnalyticity.FunctionTheoryAxioms
import IsingModel.ComplexAnalyticity.VitaliPorter.Uniqueness
import IsingModel.ComplexAnalyticity.VitaliPorter.Equicontinuity
import IsingModel.ComplexAnalyticity.VitaliPorter.PerCompact
import IsingModel.ComplexAnalyticity.VitaliPorter.Exhaustion
import IsingModel.ComplexAnalyticity.VitaliPorter.MontelExtraction
import IsingModel.ComplexAnalyticity.VitaliPorter.Theorem
import IsingModel.ComplexAnalyticity.CorrelationRatioForm
import IsingModel.AmbientComplexAnalyticity.Vitali.CorrelationVitaliPorter
import IsingModel.AmbientComplexAnalyticity.Vitali.CorrelationRealAxisVitali
import IsingModel.AmbientComplexAnalyticity.VolumeUniformZIdentity
import IsingModel.AmbientComplexAnalyticity.VolumeUniformZNonvanishing
import IsingModel.ComplexAnalyticity.ClosureCompactness
import IsingModel.Dobrushin.SingleSiteInfluence
import IsingModel.Dobrushin.SingleSiteConditional
import IsingModel.Dobrushin.SingleSiteConditionalProb
import IsingModel.Dobrushin.SingleSiteConditionalDistribution
import IsingModel.Dobrushin.SingleSiteInfluenceMatrix
import IsingModel.Dobrushin.SingleSiteObservableComparison
import IsingModel.Dobrushin.HeatBathInvariance
import IsingModel.Dobrushin.SiteOscillation
import IsingModel.Dobrushin.BoundaryInfluence
import IsingModel.Dobrushin.BoundaryWeight
import IsingModel.Dobrushin.HeatBathSweep
import IsingModel.Dobrushin.GibbsBoundaryComparison
import IsingModel.Dobrushin.ComparisonTheorem
import IsingModel.Dobrushin.Locality
import IsingModel.Dobrushin.SweepContraction
import IsingModel.Dobrushin.SingleSiteGeneralComparison
import IsingModel.Dobrushin.OscillationPropagation
import IsingModel.Dobrushin.ResolventComparison
import IsingModel.Dobrushin.DobrushinHighTemp
import IsingModel.Dobrushin.InfluenceMatrixDecay
import IsingModel.Dobrushin.InfluenceMatrixResolvent
import IsingModel.Dobrushin.DobrushinResolvent
import IsingModel.Dobrushin.ResolventDecay
import IsingModel.Dobrushin.ExponentialLocality
import IsingModel.Dobrushin.Uniqueness
import IsingModel.Dobrushin.InfiniteVolumeUniformInfluence
import IsingModel.Dobrushin.InfiniteVolumeBoundaryInfluence
import IsingModel.Dobrushin.InfiniteVolumeUniqueness

/-!
# The `IsingModel` library, aggregated

This module declares nothing — no definition, no theorem, no instance, not even a namespace
— and apart from this docstring consists of `import` lines alone, so it serves re-export and
nothing else: every name it puts in scope is declared in one of its imports, directly or
transitively. It bears the `IsingModel` library's own name, and importing it is the one step
that brings the development into scope. Lean requires the imports to open the file, so this
description follows them rather than heading them.

What those imports develop is the rigorous statistical mechanics of the Ising ferromagnet:
correlation inequalities (GKS, FKG, Lebowitz), random-current and switching representations,
Simon-Lieb and walk-sum decay estimates, Peierls contours and the low-temperature phase
transition, transfer matrices, cluster and Mayer expansions, Dobrushin uniqueness, Lee-Yang
and complex analyticity, and the passage from finite volumes to the infinite-volume limit
along exhaustions. Both layers of that development are reachable from here: the base layer,
whose subject is a graph on a finite vertex type, and the ambient layer, whose subject is a
finite volume `Λ : Finset V` inside an arbitrary `G : SimpleGraph V`.

One module of the library is not reached from here, `IsingModel.TestGenerators`: its small
explicit graphs and configuration enumerations serve the property tests of the separate
`test` library, which imports that module directly.
-/