Cut distance of a finite graphon

The complete graph on the uniform two-point carrier has cut distance 1/8 from the constant graphon 1/2 on any probability carrier. The distance is the cut norm of the difference kernel; its value follows by checking the finitely many rectangles of Fin 2.

Main results

• cutDist_finiteGraphGraphonOnFin_top_two_const_half — the exact distance 1/8.

@[simp]

theorem TauCeti.DenseGraphLimits.cutDist_finiteGraphGraphonOnFin_top_two_const_half {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : cutDist (finiteGraphGraphonOnFin ⊤) (Graphon.const μ ⟨2⁻¹, ⋯⟩) = 1 / 8

The complete graph on the uniform two-point carrier is at cut distance 1/8 from the constant graphon 1/2, whatever the probability carrier of the constant graphon.

The difference kernel is 1/2 on the two off-diagonal cells and -1/2 on the two diagonal cells, each of mass 1/4; an off-diagonal cell attains 1/8, and no rectangle does better.