Documentation
ConnesLean
Search
return to top
source
Imports
Init
ConnesLean.Common.Notation
ConnesLean.Stage1.Convolution
ConnesLean.Stage1.ConvolutionInnerProduct
ConnesLean.Stage1.DilationOperator
ConnesLean.Stage1.MultiplicativeHaar
ConnesLean.Stage1.UnitaryIdentity
ConnesLean.Stage2.ArchimedeanDistribution
ConnesLean.Stage2.ArchimedeanWeight
ConnesLean.Stage2.EnergyForm
ConnesLean.Stage2.LogCoordinates
ConnesLean.Stage2.PrimeDistribution
ConnesLean.Stage2.SupportDisjointness
ConnesLean.Stage2.TranslationOperator
ConnesLean.Stage4.MarkovProperty
ConnesLean.Stage4.MollificationConstancy
ConnesLean.Stage4.NormalContraction
ConnesLean.Stage4.NullOrConull
ConnesLean.Stage4.TranslationInvariance
ConnesLean.Stage5.ClosedForm
ConnesLean.Stage5.CompactEmbedding
ConnesLean.Stage5.CompactResolvent
ConnesLean.Stage5.FourierSymbol
ConnesLean.Stage5.SymbolLowerBound
ConnesLean.Stage6.ConstantInDomain
ConnesLean.Stage6.CrossVanishing
ConnesLean.Stage6.EnergyEquality
ConnesLean.Stage6.EnergyPositivity
ConnesLean.Stage6.IndicatorEnergy
ConnesLean.Stage6.InvarianceSplit
ConnesLean.Stage6.Irreducibility
ConnesLean.Stage6.NormInequality
ConnesLean.Stage7.GroundState
ConnesLean.Stage8.EvenGroundState
Imported by