CubicPathwidth.Alg.Proofs2.K2Theorem2a

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.Targets
import CubicPathwidth.T2.TargetA

/-!
# K2: Theorem 2(a) realized by `algo_T2a`

Route (mirror of `T2.target2a_of_bridge`, with the plain-sweep layout bridge replaced by
`AlgoT2aWidth` and the rational labels obtained from real ones by `LabelTransfer`):
for a graph `S` of maximum degree at most `4` on `Fin n`, `GoodLabels4` at a large
radius gives real injective labels `y` whose outer frontiers have at most
`(idealSup (radiusCorr4 R) + ε/2) n` vertices; `LabelTransfer` (on `ofSimpleGraph S`,
renamed by `Fin.val`) gives rational labels `Y` with the same frontier sizes at every
rational threshold; `AlgoT2aWidth` bounds the width by that quantity; `IdealLimit`
bounds `idealSup (radiusCorr4 R)` by `F4 + ε/2`; `algoT2aExported` gives the path
decomposition.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

/-- **K2.** Theorem 2(a) is realized by `algo_T2a`, given the width bridge for the
plain sweep, the relabelling of `ofSimpleGraph`, and the label transfer. -/
theorem algoT2aRealizesTheorem2a_of (hW : AlgoT2aWidth) (hX1 : RelabelOfSimpleGraph)
    (hX4 : LabelTransfer) : AlgoT2aRealizesTheorem2a := by
  unfold AlgoT2aRealizesTheorem2a
  intro h1 ε hε
  have hε2 : 0 < ε / 2 := by linarith
  -- a radius whose ideal supremum is within ε/2 of F₄
  obtain ⟨R₀, hR₀⟩ :=
    (Metric.tendsto_atTop.mp (T2.idealLimit_of_bridge T2.bridge)) (ε / 2) hε2
  set R := max R₀ 2 with hR
  have hRle : R₀ ≤ R := le_max_left _ _
  have hR2 : 2 ≤ R := le_max_right _ _
  have hclose : T2.idealSup (T2.radiusCorr4 R) ≤ T2.F4 + ε / 2 := by
    have := hR₀ R hRle
    rw [Real.dist_eq] at this
    linarith [(abs_lt.mp this).2]
  obtain ⟨N, hN⟩ :=
    T2.goodLabels4_of_star (T2.starFour_of T2.slepian T2.bridge h1) R hR2 (ε / 2) hε2
  refine ⟨N, fun n hn S _ hS => ?_⟩
  obtain ⟨y, hy, hfr⟩ := hN n hn S hS
  have hWF : (Graph.ofSimpleGraph S).WF := (ofSimpleGraphSpec n S).1
  obtain ⟨Y, hYinj, -, hout, -, -, -⟩ :=
    hX4 (Graph.ofSimpleGraph S) n S Fin.val hWF (hX1 n S) y hy
  refine ⟨Y, algoT2aExported n S Y, ?_⟩
  have hbd : ∀ t : ℚ, ((outerFr (Graph.ofSimpleGraph S) Y t).length : ℝ) ≤
      (T2.idealSup (T2.radiusCorr4 R) + ε / 2) * n := by
    intro t
    obtain ⟨s, -, hs⟩ := hout t
    rw [hs]
    exact hfr s
  have hw := hW (Graph.ofSimpleGraph S) hWF Y hYinj _ hbd
  have hn : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  refine le_trans hw ?_
  refine mul_le_mul_of_nonneg_right ?_ hn
  linarith

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.algoT2aRealizesTheorem2a_of