Documentation

LeanPool.ErdosGinzburgZiv.Imports

return to top

source

Imports

Init
LeanPool.ErdosGinzburgZiv
LeanPool.ErdosGinzburgZiv.EGZ
LeanPool.ErdosGinzburgZiv.ErdosGinzburgZivPrime
LeanPool.ErdosGinzburgZiv.Solution
LeanPool.ErdosGinzburgZiv.ZakharovTheorem12
LeanPool.ErdosGinzburgZiv.EGZ.Asymptotics
LeanPool.ErdosGinzburgZiv.EGZ.BalancedCombination
LeanPool.ErdosGinzburgZiv.EGZ.BalancedRounding
LeanPool.ErdosGinzburgZiv.EGZ.Consistency
LeanPool.ErdosGinzburgZiv.EGZ.Convex
LeanPool.ErdosGinzburgZiv.EGZ.ConvexFlag
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition
LeanPool.ErdosGinzburgZiv.EGZ.MainTheorem
LeanPool.ErdosGinzburgZiv.EGZ.TheoremOneTwelve
LeanPool.ErdosGinzburgZiv.EGZ.Balanced.Existence
LeanPool.ErdosGinzburgZiv.EGZ.Balanced.IntegerApproximation
LeanPool.ErdosGinzburgZiv.EGZ.Balanced.RationalApproximation
LeanPool.ErdosGinzburgZiv.EGZ.Balanced.RationalCoefficients
LeanPool.ErdosGinzburgZiv.EGZ.Balanced.RealCoefficients
LeanPool.ErdosGinzburgZiv.EGZ.Consistency.ConvexHullClosure
LeanPool.ErdosGinzburgZiv.EGZ.Consistency.FaceFlagHellyBound
LeanPool.ErdosGinzburgZiv.EGZ.Consistency.LocalToCumulative
LeanPool.ErdosGinzburgZiv.EGZ.Consistency.PropositionSevenOne
LeanPool.ErdosGinzburgZiv.EGZ.Consistency.TheoremOneTwelve
LeanPool.ErdosGinzburgZiv.EGZ.Convex.AffineLattice
LeanPool.ErdosGinzburgZiv.EGZ.Convex.Coordinate
LeanPool.ErdosGinzburgZiv.EGZ.Convex.FaceCombinations
LeanPool.ErdosGinzburgZiv.EGZ.Convex.Faces
LeanPool.ErdosGinzburgZiv.EGZ.Convex.FiniteHull
LeanPool.ErdosGinzburgZiv.EGZ.Convex.HollowBound
LeanPool.ErdosGinzburgZiv.EGZ.Convex.HollowReduction
LeanPool.ErdosGinzburgZiv.EGZ.Convex.Homogenization
LeanPool.ErdosGinzburgZiv.EGZ.Convex.LeastFaceInterior
LeanPool.ErdosGinzburgZiv.EGZ.Convex.Polytope
LeanPool.ErdosGinzburgZiv.EGZ.Convex.VertexHull
LeanPool.ErdosGinzburgZiv.EGZ.Convex.VertexWeights
LeanPool.ErdosGinzburgZiv.EGZ.ConvexFlag.Basic
LeanPool.ErdosGinzburgZiv.EGZ.ConvexFlag.Centerpoint
LeanPool.ErdosGinzburgZiv.EGZ.ConvexFlag.ConvexHull
LeanPool.ErdosGinzburgZiv.EGZ.ConvexFlag.FaceModel
LeanPool.ErdosGinzburgZiv.EGZ.ConvexFlag.Helly
LeanPool.ErdosGinzburgZiv.EGZ.ConvexFlag.WeakHull
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.AffineImages
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.AugmentedCompleteness
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.AugmentedCoordinates
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.AugmentedDecomposition
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.AugmentedDiagram
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.AugmentedRepresentation
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Basic
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.BoundedRun
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.CenteredLift
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.CenteredPolytope
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Cleanup
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.CommonMeasure
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.CompleteBounds
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.CompleteLevels
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.CompletePreparation
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.CompleteRefinement
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Completeness
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Conclusion
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.ConclusionBridge
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Construction
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Existence
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.FaceLevels
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.FaceMassChain
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.FacePreservation
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.FaceRefinement
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.FaceSelection
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.FaceSupport
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.FaceSurvival
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.FinalConstruction
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.GapCleanup
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.GapProgress
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Initialization
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.IntervalCapacity
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.IterationBounds
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.IterationColorCapacity
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.IterationCompleteCapacity
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.IterationConstants
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.IterationEvents
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.IterationFaceCapacity
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.IterationGapCapacity
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.IterationIntervalBounds
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.IterationLineages
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.IterationTermination
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.LargeFaceGeometry
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.LargeFaceSequence
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.LatticeCoordinates
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.LatticeTransition
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.LevelInjectivity
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Levels
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.LiftedMass
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.LineageMassMaps
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.LineageOperations
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Lineages
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.LocalToCumulative
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.LocalizedPruning
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.LowerTransfer
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Mass
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.MinimalLattice
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.MinimalParameters
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.MinimalRepresentation
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Minimalization
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.ModularRank
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.NodeMassMap
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.NodeMassMapLevels
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.NormalizedComplete
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.NormalizedFace
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.NormalizedGap
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.NormalizedMassMaps
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.NormalizedOperations
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.OperationLevels
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.OperationMassMaps
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Parameters
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.PruningData
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.PruningStability
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Pullback
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.QuotientMass
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.RealSupportRank
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Rebuild
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.RechartDecomposition
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.RechartFlag
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.RechartMass
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.RechartPreservation
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.RechartRepresentation
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.ReducedRepresentative
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Reduction
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.RefinementGrowth
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.RefinementProgress
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Restrict
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.ScalarExtension
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.SlabPruning
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.StoppedLineages
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.SupportDecomposition
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.SupportDiagram
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.SupportDiagramRepresentation
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.SupportParameters
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.SupportRechartMass
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.SupportRepresentation
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Termination
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Thickness
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.ThinDirections
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.TwoLayer
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.UniformCompleteRefinement
LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.WeightedIncidence
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.Affine
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.AffineApplication
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.AffineRelations
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.Basic
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.CharacterLinear
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.CharacterSum
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.DilatedGrowth
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.ExchangeCompletion
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.ExchangePattern
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.ExchangeResources
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.FibreSlots
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.FiniteProbability
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.FourierEnergy
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.GrowthIteration
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.PrescribedCounts
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.Relative
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.RelativeConcentration
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.RelativeProof
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.ResourceCompletion
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.SampleAvailability
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.SampleDistribution
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.Sampling
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.SetGrowth
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.SlabArithmetic
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.Subweights
LeanPool.ErdosGinzburgZiv.EGZ.Expansion.ThickSupport
LeanPool.ErdosGinzburgZiv.EGZ.Main.Assembly
LeanPool.ErdosGinzburgZiv.EGZ.Main.Centerpoint
LeanPool.ErdosGinzburgZiv.EGZ.Main.Coefficients
LeanPool.ErdosGinzburgZiv.EGZ.Main.Input
LeanPool.ErdosGinzburgZiv.EGZ.Main.Interior
LeanPool.ErdosGinzburgZiv.EGZ.Main.Parameters
LeanPool.ErdosGinzburgZiv.EGZ.Main.Selection
LeanPool.ErdosGinzburgZiv.EGZ.Main.UpperBound
LeanPool.ErdosGinzburgZiv.EGZ.Polynomial.HollowBound
LeanPool.ErdosGinzburgZiv.EGZ.ZeroSum.Basic
LeanPool.ErdosGinzburgZiv.EGZ.ZeroSum.Constants
LeanPool.ErdosGinzburgZiv.EGZ.ZeroSum.DimensionOne
LeanPool.ErdosGinzburgZiv.EGZ.ZeroSum.Multiplicity

Imported by