CubicPathwidth.PwSeq.Basic

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

Statements of the paper formalised here: Definition 9.1.

import CubicPathwidth.PwSeq.Defs
import CubicPathwidth.AsymptoticTransfer

/-!
# Basic facts on pathwidth sequences (obligation Q1)

* `targetRhoForm` (A1): the uniform `ε`–`N` form of Definition 1.1 is equivalent to the
  form with a single remainder function `ρ` with `ρ n / n → 0`.
* `targetMono` (A2): entrywise larger costs preserve being a pathwidth sequence.

For `A1`, the direction `ε`–`N ⇒ ρ` chooses thresholds `N j` for `ε = 1/(j+1)`, and sets
`ρ n = n / (J n + 1)`, where `J n` is the largest `j ≤ n` with `N j ≤ n`, as soon as
`N 0 ≤ n`. For `n < N 0` it uses the trivial bound `pw ≤ n - 1` together with the crude
lower bound `degreeWeight G c ≥ -n * ∑_{d ≤ n} |c d|`.
-/

noncomputable section

open Filter Topology

namespace CubicPathwidth
namespace PwSeq

open T2 T3 T4

/-- Crude size bound for the cost sum: `∑_{d ≤ n} |c d|`. -/
def costSum (c : ℕ → ℝ) (n : ℕ) : ℝ := ∑ d ∈ Finset.range (n + 1), |c d|

theorem costSum_nonneg (c : ℕ → ℝ) (n : ℕ) : 0 ≤ costSum c n :=
  Finset.sum_nonneg fun _ _ => abs_nonneg _

/-- Lower bound for the degree weight of any graph on `Fin n`. -/
theorem neg_costSum_le_degreeWeight (c : ℕ → ℝ) {n : ℕ} (G : SimpleGraph (Fin n)) :
    -((n : ℝ) * costSum c n) ≤ degreeWeight G c := by
  classical
  unfold degreeWeight
  have h1 : ∀ v : Fin n, -costSum c n ≤ c (G.degree v) := by
    intro v
    have hd : G.degree v ≤ n := by
      have := G.degree_lt_card_verts v
      simp at this
      omega
    have h2 : |c (G.degree v)| ≤ costSum c n :=
      Finset.single_le_sum (f := fun d => |c d|) (fun _ _ => abs_nonneg _)
        (Finset.mem_range.2 (Nat.lt_succ_of_le hd))
    have := neg_abs_le (c (G.degree v))
    linarith
  calc -((n : ℝ) * costSum c n) = ∑ _v : Fin n, -costSum c n := by simp
    _ ≤ _ := Finset.sum_le_sum fun v _ => h1 v

/-- The trivial regime: a remainder `n + n * costSum` always suffices. -/
theorem trivial_regime (c : ℕ → ℝ) {n : ℕ} (G : SimpleGraph (Fin n)) :
    HasPathwidthAtMost G (degreeWeight G c + ((n : ℝ) + (n : ℝ) * costSum c n)) := by
  apply (trivial_pathwidth_bound G).mono
  have := neg_costSum_le_degreeWeight c G
  linarith

/-- (A1) The `ε`–`N` form is Definition 1.1. -/
theorem targetRhoForm : TargetRhoForm := by
  classical
  intro k a
  constructor
  · rintro ⟨hk, h⟩
    refine ⟨hk, ?_⟩
    set c := seqCost k a with hc
    choose N hN using fun j : ℕ => h (1 / ((j : ℝ) + 1)) (by positivity)
    let J : ℕ → ℕ := fun n => Nat.findGreatest (fun j => N j ≤ n) n
    let ρ : ℕ → ℝ := fun n =>
      if N 0 ≤ n then (n : ℝ) / ((J n : ℝ) + 1) else (n : ℝ) + (n : ℝ) * costSum c n
    have hJ : ∀ n, N 0 ≤ n → N (J n) ≤ n := fun n hn =>
      Nat.findGreatest_spec (P := fun j => N j ≤ n) (Nat.zero_le n) hn
    have hJge : ∀ j n, j ≤ n → N j ≤ n → j ≤ J n := fun j n hjn hNj =>
      Nat.le_findGreatest hjn hNj
    refine ⟨ρ, ?_, ?_⟩
    · rw [Metric.tendsto_atTop]
      intro ε hε
      obtain ⟨j, hj⟩ := exists_nat_one_div_lt hε
      refine ⟨max (N 0) (max (N j) (max j 1)), fun n hn => ?_⟩
      have hN0 : N 0 ≤ n := le_trans (le_max_left _ _) hn
      have hNj : N j ≤ n :=
        le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hn
      have hjn : j ≤ n :=
        le_trans (le_trans (le_trans (le_max_left _ _) (le_max_right _ _))
          (le_max_right _ _)) hn
      have hn1 : 1 ≤ n :=
        le_trans (le_trans (le_trans (le_max_right _ _) (le_max_right _ _))
          (le_max_right _ _)) hn
      have hnpos : (0 : ℝ) < n := by exact_mod_cast hn1
      have hge : (j : ℝ) ≤ J n := by exact_mod_cast hJge j n hjn hNj
      have hval : ρ n / (n : ℝ) = 1 / ((J n : ℝ) + 1) := by
        simp only [ρ, hN0, ite_true]
        field_simp
      rw [Real.dist_eq, sub_zero, hval, abs_of_pos (by positivity)]
      refine lt_of_le_of_lt ?_ hj
      apply one_div_le_one_div_of_le (by positivity)
      linarith
    · intro n G
      by_cases hn : N 0 ≤ n
      · simp only [ρ, hn, ite_true]
        have := hN (J n) n (hJ n hn) G
        refine this.mono (le_of_eq ?_)
        simp [div_eq_mul_inv]
        ring
      · simp only [ρ, hn, ite_false]
        exact trivial_regime c G
  · rintro ⟨hk, ρ, hρ, h⟩
    refine ⟨hk, ?_⟩
    intro ε hε
    rw [Metric.tendsto_atTop] at hρ
    obtain ⟨N, hN⟩ := hρ ε hε
    refine ⟨max N 1, fun n hn G => ?_⟩
    have hnN : N ≤ n := le_trans (le_max_left _ _) hn
    have hn1 : 1 ≤ n := le_trans (le_max_right _ _) hn
    have hnpos : (0 : ℝ) < n := by exact_mod_cast hn1
    have := hN n hnN
    rw [Real.dist_eq, sub_zero] at this
    have h2 : ρ n ≤ ε * n := by
      have := (abs_lt.1 this).2
      rw [div_lt_iff₀ hnpos] at this
      exact this.le
    exact (h n G).mono (by linarith)

/-- (A2) Remark after Definition 1.1: monotonicity in the cost sequence. -/
theorem targetMono : TargetMono := by
  classical
  intro k k' a a' hk' hle ⟨_, h⟩
  refine ⟨hk', ?_⟩
  intro ε hε
  obtain ⟨N, hN⟩ := h ε hε
  refine ⟨N, fun n hn G => ?_⟩
  apply (hN n hn G).mono
  have : degreeWeight G (seqCost k a) ≤ degreeWeight G (seqCost k' a') := by
    unfold degreeWeight
    refine Finset.sum_le_sum fun v _ => ?_
    by_cases hd : 3 ≤ G.degree v
    · exact hle _ hd
    · simp [seqCost, show G.degree v ≤ 2 by omega]
  linarith

end PwSeq
end CubicPathwidth

#print axioms CubicPathwidth.PwSeq.targetRhoForm
#print axioms CubicPathwidth.PwSeq.targetMono
Back to top