CubicPathwidth.T2.AssemblyA

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

import CubicPathwidth.T2.Defs

/-!
# Parent assembly for Theorem 2(a)

`theorem2a_of_children` checks that the children of part (a) suffice.
It is conditional on its hypotheses.
-/

noncomputable section
open Filter Topology

namespace CubicPathwidth
namespace T2

theorem theorem2a_of_children (hlay : PlainLayoutClaim)
    (hgood : ∀ R : ℕ, 2 ≤ R → GoodLabels4 R) (hlim : IdealLimitClaim) : Theorem2a := by
  intro ε 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 hlim) (ε / 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 : idealSup (radiusCorr4 R) ≤ F4 + ε / 2 := by
    have := hR₀ R hRle
    rw [Real.dist_eq] at this
    linarith [(abs_lt.mp this).2]
  obtain ⟨N, hN⟩ := hgood R hR2 (ε / 2) hε2
  refine ⟨N, fun n hn G hG => ?_⟩
  obtain ⟨y, hy, hfr⟩ := hN n hn G hG
  apply hlay n G y hy
  intro t
  calc ((C3.outerFrontier G y t).card : ℝ)
      ≤ (idealSup (radiusCorr4 R) + ε / 2) * n := hfr t
    _ ≤ (F4 + ε) * n := by
        apply mul_le_mul_of_nonneg_right _ (Nat.cast_nonneg n)
        linarith

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.theorem2a_of_children