structure CellDecomposition.Line2 : Type

A line in ℝ²: a one-dimensional affine subspace, packaged with a proof that its direction has rank 1 and that its carrier set is nonempty.

• carrier : AffineSubspace ℝ (Fin 2 → ℝ)
• dim_eq : Module.finrank ℝ ↥self.carrier.direction = 1
• nonempty : (↑self.carrier).Nonempty

@[implicit_reducible]

instance CellDecomposition.instMembershipForallFinOfNatNatRealLine2 : Membership (Fin 2 → ℝ) Line2

Membership of a point in a Line2: belongs to the underlying affine subspace.

theorem CellDecomposition.polynomial_ham_sandwich_finite {ι : Type} [Fintype ι] (D : ℕ) : Fintype.card ι ≤ D ^ 2 → ∀ (S : ι → Finset (Fin 2 → ℝ)), ∃ (p : MvPolynomial (Fin 2) ℝ), p ≠ 0 ∧ p.totalDegree ≤ D ∧ (∀ (i : ι), {x ∈ S i | (MvPolynomial.eval x) p > 0}.card ≤ (S i).card / 2) ∧ ∀ (i : ι), {x ∈ S i | (MvPolynomial.eval x) p < 0}.card ≤ (S i).card / 2

Polynomial ham-sandwich theorem for finite sets in ℝ². Given at most D² finite sets S_i ⊆ ℝ², there is a nonzero polynomial p of total degree at most D such that for each i, both {x ∈ S_i : p(x) > 0} and {x ∈ S_i : p(x) < 0} contain at most half of S_i.

theorem CellDecomposition.bezout_line_polynomial (p : MvPolynomial (Fin 2) ℝ) (ℓ : Line2) : p ≠ 0 → (↑ℓ.carrier ∩ {x : Fin 2 → ℝ | (MvPolynomial.eval x) p = 0}).Finite ∧ (↑ℓ.carrier ∩ {x : Fin 2 → ℝ | (MvPolynomial.eval x) p = 0}).ncard ≤ p.totalDegree

Bézout-type bound: the intersection of a line ℓ ⊂ ℝ² with the zero set of a nonzero polynomial p is finite and has at most deg p points.

noncomputable def CellDecomposition.polyCell {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) (σ : Fin k → Bool) : Set (Fin 2 → ℝ)

The open cell {x : ∀ i, sign(polys i (x)) = σ i} cut out by a sign pattern σ : Fin k → Bool (with true meaning positive sign and false meaning negative sign).

def CellDecomposition.polyWall {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) : Set (Fin 2 → ℝ)

The "wall" ⋃_i Z(polys i): the union of the zero sets of the polynomials, separating the open cells polyCell polys σ.

noncomputable def CellDecomposition.signPatternCell (X : Finset (Fin 2 → ℝ)) {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) (σ : Fin k → Bool) : Finset (Fin 2 → ℝ)

The points of a finite set X ⊆ ℝ² lying in the open cell polyCell polys σ, returned as a Finset.

theorem CellDecomposition.polyCell_isOpen {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) (σ : Fin k → Bool) : IsOpen (polyCell polys σ)

Every polyCell is open, being a finite intersection of open half-spaces defined by polynomial inequalities.

theorem CellDecomposition.polyWall_isClosed {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) : IsClosed (polyWall polys)

The polynomial wall is closed, being a finite union of polynomial zero sets.

theorem CellDecomposition.polyWall_union_cells {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) : polyWall polys ∪ ⋃ (σ : Fin k → Bool), polyCell polys σ = Set.univ

The wall together with the union of all sign-pattern open cells covers ℝ².

theorem CellDecomposition.polyCell_pairwise_disjoint {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) : Pairwise fun (σ τ : Fin k → Bool) => Disjoint (polyCell polys σ) (polyCell polys τ)

Distinct sign patterns give disjoint open cells.

theorem CellDecomposition.polyCell_disjoint_wall {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) (σ : Fin k → Bool) : Disjoint (polyCell polys σ) (polyWall polys)

Each open cell is disjoint from the wall.

theorem CellDecomposition.polyWall_line_finite {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) (hne : ∀ (i : Fin k), polys i ≠ 0) (ℓ : Line2) : (↑ℓ.carrier ∩ polyWall polys).Finite

The intersection of a line with the wall of nonzero polynomials is finite, by Bézout applied to each polynomial.

theorem CellDecomposition.polyWall_line_ncard {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) (hne : ∀ (i : Fin k), polys i ≠ 0) (ℓ : Line2) : (↑ℓ.carrier ∩ polyWall polys).ncard ≤ ∑ i : Fin k, (polys i).totalDegree

Bézout bound: the number of intersection points of a line with the polynomial wall is at most ∑_i deg(polys i).

theorem CellDecomposition.signPatternCell_snoc_true_subset (X : Finset (Fin 2 → ℝ)) {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) (p : MvPolynomial (Fin 2) ℝ) (σ : Fin k → Bool) : signPatternCell X (Fin.snoc polys p) (Fin.snoc σ true) ⊆ {x ∈ signPatternCell X polys σ | (MvPolynomial.eval x) p > 0}

Inductive step: after appending a polynomial p and the sign true, the sign-pattern cell sits inside the previous cell intersected with {x : p(x) > 0}.

theorem CellDecomposition.signPatternCell_snoc_false_subset (X : Finset (Fin 2 → ℝ)) {k : ℕ} (polys : Fin k → MvPolynomial (Fin 2) ℝ) (p : MvPolynomial (Fin 2) ℝ) (σ : Fin k → Bool) : signPatternCell X (Fin.snoc polys p) (Fin.snoc σ false) ⊆ {x ∈ signPatternCell X polys σ | (MvPolynomial.eval x) p < 0}

Inductive step: after appending a polynomial p and the sign false, the sign-pattern cell sits inside the previous cell intersected with {x : p(x) < 0}.

theorem CellDecomposition.degree_bound_step (j : ℕ) : 2 ^ j ≤ (2 ^ ((j + 1) / 2)) ^ 2

Arithmetic estimate 2^j ≤ (2^{⌊(j+1)/2⌋})² used to control degrees at each bisection step.

theorem CellDecomposition.card_fin_bool_fun (k : ℕ) : Fintype.card (Fin k → Bool) = 2 ^ k

There are 2^k sign patterns in Fin k → Bool.

theorem CellDecomposition.degree_sum_bound_even (m : ℕ) : ∑ j ∈ Finset.range (2 * m), 2 ^ ((j + 1) / 2) = 3 * (2 ^ m - 1)

Closed-form for the cumulative degree sum at an even number of bisection steps: ∑_{j<2m} 2^{⌊(j+1)/2⌋} = 3(2^m − 1).

theorem CellDecomposition.degree_sum_bound (k : ℕ) : ∑ j ∈ Finset.range k, 2 ^ ((j + 1) / 2) ≤ 4 * 2 ^ (k / 2)

Cumulative degree bound after k bisection steps: ∑_{j<k} 2^{⌊(j+1)/2⌋} ≤ 4 · 2^{⌊k/2⌋}.

theorem CellDecomposition.two_pow_log_bound (s : ℕ) (hs : 1 ≤ s) : s ^ 2 ≤ 2 ^ (2 * Nat.log 2 s + 2)

For s ≥ 1, s² ≤ 2^{2 log₂ s + 2}. Used to relate the target parameter s to the chosen number of bisection steps k = 2 log₂ s + 2.

theorem CellDecomposition.two_pow_half_log_bound (s : ℕ) (hs : 1 ≤ s) : 2 ^ ((2 * Nat.log 2 s + 2) / 2) ≤ 2 * s

For s ≥ 1, 2^{⌊(2 log₂ s + 2) / 2⌋} ≤ 2s. Used to convert the O(2^{k/2}) degree bound into an O(s) bound.

theorem CellDecomposition.iterative_bisection (X : Finset (Fin 2 → ℝ)) (k : ℕ) : ∃ (polys : Fin k → MvPolynomial (Fin 2) ℝ), (∀ (i : Fin k), polys i ≠ 0) ∧ (∀ (i : Fin k), (polys i).totalDegree ≤ 2 ^ ((↑i + 1) / 2)) ∧ ∀ (σ : Fin k → Bool), (signPatternCell X polys σ).card ≤ X.card / 2 ^ k

Iterated polynomial ham-sandwich bisection. For any finite X ⊆ ℝ² and any k, there exist polynomials polys₀, …, polys_{k−1} (all nonzero) with deg(polys i) ≤ 2^{⌊(i+1)/2⌋} such that each of the 2^k sign-pattern cells contains at most |X| / 2^k points of X.

theorem CellDecomposition.cell_decomposition_lemma : ∃ (C : ℝ) (_ : C > 0), ∀ (X : Finset (Fin 2 → ℝ)) (s : ℕ), 1 ≤ s → ∃ (n : ℕ) (O : Fin n → Set (Fin 2 → ℝ)) (W : Set (Fin 2 → ℝ)), (∀ (i : Fin n), IsOpen (O i)) ∧ IsClosed W ∧ W ∪ ⋃ (i : Fin n), O i = Set.univ ∧ (Pairwise fun (i j : Fin n) => Disjoint (O i) (O j)) ∧ (∀ (i : Fin n), Disjoint (O i) W) ∧ (∀ (ℓ : Line2), (↑ℓ.carrier ∩ W).Finite ∧ ↑(↑ℓ.carrier ∩ W).ncard ≤ C * ↑s) ∧ ∀ (i : Fin n), ↑(↑X ∩ O i).ncard ≤ C * ↑X.card / ↑s ^ 2

Cell decomposition lemma (Szemerédi–Trotter). For any finite X ⊆ ℝ² and integer s ≥ 1, the plane decomposes as ℝ² = W ∪ ⋃ᵢ Oᵢ, with the Oᵢ pairwise disjoint open sets, W closed and disjoint from each Oᵢ, such that every line meets W in at most C s points and each Oᵢ contains at most C |X| / s² points of X. Obtained via iterated polynomial bisection.