CubicPathwidth.BoundaryAsymptotics

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

import CubicPathwidth.BoundaryInduction

/-!
# The uniform limit in the boundary/core transfer

This file checks how a finite endpoint bound with one sublinear overhead
implies the exact original BoundaryTransferClaim. The finite structural
lemma is an explicit hypothesis, not an axiom or a completed graph proof.
-/

noncomputable section
namespace CubicPathwidth

/-- A uniform affine bound, valid also for small and empty graphs. -/
def AffinePathwidthBound (b C : ℝ) : Prop :=
  ∀ n : ℕ, ∀ G : SimpleGraph (Fin n), IsSubcubic G →
    HasPathwidthAtMost G (b * (n : ℝ) + C)

/-- The exact finite endpoint implication needed from the core construction. -/
def FiniteEndpointTransfer (L : ℕ → ℝ) : Prop :=
  ∀ b C : ℝ, 0 ≤ b → b ≤ 1 / 3 → 2 ≤ C → AffinePathwidthBound b C →
    ∀ n : ℕ, ∀ G : SimpleGraph (Fin n), IsSubcubic G → ∀ X : Finset (Fin n),
      HasEndingPathwidthAtMost G X (endpointBudget b C L n X.card)

/-- The error threshold is chosen before the graph and the boundary. -/
def SublinearError (L : ℕ → ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → L n ≤ ε * (n : ℝ)

theorem affinePathwidthBound_of_uniform {b : ℝ} (hb : 0 ≤ b)
    (h : UniformPathwidthBound b) (η : ℝ) (hη : 0 < η) :
    ∃ C : ℝ, 2 ≤ C ∧ AffinePathwidthBound (b + η) C := by
  obtain ⟨N, hN⟩ := h η hη
  refine ⟨max 2 (N : ℝ), le_max_left _ _, ?_⟩
  intro n G hG
  have hC : 0 ≤ max 2 (N : ℝ) := le_trans (by norm_num) (le_max_left _ _)
  by_cases hn : N ≤ n
  · exact (hN n hn G hG).mono (by linarith)
  · apply (trivial_pathwidth_bound G).mono
    have hn' : (n : ℝ) ≤ N := by exact_mod_cast (show n ≤ N by omega)
    have hprod := mul_nonneg (show 0 ≤ b + η by linarith) (Nat.cast_nonneg n : (0 : ℝ) ≤ n)
    linarith [le_max_right (2 : ℝ) (N : ℝ)]

/-- Supply the finite structural proof and any uniformly sublinear error to
obtain the unchanged boundary-transfer proposition. -/
theorem boundaryTransfer_of_finite {L : ℕ → ℝ}
    (hL : SublinearError L) (hfinite : FiniteEndpointTransfer L) :
    BoundaryTransferClaim := by
  intro b hb hb' hbound ε hε
  let η : ℝ := min (ε / 4) ((1 / 3 - b) / 2)
  have hη : 0 < η := lt_min (by linarith) (by linarith)
  have hηε : η ≤ ε / 4 := min_le_left _ _
  have hηb : η ≤ (1 / 3 - b) / 2 := min_le_right _ _
  obtain ⟨C, hC, hAffine⟩ := affinePathwidthBound_of_uniform hb hbound η hη
  obtain ⟨NL, hNL⟩ := hL (ε / 4) (by linarith)
  obtain ⟨NC, hNC⟩ := exists_nat_ge ((C + 1) / (ε / 2))
  refine ⟨max NL NC, ?_⟩
  intro n hn G hG X
  have hnL := (le_max_left NL NC).trans hn
  have hnC := (le_max_right NL NC).trans hn
  have hLn := hNL n hnL
  have hCn : C + 1 ≤ (ε / 2) * (n : ℝ) := by
    have hnc : (NC : ℝ) ≤ n := by exact_mod_cast hnC
    have he := (div_le_iff₀ (by linarith : 0 < ε / 2)).mp (hNC.trans hnc)
    nlinarith
  obtain ⟨D, hEnd, hw⟩ := hfinite (b + η) C (by linarith) (by linarith)
    hC hAffine n G hG X
  refine ⟨D, hEnd, hw.mono ?_⟩
  let M : ℝ := max (X.card : ℝ) (b * (n : ℝ) + (1 - 3 * b) * (X.card : ℝ))
  have hxM : (X.card : ℝ) ≤ M := le_max_left _ _
  have hbM : b * (n : ℝ) + (1 - 3 * b) * (X.card : ℝ) ≤ M := le_max_right _ _
  have hηx := mul_nonneg hη.le (Nat.cast_nonneg X.card : (0 : ℝ) ≤ X.card)
  have hηn := mul_nonneg hη.le (Nat.cast_nonneg n : (0 : ℝ) ≤ n)
  have hηupper := mul_le_mul_of_nonneg_right hηε (Nat.cast_nonneg n : (0 : ℝ) ≤ n)
  have hmax : max ((X.card : ℝ) + 1)
      ((b + η) * (n : ℝ) + (1 - 3 * (b + η)) * (X.card : ℝ) + C) ≤
      M + η * (n : ℝ) + C + 1 := by
    apply max_le <;> nlinarith
  change endpointBudget (b + η) C L n X.card ≤ M + ε * (n : ℝ)
  unfold endpointBudget
  nlinarith

/-- A stable-boundary construction is enough for the whole finite endpoint
lemma; the deletion induction contributes no additional error. -/
theorem finiteEndpointTransfer_of_stable {L : ℕ → ℝ}
    (hLmono : Monotone L) (hLpos : ∀ m, 0 ≤ L m)
    (hstable : ∀ b C : ℝ, 0 ≤ b → b ≤ 1 / 3 → 2 ≤ C → AffinePathwidthBound b C →
      ∀ n : ℕ, ∀ G : SimpleGraph (Fin n), IsSubcubic G →
        ∀ U X : Finset (Fin n), X ⊆ U → StableBoundary G U X →
          HasEndingSection G U X (endpointBudget b C L U.card X.card)) :
    FiniteEndpointTransfer L := by
  intro b C hb hb' hC hAffine n G hG X
  obtain ⟨P, hEnd, hw⟩ := endingSection_of_stable G (endpointBudget b C L)
    (fun _ _ _ _ hm hx => endpointBudget_mono hb hb' hLmono hm hx)
    (fun m x _ => endpointBudget_ge_size b C hLpos m x)
    (hstable b C hb hb' hC hAffine n G hG) Finset.univ X (Finset.subset_univ _)
  refine ⟨P.toFull, ?_, ?_⟩
  · exact hEnd
  · simpa using P.toFull_width hw

end CubicPathwidth
Back to top