CubicPathwidth.EndpointTransfer

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

import CubicPathwidth.Completion

/-!
# Separate cut and distinct-endpoint coefficients (T18-F)

The proved cut gluing `pathwidth_of_cut_endpoint_bounds` uses, on each side,
the set of DISTINCT boundary endpoints `(edges G A).image Prod.fst` (resp.
`Prod.snd`), and the cut size only as the connector width.  The existing
coefficient step bounds the endpoint counts by the cut size.  Here the two
are controlled by separate coefficients `κ` (cut) and `ξ` (endpoints per side).

Main results:
* `endpoint_coefficient_step`: from a uniform pathwidth coefficient `b < 1/3`
  and a `(κ, ξ)` partition family, the coefficient `max κ (ξ + (1/2 - 3ξ) b)`.
* `endpoint_transfer`: for `0 ≤ κ < 1/6`, `0 ≤ ξ ≤ 1/6`, the coefficient
  `max κ (2ξ/(1+6ξ))`.
* `bisection_transfer`: for every `0 ≤ c < 1/6`, a uniform bisection
  coefficient `c` gives the pathwidth coefficient `2c/(1+6c)` (the general
  parameter version of the project's coefficient step).
-/

noncomputable section
namespace CubicPathwidth
open CutConnector SectionDecomposition

/-- A uniform family of bisections with cut coefficient `κ` and at most
`(ξ+ε)n` distinct boundary endpoints on EACH side. -/
def UniformEndpointPartitionBound (κ ξ : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
    ∀ G : SimpleGraph (Fin n), IsSubcubic G →
      ∃ A : Finset (Fin n), IsBisection A ∧
        (crossingEdges G A : ℝ) ≤ (κ + ε) * (n : ℝ) ∧
        ((((edges G A).image Prod.fst).card : ℕ) : ℝ) ≤ (ξ + ε) * (n : ℝ) ∧
        ((((edges G A).image Prod.snd).card : ℕ) : ℝ) ≤ (ξ + ε) * (n : ℝ)

theorem uniformBisection_of_partition {κ ξ : ℝ} (h : UniformEndpointPartitionBound κ ξ) :
    UniformBisectionBound κ := by
  intro ε hε
  obtain ⟨N, hN⟩ := h ε hε
  refine ⟨N, fun n hn G hG => ?_⟩
  obtain ⟨A, hA, hc, -, -⟩ := hN n hn G hG
  exact ⟨A, hA, hc⟩

/-- Distinct endpoints never exceed the cut size, so a bisection coefficient
`c` gives a partition family with `κ = ξ = c`. -/
theorem partition_of_bisection {c : ℝ} (h : UniformBisectionBound c) :
    UniformEndpointPartitionBound c c := by
  classical
  intro ε hε
  obtain ⟨N, hN⟩ := h ε hε
  refine ⟨N, fun n hn G hG => ?_⟩
  obtain ⟨A, hA, hc⟩ := hN n hn G hG
  have hX : (((edges G A).image Prod.fst).card : ℝ) ≤ crossingEdges G A := by
    exact_mod_cast (Finset.card_image_le).trans_eq (edges_card G A)
  have hY : (((edges G A).image Prod.snd).card : ℝ) ≤ crossingEdges G A := by
    exact_mod_cast (Finset.card_image_le).trans_eq (edges_card G A)
  exact ⟨A, hA, hc, hX.trans hc, hY.trans hc⟩

private theorem side_estimate_xi (b ξ ε n m x : ℝ)
    (hb : 0 ≤ b) (hb' : b ≤ 1 / 3) (_hξ0 : 0 ≤ ξ) (hξ : ξ ≤ 1 / 6)
    (hε : 0 < ε) (hn : 0 ≤ n)
    (hm : m ≤ n) (hhalf : 2 * m ≤ n + 1)
    (hx : x ≤ (ξ + ε / 4) * n) (hlarge : 1 ≤ ε * n) :
    max x (b * m + (1 - 3 * b) * x) + (ε / 4) * m ≤
      (ξ + (1 / 2 - 3 * ξ) * b + ε) * n := by
  have hd : 0 ≤ 1 - 3 * b := by linarith
  have hxm := mul_le_mul_of_nonneg_left hx hd
  have hbm := mul_le_mul_of_nonneg_left hhalf hb
  have hem := mul_le_mul_of_nonneg_left hm (by linarith : 0 ≤ ε / 4)
  have hlam : 0 ≤ (1 / 2 - 3 * ξ) * b := mul_nonneg (by linarith) hb
  have hlamn : 0 ≤ (1 / 2 - 3 * ξ) * b * n := mul_nonneg hlam hn
  have hbe : 0 ≤ b * (ε * n) := mul_nonneg hb (by nlinarith)
  have hen : 0 ≤ ε * n := by nlinarith
  apply (le_sub_iff_add_le).mp
  apply max_le
  · nlinarith
  · nlinarith

/-- One coefficient step with separate cut and endpoint coefficients. -/
theorem endpoint_coefficient_step (κ ξ b : ℝ) (hξ0 : 0 ≤ ξ) (hξ : ξ ≤ 1 / 6)
    (hb : 0 ≤ b) (hb' : b < 1 / 3)
    (hpart : UniformEndpointPartitionBound κ ξ) (hpw : UniformPathwidthBound b) :
    UniformPathwidthBound (max κ (ξ + (1 / 2 - 3 * ξ) * b)) := by
  classical
  have hend : UniformEndpointBound b := boundaryTransfer b hb hb' hpw
  intro ε hε
  have hε4 : 0 < ε / 4 := by linarith
  obtain ⟨Nc, hNc⟩ := hpart (ε / 4) hε4
  obtain ⟨Ne, hNe⟩ := hend (ε / 4) hε4
  obtain ⟨M, hM⟩ := exists_nat_ge (1 / ε)
  refine ⟨max Nc (max (2 * Ne + 2) M), ?_⟩
  intro n hn G hG
  have hnC : Nc ≤ n := (le_max_left _ _).trans hn
  have hnE : 2 * Ne + 2 ≤ n := (le_trans (le_max_left _ _) (le_max_right _ _)).trans hn
  have hnM : M ≤ n := (le_trans (le_max_right _ _) (le_max_right _ _)).trans hn
  have hlarge : (1 : ℝ) ≤ ε * (n : ℝ) := by
    have hmn : (M : ℝ) ≤ n := by exact_mod_cast hnM
    have h := (div_le_iff₀ hε).mp (hM.trans hmn)
    nlinarith
  obtain ⟨A, hbal, hcut, hXreal, hYreal⟩ := hNc n hnC G hG
  let B := Finset.univ \ A
  let X := (edges G A).image Prod.fst
  let Y := (edges G A).image Prod.snd
  have hBcard : B.card = n - A.card := by
    simpa [B] using Finset.card_sdiff_of_subset (Finset.subset_univ A)
  have hsum : A.card + B.card = n := by
    simpa [B, Nat.add_comm] using Finset.card_sdiff_add_card_eq_card (Finset.subset_univ A)
  have hbalanced : A.card ≤ B.card + 1 ∧ B.card ≤ A.card + 1 := by
    simpa only [IsBisection, ← hBcard] using hbal
  have hAmin : Ne ≤ A.card := by omega
  have hBmin : Ne ≤ B.card := by omega
  have hAn : A.card ≤ n := by omega
  have hBn : B.card ≤ n := by omega
  have hAhalf : 2 * A.card ≤ n + 1 := by omega
  have hBhalf : 2 * B.card ≤ n + 1 := by omega
  have hXsub : X ⊆ A := left_subset G A
  have hYsub : Y ⊆ B := by
    intro v hv
    exact Finset.mem_sdiff.mpr ⟨Finset.mem_univ _, right_not_mem G A hv⟩
  have hleft := hNe A.card hAmin (inducedOnFin G A) (inducedOnFin_subcubic hG A)
    (boundaryPreimage A X)
  have hright := hNe B.card hBmin (inducedOnFin G B) (inducedOnFin_subcubic hG B)
    (boundaryPreimage B Y)
  rw [boundaryPreimage_card A X hXsub] at hleft
  rw [boundaryPreimage_card B Y hYsub] at hright
  have hglue := pathwidth_of_cut_endpoint_bounds G A hleft hright
  apply hglue.mono
  have hSA := side_estimate_xi b ξ ε n A.card X.card hb hb'.le hξ0 hξ hε (Nat.cast_nonneg n)
    (by exact_mod_cast hAn) (by exact_mod_cast hAhalf) hXreal hlarge
  have hSB := side_estimate_xi b ξ ε n B.card Y.card hb hb'.le hξ0 hξ hε (Nat.cast_nonneg n)
    (by exact_mod_cast hBn) (by exact_mod_cast hBhalf) hYreal hlarge
  have hmaxR : (ξ + (1 / 2 - 3 * ξ) * b + ε) * (n : ℝ) ≤
      (max κ (ξ + (1 / 2 - 3 * ξ) * b) + ε) * (n : ℝ) := by
    apply mul_le_mul_of_nonneg_right _ (Nat.cast_nonneg n)
    linarith [le_max_right κ (ξ + (1 / 2 - 3 * ξ) * b)]
  have hmaxK : (κ + ε / 4) * (n : ℝ) ≤ (max κ (ξ + (1 / 2 - 3 * ξ) * b) + ε) * (n : ℝ) := by
    apply mul_le_mul_of_nonneg_right _ (Nat.cast_nonneg n)
    linarith [le_max_left κ (ξ + (1 / 2 - 3 * ξ) * b)]
  apply max_le
  · apply max_le
    · exact hSA.trans hmaxR
    · exact hSB.trans hmaxR
  · exact hcut.trans hmaxK

/-- The contraction map of the transfer. -/
def endpointMap (κ ξ b : ℝ) : ℝ := max κ (ξ + (1 / 2 - 3 * ξ) * b)

/-- Iterates of the transfer from the start value `b0`. -/
def endpointIter (κ ξ b0 : ℝ) : ℕ → ℝ
  | 0 => b0
  | j + 1 => endpointMap κ ξ (endpointIter κ ξ b0 j)

/-- The fixed point `max κ (2ξ/(1+6ξ))`. -/
def endpointFixed (κ ξ : ℝ) : ℝ := max κ (2 * ξ / (1 + 6 * ξ))

theorem endpointMap_range (κ ξ b : ℝ) (hκ0 : 0 ≤ κ) (hκ : κ < 1 / 3)
    (_hξ0 : 0 ≤ ξ) (hξ : ξ ≤ 1 / 6) (_hb : 0 ≤ b) (hb' : b < 1 / 3) :
    0 ≤ endpointMap κ ξ b ∧ endpointMap κ ξ b < 1 / 3 := by
  unfold endpointMap
  constructor
  · exact le_trans hκ0 (le_max_left _ _)
  · apply max_lt hκ
    have hl : 0 ≤ 1 / 2 - 3 * ξ := by linarith
    have := mul_le_mul_of_nonneg_left hb'.le hl
    nlinarith

theorem endpointIter_range (κ ξ b0 : ℝ) (hκ0 : 0 ≤ κ) (hκ : κ < 1 / 3)
    (hξ0 : 0 ≤ ξ) (hξ : ξ ≤ 1 / 6) (hb0 : 0 ≤ b0) (hb0' : b0 < 1 / 3) :
    ∀ j, 0 ≤ endpointIter κ ξ b0 j ∧ endpointIter κ ξ b0 j < 1 / 3 := by
  intro j
  induction j with
  | zero => exact ⟨hb0, hb0'⟩
  | succ j ih => exact endpointMap_range κ ξ _ hκ0 hκ hξ0 hξ ih.1 ih.2

theorem endpointFixed_isFixed (κ ξ : ℝ) (hξ0 : 0 ≤ ξ) (hξ : ξ ≤ 1 / 6) :
    endpointMap κ ξ (endpointFixed κ ξ) = endpointFixed κ ξ := by
  unfold endpointMap endpointFixed
  have hpos : 0 < 1 + 6 * ξ := by linarith
  set β := 2 * ξ / (1 + 6 * ξ) with hβ
  have hβeq : ξ + (1 / 2 - 3 * ξ) * β = β := by
    rw [hβ]; field_simp; ring
  rcases le_total κ β with h | h
  · rw [max_eq_right h, hβeq, max_eq_right h]
  · rw [max_eq_left h]
    have hl : 0 ≤ 1 / 2 - 3 * ξ := by linarith
    have hle : ξ + (1 / 2 - 3 * ξ) * κ ≤ κ := by
      have h1 : (1 / 2 - 3 * ξ) * β ≤ (1 / 2 - 3 * ξ) * κ := mul_le_mul_of_nonneg_left h hl
      -- ξ = β - λβ = (1-λ)β ≤ (1-λ)κ
      nlinarith [hβeq]
    exact max_eq_left hle

theorem endpointMap_lipschitz (κ ξ a b : ℝ) (_hξ0 : 0 ≤ ξ) (hξ : ξ ≤ 1 / 6) :
    |endpointMap κ ξ a - endpointMap κ ξ b| ≤ (1 / 2 - 3 * ξ) * |a - b| := by
  unfold endpointMap
  have hl : 0 ≤ 1 / 2 - 3 * ξ := by linarith
  have key : |max κ (ξ + (1 / 2 - 3 * ξ) * a) - max κ (ξ + (1 / 2 - 3 * ξ) * b)| ≤
      |(ξ + (1 / 2 - 3 * ξ) * a) - (ξ + (1 / 2 - 3 * ξ) * b)| := by
    rw [max_comm κ (ξ + (1 / 2 - 3 * ξ) * a), max_comm κ (ξ + (1 / 2 - 3 * ξ) * b)]
    exact abs_max_sub_max_le_abs _ _ κ
  calc |max κ (ξ + (1 / 2 - 3 * ξ) * a) - max κ (ξ + (1 / 2 - 3 * ξ) * b)|
      ≤ |(ξ + (1 / 2 - 3 * ξ) * a) - (ξ + (1 / 2 - 3 * ξ) * b)| := key
    _ = (1 / 2 - 3 * ξ) * |a - b| := by
        rw [show (ξ + (1 / 2 - 3 * ξ) * a) - (ξ + (1 / 2 - 3 * ξ) * b) =
          (1 / 2 - 3 * ξ) * (a - b) by ring, abs_mul, abs_of_nonneg hl]

theorem endpointIter_close (κ ξ b0 : ℝ) (hξ0 : 0 ≤ ξ) (hξ : ξ ≤ 1 / 6) :
    ∀ j, |endpointIter κ ξ b0 j - endpointFixed κ ξ| ≤
      (1 / 2 - 3 * ξ) ^ j * |b0 - endpointFixed κ ξ| := by
  intro j
  induction j with
  | zero => simp [endpointIter]
  | succ j ih =>
    have hl : 0 ≤ 1 / 2 - 3 * ξ := by linarith
    calc |endpointIter κ ξ b0 (j + 1) - endpointFixed κ ξ|
        = |endpointMap κ ξ (endpointIter κ ξ b0 j) -
            endpointMap κ ξ (endpointFixed κ ξ)| := by
          rw [endpointFixed_isFixed κ ξ hξ0 hξ]; rfl
      _ ≤ (1 / 2 - 3 * ξ) * |endpointIter κ ξ b0 j - endpointFixed κ ξ| :=
          endpointMap_lipschitz κ ξ _ _ hξ0 hξ
      _ ≤ (1 / 2 - 3 * ξ) * ((1 / 2 - 3 * ξ) ^ j * |b0 - endpointFixed κ ξ|) :=
          mul_le_mul_of_nonneg_left ih hl
      _ = (1 / 2 - 3 * ξ) ^ (j + 1) * |b0 - endpointFixed κ ξ| := by ring

/-- Main transfer: a `(κ, ξ)` partition family gives the pathwidth coefficient
`max κ (2ξ/(1+6ξ))`.  The start value `2κ` comes from the proved bootstrap. -/
theorem endpoint_transfer (κ ξ : ℝ) (hκ0 : 0 ≤ κ) (hκ : κ < 1 / 6)
    (hξ0 : 0 ≤ ξ) (hξ : ξ ≤ 1 / 6) (hpart : UniformEndpointPartitionBound κ ξ) :
    UniformPathwidthBound (endpointFixed κ ξ) := by
  have hstart : UniformPathwidthBound (2 * κ) :=
    uniformPathwidthBound_twice_of_bisection hκ0 (uniformBisection_of_partition hpart)
  have hb0 : 0 ≤ 2 * κ := by linarith
  have hb0' : 2 * κ < 1 / 3 := by linarith
  have hrange := endpointIter_range κ ξ (2 * κ) hκ0 (by linarith) hξ0 hξ hb0 hb0'
  have hiter : ∀ j, UniformPathwidthBound (endpointIter κ ξ (2 * κ) j) := by
    intro j
    induction j with
    | zero => simpa [endpointIter] using hstart
    | succ j ih =>
      exact endpoint_coefficient_step κ ξ _ hξ0 hξ (hrange j).1 (hrange j).2 hpart ih
  apply uniformPathwidthBound_of_approximations
  intro η hη
  have hl0 : 0 ≤ 1 / 2 - 3 * ξ := by linarith
  have hl1 : 1 / 2 - 3 * ξ < 1 := by linarith
  set D := |2 * κ - endpointFixed κ ξ| with hD
  have hDpos : 0 < D + 1 := by positivity
  obtain ⟨j, hj⟩ := exists_pow_lt_of_lt_one (div_pos hη hDpos) hl1
  refine ⟨endpointIter κ ξ (2 * κ) j, ?_, hiter j⟩
  have hc := endpointIter_close κ ξ (2 * κ) hξ0 hξ j
  have hpowle : (1 / 2 - 3 * ξ) ^ j * D ≤ (1 / 2 - 3 * ξ) ^ j * (D + 1) := by
    have : 0 ≤ (1 / 2 - 3 * ξ) ^ j := pow_nonneg hl0 j
    nlinarith
  have hlt : (1 / 2 - 3 * ξ) ^ j * (D + 1) < η := by
    have := (lt_div_iff₀ hDpos).mp hj
    linarith
  have habs := (abs_le.mp (hc.trans (hpowle.trans hlt.le))).2
  have : endpointIter κ ξ (2 * κ) j - endpointFixed κ ξ < η := by
    have h2 := hc.trans_lt (lt_of_le_of_lt hpowle hlt)
    exact lt_of_le_of_lt (le_abs_self _) h2
  linarith

/-- General-parameter version of the project's coefficient step: every uniform
bisection coefficient `0 ≤ c < 1/6` gives the pathwidth coefficient `2c/(1+6c)`. -/
theorem bisection_transfer (c : ℝ) (hc0 : 0 ≤ c) (hc : c < 1 / 6)
    (hbis : UniformBisectionBound c) :
    UniformPathwidthBound (2 * c / (1 + 6 * c)) := by
  have h := endpoint_transfer c c hc0 hc hc0 hc.le (partition_of_bisection hbis)
  have hfix : endpointFixed c c = 2 * c / (1 + 6 * c) := by
    unfold endpointFixed
    apply max_eq_right
    have hpos : 0 < 1 + 6 * c := by linarith
    rw [le_div_iff₀ hpos]
    nlinarith
  rw [hfix] at h
  exact h

end CubicPathwidth

#print axioms CubicPathwidth.endpoint_coefficient_step
#print axioms CubicPathwidth.endpoint_transfer
#print axioms CubicPathwidth.bisection_transfer