CubicPathwidth.T3.GoodLabelsCount5

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

import CubicPathwidth.T3.GoodLabelsCount5A
import CubicPathwidth.T3.GoodLabelsCount5B

/-!
# Good labels, degree-count form, maximum degree 5

`goodLabelsCount5_step`: conditional on `DegreeLabels5Claim`, `HetStarClaim`,
`StarBoundContClaim` and `Charging5Claim`, an admissible triple `(a₃, a₄, a₅)` with
`5 Φ(-3) ≤ a₃ ≤ a₄ ≤ a₅` has `GoodLabelsCount5 a₃ a₄ a₅`.

Port of `T2.goodLabelsCount_of`. Labels come from the abstract scheme of
`DegreeLabels5Claim`; the per-vertex frontier probability is bounded by `HetStarClaim`
and `StarBoundContClaim`; `Charging5Claim` sums the per-type star bounds; the two tails
are controlled by Gaussian tail counts (a frontier vertex below `-3` has a neighbor
below `-3`, and every vertex has at most five neighbors).
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace T3
namespace GLC5

open T2

variable {n : ℕ} {G : SimpleGraph (Fin n)}

theorem nbrCount_sum (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 5 G) (v : Fin n) :
    nbrCount G v 3 + nbrCount G v 4 + nbrCount G v 5 = G.degree v := by
  have hN : (G.neighborFinset v).card = ∑ b ∈ ({3, 4, 5} : Finset ℕ),
      ((G.neighborFinset v).filter fun a => G.degree a = b).card :=
    Finset.card_eq_sum_card_fiberwise (f := fun a => G.degree a) (t := ({3, 4, 5} : Finset ℕ))
      (by intro x _; simpa using deg_cases5 hmin hmax x)
  rw [G.card_neighborFinset_eq_degree] at hN
  rw [hN]
  simp [GLC.nbrCount_eq, Finset.sum_insert, add_assoc]

theorem degreeCount_add5 (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 5 G) :
    degreeCount G 3 + degreeCount G 4 + degreeCount G 5 = n := by
  have hN : (Finset.univ : Finset (Fin n)).card = ∑ b ∈ ({3, 4, 5} : Finset ℕ),
      ((Finset.univ : Finset (Fin n)).filter fun a => G.degree a = b).card :=
    Finset.card_eq_sum_card_fiberwise (f := fun a => G.degree a) (t := ({3, 4, 5} : Finset ℕ))
      (by intro x _; simpa using deg_cases5 hmin hmax x)
  rw [Finset.card_univ, Fintype.card_fin] at hN
  have h2 : (∑ b ∈ ({3, 4, 5} : Finset ℕ),
      ((Finset.univ : Finset (Fin n)).filter fun a => G.degree a = b).card) =
      degreeCount G 3 + degreeCount G 4 + degreeCount G 5 := by
    simp [degreeCount, Finset.sum_insert, add_assoc]
  omega

theorem sum_tb5_le (hch : Charging5Claim) {a₃ a₄ a₅ : ℝ} (hadm : AdmissibleTriple a₃ a₄ a₅)
    (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 5 G) {τ : ℝ}
    (hτ : τ ∈ Set.Icc (-3 : ℝ) 3) :
    ∑ v, tb5 G v τ ≤ a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) +
      a₅ * (degreeCount G 5 : ℝ) := by
  obtain ⟨t₃₄, t₃₅, t₄₅, ht⟩ := hadm τ hτ
  refine hch n G hmin hmax (fun v => tb5 G v τ) a₃ a₄ a₅ t₃₄ t₃₅ t₄₅ ?_
  intro v
  exact ht (G.degree v) (nbrCount G v 3) (nbrCount G v 4) (nbrCount G v 5)
    (deg_cases5 hmin hmax v) (nbrCount_sum hmin hmax v)

theorem sum_outer_le_count5 (hS : HetStarClaim) (hch : Charging5Claim) {a₃ a₄ a₅ : ℝ}
    (hadm : AdmissibleTriple a₃ a₄ a₅) {K : ℕ} {vec : Fin n → GaussianField.Sample n}
    (hs : GLC.Sch G K vec) (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 5 G)
    {η δ : ℝ} (hη0 : 0 < η) (hη1 : η < 1)
    (he : ∀ d k₃ k₄ : ℕ, (d = 3 ∨ d = 4 ∨ d = 5) → k₃ ≤ 5 → k₄ ≤ 5 → ∀ r' : Fin d → ℝ,
        (∀ i, (1 - η) * typeFloors d k₃ k₄ i ≤ r' i ∧ r' i ≤ typeFloors d k₃ k₄ i) →
        ∀ τ ∈ Set.Icc (-3 : ℝ) 3,
          starBound r' τ ≤ starBound (typeFloors d k₃ k₄) τ + δ)
    (hedge : ∀ u v, G.Adj u v →
      (1 - η) * rFloor (G.degree u) (G.degree v) ≤ ⟪vec u, vec v⟫)
    {τ : ℝ} (hτ : τ ∈ Set.Icc (-3 : ℝ) 3) :
    ∑ v, (stdGaussian (GaussianField.Sample n)).real (GLC.outerEv G vec τ v) ≤
      a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) +
        a₅ * (degreeCount G 5 : ℝ) + n * δ := by
  calc _ ≤ ∑ v : Fin n, (tb5 G v τ + δ) :=
        Finset.sum_le_sum fun v _ => prob_outer_le_tb5 hS hs hmin hmax hη0 hη1 he hedge v hτ
    _ = ∑ v, tb5 G v τ + n * δ := by
        rw [Finset.sum_add_distrib]; simp
    _ ≤ _ := by
        have := sum_tb5_le hch hadm hmin hmax hτ
        linarith

end GLC5

open T2 GLC5 in

/-- **Good labels, degree-count form, maximum degree 5.** -/
theorem goodLabelsCount5_step : GoodLabelsCount5Step := by
  intro hL hS hC hch a₃ a₄ a₅ hadm htail h34 h45 ε hε
  obtain ⟨η, hη0, hη1, he⟩ := eta_exists5 hC (δ := ε / 4) (by positivity)
  obtain ⟨K, hK⟩ := hL η hη0
  have hPhi : 0 ≤ Phi (-3) := measureReal_nonneg
  have ha3 : 0 ≤ a₃ := by linarith
  set q : ℕ := ⌈10 / ε⌉₊ + 1 with hq
  set M : ℕ := 3 * q with hM
  set D : ℝ := depBound5 (K + 1) with hDdef
  set Mc : ℝ := 4 * (M : ℝ) + 2 with hMc
  refine ⟨⌈D * (12 * Mc / ε) ^ 2⌉₊ + 1, ?_⟩
  intro n hn G hmin hmax
  obtain ⟨vec, hnorm, hcorr, hloc, hinj⟩ := hK n G hmin hmax
  have hs : GLC.Sch G K vec := ⟨hnorm, hloc, hinj⟩
  -- numeric facts
  have hq0 : 0 < q := by omega
  have hq' : (0 : ℝ) < q := by exact_mod_cast hq0
  have hqε : 5 / 2 / (q : ℝ) ≤ ε / 4 := by
    have h1 : (10 / ε : ℝ) ≤ q := by
      have := Nat.le_ceil (10 / ε)
      push_cast [hq]
      linarith
    rw [div_le_iff₀ hq']
    rw [div_le_iff₀ hε] at h1
    linarith
  have hKq : (M : ℝ) / q = 3 := by
    rw [hM]
    push_cast
    field_simp
  have hD : 0 < D := depBound5_pos _
  have hMpos : 0 < Mc := by positivity
  have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  have hnD : D * (12 * Mc / ε) ^ 2 ≤ n := by
    have := Nat.le_ceil (D * (12 * Mc / ε) ^ 2)
    have : (⌈D * (12 * Mc / ε) ^ 2⌉₊ : ℝ) + 1 ≤ n := by exact_mod_cast hn
    linarith
  have hsqrt : Mc * Real.sqrt (n * D) ≤ ε / 12 * n := by
    have hs' : Real.sqrt (n * D) ≤ ε * n / (12 * Mc) := by
      rw [Real.sqrt_le_iff]
      refine ⟨by positivity, ?_⟩
      have e : (ε * n / (12 * Mc)) ^ 2 = n * (n * (ε / (12 * Mc)) ^ 2) := by ring
      rw [e]
      apply mul_le_mul_of_nonneg_left _ hn0
      have e2 : D = D * (12 * Mc / ε) ^ 2 * (ε / (12 * Mc)) ^ 2 := by
        field_simp
      rw [e2]
      apply mul_le_mul_of_nonneg_right hnD (by positivity)
    calc Mc * Real.sqrt (n * D) ≤ Mc * (ε * n / (12 * Mc)) :=
          mul_le_mul_of_nonneg_left hs' hMpos.le
      _ = ε / 12 * n := by field_simp
  -- a good sample
  obtain ⟨x, hxN, hx⟩ := exists_notMem_null_le_integral
    (GLC.integrable_devTotal G vec M q 3) (GLC.lab_injective_ae hs)
  set dev := GLC.devTotal G vec M q 3 x with hdev_def
  have hdev : dev ≤ ε / 12 * n := by
    have h1 := devTotal_integral_le5 hs hmax M q 3
    exact hx.trans (h1.trans hsqrt)
  have hdev0 : 0 ≤ dev :=
    (abs_nonneg _).trans (GLC.dev_tail_le (G := G) (vec := vec) (M := M) (q := q) (T := 3) x).1
  have hinjx : Function.Injective (GLC.lab vec x) := by
    by_contra h'
    exact hxN h'
  refine ⟨GLC.lab vec x, hinjx, ?_⟩
  intro t
  -- the count identity
  have hcount := degreeCount_add5 hmin hmax
  have hcountR : (degreeCount G 3 : ℝ) + (degreeCount G 4 : ℝ) + (degreeCount G 5 : ℝ) = n := by
    exact_mod_cast hcount
  have hn3 : (0 : ℝ) ≤ (degreeCount G 3 : ℝ) := Nat.cast_nonneg _
  have hn4 : (0 : ℝ) ≤ (degreeCount G 4 : ℝ) := Nat.cast_nonneg _
  have hn5 : (0 : ℝ) ≤ (degreeCount G 5 : ℝ) := Nat.cast_nonneg _
  have hAn : a₃ * n ≤ a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) +
      a₅ * (degreeCount G 5 : ℝ) := by
    rw [← hcountR]
    have i4 := mul_le_mul_of_nonneg_right h34 hn4
    have i5 := mul_le_mul_of_nonneg_right (h34.trans h45) hn5
    linarith
  by_cases htlow : t ≤ -3
  · -- far below
    have h1 := outer_tail_low5 G hmax (GLC.lab vec x) htlow
    have heq : (Finset.univ.filter fun v => GLC.lab vec x v ≤ -3) =
        Finset.univ.filter fun v => x ∈ GLC.lowTailEv vec 3 v :=
      Finset.filter_congr fun v _ => Iff.rfl
    rw [heq] at h1
    have h2' := L4.card_le_sum_add_dev (GLC.lowTailEv vec 3) x
    have h3' := GLC.sum_lowTail_eq G vec hs 3
    have h4 := (GLC.dev_tail_le (G := G) (vec := vec) (M := M) (q := q) (T := 3) x).1
    have h1' : ((C3.outerFrontier G (GLC.lab vec x) t).card : ℝ) ≤
        5 * ((Finset.univ.filter fun v => x ∈ GLC.lowTailEv vec 3 v).card : ℝ) := by
      exact_mod_cast h1
    have e3 : (n : ℝ) * (5 * Phi (-3)) ≤ n * a₃ := mul_le_mul_of_nonneg_left htail hn0
    nlinarith
  by_cases hthigh : (3 : ℝ) < t
  · -- far above
    have h1 := C3.outer_tail G (GLC.lab vec x) hthigh.le
    have heq : (Finset.univ.filter fun v => (3 : ℝ) < GLC.lab vec x v) =
        Finset.univ.filter fun v => x ∈ GLC.highTailEv vec 3 v :=
      Finset.filter_congr fun v _ => Iff.rfl
    rw [heq] at h1
    have h2' := L4.card_le_sum_add_dev (GLC.highTailEv vec 3) x
    have h3' := GLC.sum_highTail_le G vec hs 3
    have h4 := (GLC.dev_tail_le (G := G) (vec := vec) (M := M) (q := q) (T := 3) x).2
    have h1' : ((C3.outerFrontier G (GLC.lab vec x) t).card : ℝ) ≤
        ((Finset.univ.filter fun v => x ∈ GLC.highTailEv vec 3 v).card : ℝ) := by
      exact_mod_cast h1
    have e3 : (n : ℝ) * Phi (-3) ≤ n * a₃ := by
      apply mul_le_mul_of_nonneg_left _ hn0
      linarith
    nlinarith
  · -- inside the grid
    push Not at htlow hthigh
    obtain ⟨i, hi, hlo, hhi⟩ := L4.exists_index (K := M) hq0
      (by rw [neg_div, hKq]; linarith) (by rw [hKq]; exact hthigh)
    have hg := outer_grid5 G hmax (GLC.lab vec x) hlo hhi
    rw [GLC.outerFrontier_eq, GLC.outerFrontier_eq, GLC.cellSet_eq] at hg
    have hg' : ((Finset.univ.filter fun v => x ∈ GLC.outerEv G vec t v).card : ℝ) ≤
        ((Finset.univ.filter fun v => x ∈ GLC.outerEv G vec (GLC.cellLo M q i) v).card : ℝ) +
        5 * ((Finset.univ.filter fun v =>
          x ∈ GLC.cellEv vec (GLC.cellLo M q i) (GLC.cellHi M q i) v).card : ℝ) := by
      exact_mod_cast hg
    have a1 := L4.card_le_sum_add_dev (GLC.outerEv G vec (GLC.cellLo M q i)) x
    have a2 := sum_outer_le_count5 hS hch hadm hs hmin hmax hη0 hη1 he hcorr
      (GLC.cellLo_mem hq0 hi)
    have a3 := GLC.dev_outer_le (G := G) (vec := vec) (q := q) (T := 3) x hi
    have b1 := L4.card_le_sum_add_dev (GLC.cellEv vec (GLC.cellLo M q i) (GLC.cellHi M q i)) x
    have hw : GLC.cellHi M q i - GLC.cellLo M q i = 1 / q := by
      unfold GLC.cellHi GLC.cellLo
      field_simp
      ring
    have b2 := GLC.sum_cell_le G vec hs (a := GLC.cellLo M q i) (b := GLC.cellHi M q i)
      (by rw [← sub_nonneg, hw]; positivity)
    have b3 := GLC.dev_cell_le (G := G) (vec := vec) (M := M) (q := q) (T := 3) x hi
    rw [hw] at b2
    rw [GLC.outerFrontier_eq]
    have e4 : (n : ℝ) * (5 / 2 / q) ≤ n * (ε / 4) := mul_le_mul_of_nonneg_left hqε hn0
    have e5 : (n : ℝ) * (1 / q / 2) = n * (5 / 2 / q) / 5 := by ring
    linarith

end T3
end CubicPathwidth

#print axioms CubicPathwidth.T3.goodLabelsCount5_step