CubicPathwidth.CutSweep.SweepGrid

Source file CubicPathwidth/CutSweep/SweepGrid.lean of the Lean project (how it is built).

import CubicPathwidth.CutSweep.Defs

/-!
# Deterministic grid comparison for threshold counts (`sec:warmup`, "A grid of thresholds")

Every count used in the sweep is a *pair count*
`pairCount G y S = ∑_v #{u ∈ N(v) : (y v, y u) ∈ S}` for a set `S ⊆ ℝ × ℝ`.
The threshold count is the pair count of `crossSet t = (-∞, t] × (t, ∞)`
(each crossing edge counted at its lower end). The grid comparison is then an
inclusion of sets in the plane:

* `a ≤ t < b`: `crossSet t ⊆ crossSet a ∪ cellSet a b`, so
  `e_t ≤ e_a + pairCount (cellSet a b)`, and `pairCount (cellSet a b)` is at most
  three times the number of labels in `(a, b]`;
* `t ≤ -T`: `crossSet t ⊆ lowSet T` (the lower end is at most `-T`);
* `T ≤ t`: `crossSet t ⊆ highSet T` (the upper end is above `T`).
-/

noncomputable section
open Classical

namespace CubicPathwidth
namespace CutSweep

variable {n : ℕ}

/-- `∑_v #{u ∈ N(v) : (y v, y u) ∈ S}`. -/
def pairCount (G : SimpleGraph (Fin n)) (y : Fin n → ℝ) (S : Set (ℝ × ℝ)) : ℕ :=
  ∑ v, ((G.neighborFinset v).filter fun u => (y v, y u) ∈ S).card

/-- Lower end at most `t`, upper end above `t`. -/
def crossSet (t : ℝ) : Set (ℝ × ℝ) := Set.Iic t ×ˢ Set.Ioi t

/-- Lower end in the cell `(a, b]`. -/
def cellSet (a b : ℝ) : Set (ℝ × ℝ) := Set.Ioc a b ×ˢ Set.univ

/-- Lower end at most `-T`. -/
def lowSet (T : ℝ) : Set (ℝ × ℝ) := Set.Iic (-T) ×ˢ Set.univ

/-- Upper end above `T`. -/
def highSet (T : ℝ) : Set (ℝ × ℝ) := Set.univ ×ˢ Set.Ioi T

theorem measurableSet_crossSet (t : ℝ) : MeasurableSet (crossSet t) :=
  measurableSet_Iic.prod measurableSet_Ioi

theorem measurableSet_cellSet (a b : ℝ) : MeasurableSet (cellSet a b) :=
  measurableSet_Ioc.prod MeasurableSet.univ

theorem measurableSet_lowSet (T : ℝ) : MeasurableSet (lowSet T) :=
  measurableSet_Iic.prod MeasurableSet.univ

theorem measurableSet_highSet (T : ℝ) : MeasurableSet (highSet T) :=
  MeasurableSet.univ.prod measurableSet_Ioi

variable (G : SimpleGraph (Fin n))

/-- The threshold count counts every crossing edge at its lower end. -/
theorem crossCount_eq_pairCount (y : Fin n → ℝ) (t : ℝ) :
    crossCount G y t = pairCount G y (crossSet t) := by
  unfold crossCount cutSize pairCount levelSet
  rw [Finset.sum_filter]
  refine Finset.sum_congr rfl fun v _ => ?_
  by_cases hv : y v ≤ t
  · simp only [hv, ↓reduceIte]
    congr 1
    ext u
    simp [crossSet, hv]
  · simp only [hv, ↓reduceIte]
    symm
    rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff]
    intro u _ h
    exact hv h.1

theorem pairCount_mono (y : Fin n → ℝ) {S S' : Set (ℝ × ℝ)} (h : S ⊆ S') :
    pairCount G y S ≤ pairCount G y S' := by
  unfold pairCount
  refine Finset.sum_le_sum fun v _ => Finset.card_le_card ?_
  intro u hu
  simp only [Finset.mem_filter] at hu ⊢
  exact ⟨hu.1, h hu.2⟩

theorem pairCount_le_union (y : Fin n → ℝ) {S S₁ S₂ : Set (ℝ × ℝ)} (h : S ⊆ S₁ ∪ S₂) :
    pairCount G y S ≤ pairCount G y S₁ + pairCount G y S₂ := by
  unfold pairCount
  rw [← Finset.sum_add_distrib]
  refine Finset.sum_le_sum fun v _ => ?_
  refine (Finset.card_le_card ?_).trans (Finset.card_union_le _ _)
  intro u hu
  simp only [Finset.mem_filter, Finset.mem_union] at hu ⊢
  rcases h hu.2 with h1 | h2
  · exact Or.inl ⟨hu.1, h1⟩
  · exact Or.inr ⟨hu.1, h2⟩

theorem crossSet_subset_grid {a t b : ℝ} (hat : a ≤ t) (htb : t < b) :
    crossSet t ⊆ crossSet a ∪ cellSet a b := by
  rintro ⟨p, q⟩ ⟨hp, hq⟩
  simp only [Set.mem_Iic, Set.mem_Ioi] at hp hq
  by_cases hpa : p ≤ a
  · exact Or.inl ⟨hpa, show a < q by linarith⟩
  · exact Or.inr ⟨⟨not_le.mp hpa, by linarith⟩, Set.mem_univ _⟩

theorem crossSet_subset_low {t T : ℝ} (ht : t ≤ -T) : crossSet t ⊆ lowSet T := by
  rintro ⟨p, q⟩ ⟨hp, -⟩
  exact ⟨show p ≤ -T from le_trans hp ht, Set.mem_univ _⟩

theorem crossSet_subset_high {t T : ℝ} (ht : T ≤ t) : crossSet t ⊆ highSet T := by
  rintro ⟨p, q⟩ ⟨-, hq⟩
  exact ⟨Set.mem_univ _, show T < q from lt_of_le_of_lt ht hq⟩

/-- Grid step: `e_t ≤ e_a + pairCount (cellSet a b)` for `a ≤ t < b`. -/
theorem crossCount_le_grid (y : Fin n → ℝ) {a t b : ℝ} (hat : a ≤ t) (htb : t < b) :
    crossCount G y t ≤ crossCount G y a + pairCount G y (cellSet a b) := by
  rw [crossCount_eq_pairCount, crossCount_eq_pairCount]
  exact pairCount_le_union G y (crossSet_subset_grid hat htb)

theorem crossCount_le_low (y : Fin n → ℝ) {t T : ℝ} (ht : t ≤ -T) :
    crossCount G y t ≤ pairCount G y (lowSet T) := by
  rw [crossCount_eq_pairCount]
  exact pairCount_mono G y (crossSet_subset_low ht)

theorem crossCount_le_high (y : Fin n → ℝ) {t T : ℝ} (ht : T ≤ t) :
    crossCount G y t ≤ pairCount G y (highSet T) := by
  rw [crossCount_eq_pairCount]
  exact pairCount_mono G y (crossSet_subset_high ht)

/-- Every `t ∈ [-T, T)` lies in a grid cell `[-T + j/K, -T + (j+1)/K)` with
`j < 2TK`. -/
theorem exists_grid_index {T K : ℕ} (hK : 0 < K) {t : ℝ} (h1 : -(T : ℝ) ≤ t) (h2 : t < T) :
    ∃ j < 2 * T * K, -(T : ℝ) + j / K ≤ t ∧ t < -(T : ℝ) + (j + 1) / K := by
  have hK' : (0 : ℝ) < K := by exact_mod_cast hK
  set s := (t + T) * K with hs
  have hs0 : 0 ≤ s := by rw [hs]; nlinarith
  refine ⟨⌊s⌋₊, ?_, ?_, ?_⟩
  · have : s < 2 * T * K := by rw [hs]; nlinarith
    have h := Nat.floor_lt hs0 |>.mpr (by exact_mod_cast this : s < ((2 * T * K : ℕ) : ℝ))
    exact h
  · have h := Nat.floor_le hs0
    have : (⌊s⌋₊ : ℝ) / K ≤ t + T := by rw [div_le_iff₀ hK']; linarith
    linarith
  · have h := Nat.lt_floor_add_one s
    have : t + T < ((⌊s⌋₊ : ℝ) + 1) / K := by rw [lt_div_iff₀ hK']; linarith
    linarith

end CutSweep
end CubicPathwidth
Back to top