CubicPathwidth.T2.DegreeLabelsShell

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

import CubicPathwidth.T2.DefsB

/-!
# Outer-shell mass for degree-sensitive labels

Abstract data: a mass `ν : V → [0, ∞)` with `ν u = 1` at a source `u`, and
weights `c x ∈ [1/3, 1/2]` with `(d_x - 1) c x ≤ 1`, such that every vertex
`w ≠ u` has a *tight parent*: a neighbor `x` with `ν w = c x * ν x`. In the
application `ν = amp u ^ 2` and `c x = 1 / (d_x - 1)`.

For a vertex set `S` the boundary `bd S` consists of the vertices outside `S`
with a tight parent in `S`. For the super-level set `lvl t = {ν > t}` the
boundary mass `cutMass t` is the mass of a cut of a shortest-path tree.

* `bdMass_insert`: adding a boundary vertex does not increase the boundary
  mass (its tight children, other than its parent, carry at most its mass);
* `cutMass_mono`: `cutMass` is monotone on `[0, 1)`;
* `shell_le`: the shell `{θ ≤ ν < 3θ}` has mass at most `3 cutMass (4θ)`;
* `pack`: `J cutMass (4θ) ≤ ∑_{ν ≥ θ} ν` when `4^J θ < 1`, since the cuts
  at the levels `4^{j+1} θ` are pairwise disjoint.
-/

noncomputable section
open scoped BigOperators
open Classical

namespace CubicPathwidth
namespace T2
namespace DL

variable {n : ℕ} (G : SimpleGraph (Fin n)) (ν c : Fin n → ℝ)

/-- Vertices outside `S` with a tight parent in `S`. -/
def bd (S : Finset (Fin n)) : Finset (Fin n) :=
  Finset.univ.filter fun w => w ∉ S ∧ ∃ x ∈ S, G.Adj x w ∧ ν w = c x * ν x

def bdMass (S : Finset (Fin n)) : ℝ := ∑ w ∈ bd G ν c S, ν w

def UpClosed (S : Finset (Fin n)) : Prop := ∀ y ∈ S, ∀ z, ν y < ν z → z ∈ S

/-- Super-level set `{ν > t}`. -/
def lvl (t : ℝ) : Finset (Fin n) := Finset.univ.filter fun w => t < ν w

def cutMass (t : ℝ) : ℝ := bdMass G ν c (lvl ν t)

/-- Hypotheses on the abstract data. -/
structure Hyp (u : Fin n) : Prop where
  nonneg : ∀ w, 0 ≤ ν w
  root : ν u = 1
  c_lo : ∀ x, 1 / 3 ≤ c x
  c_hi : ∀ x, c x ≤ 1 / 2
  deg : ∀ x, ((G.degree x : ℝ) - 1) * c x ≤ 1
  parent : ∀ w, w ≠ u → ∃ x, G.Adj x w ∧ ν w = c x * ν x

variable {G ν c}

theorem sum_union_le_of_nonneg {s t : Finset (Fin n)} {f : Fin n → ℝ} (hf : ∀ i, 0 ≤ f i) :
    ∑ i ∈ s ∪ t, f i ≤ ∑ i ∈ s, f i + ∑ i ∈ t, f i := by
  have h := Finset.sum_union_inter (s₁ := s) (s₂ := t) (f := f)
  have h0 : 0 ≤ ∑ i ∈ s ∩ t, f i := Finset.sum_nonneg fun i _ => hf i
  linarith

theorem bdMass_insert {u : Fin n} (H : Hyp G ν c u) {S : Finset (Fin n)} {x p : Fin n}
    (hxS : x ∉ S) (hpS : p ∈ S) (hpx : G.Adj p x) (hx : ν x = c p * ν p) :
    bdMass G ν c (insert x S) ≤ bdMass G ν c S := by
  have hxbd : x ∈ bd G ν c S := by
    simp only [bd, Finset.mem_filter, Finset.mem_univ, true_and]
    exact ⟨hxS, p, hpS, hpx, hx⟩
  set K := ((G.neighborFinset x).erase p).filter (fun w => ν w = c x * ν x) with hK
  have hsub : bd G ν c (insert x S) ⊆ (bd G ν c S).erase x ∪ K := by
    intro w hw
    simp only [bd, Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_insert,
      not_or] at hw
    obtain ⟨⟨hwx, hwS⟩, y, hy, hyw, hwy⟩ := hw
    rcases hy with hy | hy
    · subst hy
      apply Finset.mem_union_right
      simp only [hK, Finset.mem_filter, Finset.mem_erase, SimpleGraph.mem_neighborFinset]
      exact ⟨⟨fun h => hwS (h ▸ hpS), hyw⟩, hwy⟩
    · apply Finset.mem_union_left
      simp only [Finset.mem_erase, bd, Finset.mem_filter, Finset.mem_univ, true_and]
      exact ⟨hwx, hwS, y, hy, hyw, hwy⟩
  have h1 := Finset.sum_le_sum_of_subset_of_nonneg hsub (fun w _ _ => H.nonneg w)
  have h2 := sum_union_le_of_nonneg (s := (bd G ν c S).erase x) (t := K) H.nonneg
  have h4 := Finset.sum_erase_eq_sub (f := ν) hxbd
  have h5 : ∑ w ∈ K, ν w = K.card * (c x * ν x) := by
    rw [Finset.sum_congr rfl (fun w hw => (Finset.mem_filter.mp hw).2), Finset.sum_const,
      nsmul_eq_mul]
  have hpN : p ∈ G.neighborFinset x := (G.mem_neighborFinset x p).mpr hpx.symm
  have h6 : (K.card : ℝ) ≤ (G.degree x : ℝ) - 1 := by
    have hc := Finset.card_le_card (Finset.filter_subset (fun w => ν w = c x * ν x)
      ((G.neighborFinset x).erase p))
    rw [Finset.card_erase_of_mem hpN, G.card_neighborFinset_eq_degree] at hc
    have hd : 1 ≤ G.degree x := by
      rw [← G.card_neighborFinset_eq_degree]
      exact Finset.card_pos.mpr ⟨p, hpN⟩
    have hc' : (K.card : ℝ) ≤ ((G.degree x - 1 : ℕ) : ℝ) := by exact_mod_cast hc
    rw [Nat.cast_sub hd] at hc'
    simpa using hc'
  have h7 := H.deg x
  have hcx : 0 ≤ c x := by linarith [H.c_lo x]
  have hνx := H.nonneg x
  have h8 := mul_le_mul_of_nonneg_right h6 (mul_nonneg hcx hνx)
  have h9 := mul_le_mul_of_nonneg_right h7 hνx
  unfold bdMass
  nlinarith

theorem bdMass_anti {u : Fin n} (H : Hyp G ν c u) : ∀ (N : ℕ) (S T : Finset (Fin n)),
    (T \ S).card = N → u ∈ S → UpClosed ν S → UpClosed ν T → S ⊆ T →
      (∀ z ∈ T, 0 < ν z) → bdMass G ν c T ≤ bdMass G ν c S := by
  intro N
  induction N with
  | zero =>
    intro S T hN _ _ _ hST _
    have hTS : T ⊆ S := by
      intro z hz
      by_contra h
      have hz' : z ∈ T \ S := Finset.mem_sdiff.mpr ⟨hz, h⟩
      rw [Finset.card_eq_zero] at hN
      simp [hN] at hz'
    rw [Finset.Subset.antisymm hST hTS]
  | succ N ih =>
    intro S T hN huS hS hT hST hpos
    have hne : (T \ S).Nonempty := by
      rw [← Finset.card_pos, hN]
      omega
    obtain ⟨x, hx, hmax⟩ := Finset.exists_max_image (T \ S) ν hne
    obtain ⟨hxT, hxS⟩ := Finset.mem_sdiff.mp hx
    have hxu : x ≠ u := fun h => hxS (h ▸ huS)
    obtain ⟨p, hpx, hxp⟩ := H.parent x hxu
    have hνx := hpos x hxT
    have hνp : ν x < ν p := by
      have h1 := H.c_hi p
      have h2 := H.nonneg p
      nlinarith
    have hpT : p ∈ T := hT x hxT p hνp
    have hpS : p ∈ S := by
      by_contra h
      have := hmax p (Finset.mem_sdiff.mpr ⟨hpT, h⟩)
      linarith
    have hS' : UpClosed ν (insert x S) := by
      intro y hy z hyz
      rcases Finset.mem_insert.mp hy with hy | hy
      · rw [hy] at hyz
        have hzT := hT x hxT z hyz
        by_contra hz
        have hzS : z ∉ S := fun h => hz (Finset.mem_insert_of_mem h)
        have := hmax z (Finset.mem_sdiff.mpr ⟨hzT, hzS⟩)
        linarith
      · exact Finset.mem_insert_of_mem (hS y hy z hyz)
    have hcard : (T \ insert x S).card = N := by
      rw [Finset.sdiff_insert, Finset.card_erase_of_mem hx, hN]
      rfl
    have := ih (insert x S) T hcard (Finset.mem_insert_of_mem huS) hS' hT
      (Finset.insert_subset hxT hST) hpos
    exact this.trans (bdMass_insert H hxS hpS hpx hxp)

theorem upClosed_lvl (t : ℝ) : UpClosed ν (lvl ν t) := by
  intro y hy z hyz
  simp only [lvl, Finset.mem_filter, Finset.mem_univ, true_and] at hy ⊢
  linarith

theorem cutMass_mono {u : Fin n} (H : Hyp G ν c u) {s t : ℝ} (hs : 0 ≤ s) (hst : s ≤ t)
    (ht : t < 1) : cutMass G ν c s ≤ cutMass G ν c t := by
  refine bdMass_anti H _ (lvl ν t) (lvl ν s) rfl ?_ (upClosed_lvl t) (upClosed_lvl s) ?_ ?_
  · simp [lvl, H.root, ht]
  · intro w hw
    simp only [lvl, Finset.mem_filter, Finset.mem_univ, true_and] at hw ⊢
    linarith
  · intro z hz
    simp only [lvl, Finset.mem_filter, Finset.mem_univ, true_and] at hz
    linarith

theorem mem_bd_lvl {w : Fin n} {t : ℝ} :
    w ∈ bd G ν c (lvl ν t) ↔ ν w ≤ t ∧ ∃ x, t < ν x ∧ G.Adj x w ∧ ν w = c x * ν x := by
  simp [bd, lvl]

theorem mem_cut {u : Fin n} (H : Hyp G ν c u) {w : Fin n} (hwu : w ≠ u) {t : ℝ}
    (h1 : ν w ≤ t) (h2 : t < 2 * ν w) : w ∈ bd G ν c (lvl ν t) := by
  obtain ⟨x, hx, hwx⟩ := H.parent w hwu
  refine mem_bd_lvl.mpr ⟨h1, x, ?_, hx, hwx⟩
  have := H.c_hi x
  have := H.nonneg x
  nlinarith

theorem cut_lower {u : Fin n} (H : Hyp G ν c u) {w : Fin n} {t : ℝ}
    (hw : w ∈ bd G ν c (lvl ν t)) : t < 3 * ν w := by
  obtain ⟨-, x, hx, -, hwx⟩ := mem_bd_lvl.mp hw
  have := H.c_lo x
  have := H.nonneg x
  nlinarith

theorem shell_le {u : Fin n} (H : Hyp G ν c u) {θ : ℝ} (hθ : 0 < θ) (h4 : 4 * θ < 1) :
    ∑ w ∈ Finset.univ.filter (fun w => θ ≤ ν w ∧ ν w < 3 * θ), ν w ≤
      3 * cutMass G ν c (4 * θ) := by
  have hsub : Finset.univ.filter (fun w => θ ≤ ν w ∧ ν w < 3 * θ) ⊆
      (bd G ν c (lvl ν θ) ∪ bd G ν c (lvl ν (2 * θ))) ∪ bd G ν c (lvl ν (4 * θ)) := by
    intro w hw
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hw
    obtain ⟨hw1, hw2⟩ := hw
    have hwu : w ≠ u := by
      intro h
      rw [h, H.root] at hw2
      linarith
    simp only [Finset.mem_union]
    by_cases ha : ν w ≤ θ
    · exact Or.inl (Or.inl (mem_cut H hwu ha (by linarith)))
    by_cases hb : ν w ≤ 2 * θ
    · exact Or.inl (Or.inr (mem_cut H hwu hb (by linarith)))
    · exact Or.inr (mem_cut H hwu (by linarith) (by linarith))
  have h1 := Finset.sum_le_sum_of_subset_of_nonneg hsub (fun w _ _ => H.nonneg w)
  have h2 := sum_union_le_of_nonneg (s := bd G ν c (lvl ν θ) ∪ bd G ν c (lvl ν (2 * θ)))
    (t := bd G ν c (lvl ν (4 * θ))) H.nonneg
  have h3 := sum_union_le_of_nonneg (s := bd G ν c (lvl ν θ))
    (t := bd G ν c (lvl ν (2 * θ))) H.nonneg
  have m1 := cutMass_mono H hθ.le (by linarith : θ ≤ 4 * θ) h4
  have m2 := cutMass_mono H (by linarith : (0 : ℝ) ≤ 2 * θ) (by linarith : 2 * θ ≤ 4 * θ) h4
  unfold cutMass bdMass at m1 m2 ⊢
  linarith

theorem no_common_cut {u : Fin n} (H : Hyp G ν c u) {a b : ℝ} (ha : 0 < a) (hab : 4 * a ≤ b)
    {w : Fin n} (hwa : w ∈ bd G ν c (lvl ν a)) (hwb : w ∈ bd G ν c (lvl ν b)) : False := by
  have h1 := (mem_bd_lvl.mp hwa).1
  have h2 := cut_lower H hwb
  linarith

theorem pack {u : Fin n} (H : Hyp G ν c u) {θ : ℝ} (hθ : 0 < θ) (J : ℕ)
    (hJ : (4 : ℝ) ^ J * θ < 1) :
    (J : ℝ) * cutMass G ν c (4 * θ) ≤ ∑ w ∈ Finset.univ.filter (fun w => θ ≤ ν w), ν w := by
  set lam : ℕ → ℝ := fun j => (4 : ℝ) ^ (j + 1) * θ with hlam
  have hpow : ∀ {i j : ℕ}, i ≤ j → (4 : ℝ) ^ i ≤ 4 ^ j := fun h =>
    pow_le_pow_right₀ (by norm_num) h
  have hlam_lt : ∀ j ∈ Finset.range J, lam j < 1 := by
    intro j hj
    have := hpow (show j + 1 ≤ J from Finset.mem_range.mp hj)
    have := mul_le_mul_of_nonneg_right this hθ.le
    simp only [hlam]
    linarith
  have hlam_ge : ∀ j, 4 * θ ≤ lam j := by
    intro j
    have := hpow (show 1 ≤ j + 1 by omega)
    have := mul_le_mul_of_nonneg_right this hθ.le
    simp only [hlam]
    simpa using this
  have hmono : ∀ j ∈ Finset.range J, cutMass G ν c (4 * θ) ≤ cutMass G ν c (lam j) :=
    fun j hj => cutMass_mono H (by linarith) (hlam_ge j) (hlam_lt j hj)
  have hdisj : (↑(Finset.range J) : Set ℕ).PairwiseDisjoint
      (fun j => bd G ν c (lvl ν (lam j))) := by
    intro i _ j _ hij
    simp only [Function.onFun]
    rw [Finset.disjoint_left]
    intro w hwi hwj
    have hθ4 : ∀ k, 0 < lam k := fun k => by simp only [hlam]; positivity
    rcases lt_or_gt_of_ne hij with h | h
    · have := mul_le_mul_of_nonneg_right (hpow (show i + 2 ≤ j + 1 by omega)) hθ.le
      exact no_common_cut H (hθ4 i) (by simp only [hlam]; rw [pow_succ] at this; linarith)
        hwi hwj
    · have := mul_le_mul_of_nonneg_right (hpow (show j + 2 ≤ i + 1 by omega)) hθ.le
      exact no_common_cut H (hθ4 j) (by simp only [hlam]; rw [pow_succ] at this; linarith)
        hwj hwi
  have hsub : (Finset.range J).biUnion (fun j => bd G ν c (lvl ν (lam j))) ⊆
      Finset.univ.filter (fun w => θ ≤ ν w) := by
    intro w hw
    obtain ⟨j, -, hwj⟩ := Finset.mem_biUnion.mp hw
    have := cut_lower H hwj
    have := hlam_ge j
    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
    linarith
  have hsum := Finset.sum_le_sum_of_subset_of_nonneg hsub (fun w _ _ => H.nonneg w)
  rw [Finset.sum_biUnion hdisj] at hsum
  have hcard := Finset.card_nsmul_le_sum (Finset.range J) (fun j => cutMass G ν c (lam j))
    (cutMass G ν c (4 * θ)) hmono
  rw [Finset.card_range, nsmul_eq_mul] at hcard
  unfold cutMass bdMass at hcard ⊢
  linarith

end DL
end T2
end CubicPathwidth