module module

`IndisputableMonolith.Mathematics.BipartiteDistanceSpectrum`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Mathematics.DistanceShellMultiplicity module_import

declarations in this module (16)

abbrev Point2 L28
abbrev Point4 L29
def crossDistSqSpectrum L32
def crossDistSpectrum L39
structure TwoChannelRangeExperiment L44
theorem crossDistSqSpectrum_card_le_pairs L55
def Erdos661Positive L66
def PlanarCrossSpectrumRigidity L77
def FixedCrossDistanceInFourSpace L89
def normSq L95
def normSqImage L99
def crossDifferenceSet L104
def crossNormSqAlphabet L109
structure GaussianLikeLattice L116
def ApproxContainedInGaussianLikeLattice L129
def PlanarNormFiberRigidityTarget L142