Finite rows and incidence columns for floating rounding

Definition

erdos390_floating_rounding

by doctosil · Sep 16, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatoricserdos390rounding

For finite coordinate, row and column sets $A,R,C$ , a map $r:A\to R$ and an incidence relation $I\subseteq C\times A$ , define the row fiber $A_s=\{a:r(a)=s\}$ , the columns containing a coordinate $C_a=\{c:(c,a)\in I\}$ , and the real-valued incidence indicator $1_I(c,a)$ . These provide the interface for exact row sums and bounded column discrepancy in finite floating rounding.

Definition code

import Mathlib

namespace Erdos390.WholePaper

noncomputable section

def columnsContaining {A C : Type*} [Fintype C]
    (H : Finset C) (inc : C → A → Prop) (a : A) : Finset C := by
  classical
  exact H.filter fun c ↦ inc c a

def rowSet {A R : Type*} [Fintype A]
    (row : A → R) (r : R) : Finset A := by
  classical
  exact Finset.univ.filter fun a ↦ row a = r

def zeroOneColumn {A C : Type*} (inc : C → A → Prop) (c : C) (a : A) : ℝ := by
  classical
  exact if inc c a then 1 else 0

end
end Erdos390.WholePaper

Source

Shouqiao Wang, A Proposed Solution to Erdos Problem 390, Section 10, floating rounding; https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/FloatingRounding.lean

View graph