CubicPathwidth.T2.GoodLabelsCount

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

import CubicPathwidth.T2.DefsB
import CubicPathwidth.T2.GoodLabels4
import CubicPathwidth.T2.GoodLabelsCountA
import CubicPathwidth.T2.GoodLabelsCountB

/-!
# Good labels, degree-count form, from the four claims

`goodLabelsCount_of`: conditional on `DegreeLabelsClaim`, `HetStarClaim`,
`StarBoundContClaim` and `ChargingClaim`, an admissible pair `(a₃, a₄)` with
`4 Φ(-3) ≤ a₃ ≤ a₄` has `GoodLabelsCount a₃ a₄`.

Port of `goodLabels4_of_star`. Labels come from the abstract scheme of
`DegreeLabelsClaim`; the per-vertex frontier probability is bounded by
`HetStarClaim` and `StarBoundContClaim`; `ChargingClaim` sums the per-type star
bounds; the two tails are controlled by Gaussian tail counts.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace T2
namespace GLC

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

/-- The star bound of the type of `v`, at level `τ`. -/
def tb (G : SimpleGraph (Fin n)) (v : Fin n) (τ : ℝ) : ℝ :=
  if G.degree v = 3 then starBound (floorsThree (nbrCount G v 4)) τ
  else starBound (floorsFour (nbrCount G v 3)) τ

theorem nbrCount_le_degree (v : Fin n) (d : ℕ) : nbrCount G v d ≤ G.degree v := by
  rw [nbrCount_eq, ← G.card_neighborFinset_eq_degree]
  exact Finset.card_filter_le _ _

theorem sum_tb_le (hch : ChargingClaim) {a₃ a₄ : ℝ} (hadm : AdmissiblePair a₃ a₄)
    (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G) {τ : ℝ}
    (hτ : τ ∈ Set.Icc (-3 : ℝ) 3) :
    ∑ v, tb G v τ ≤ a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) := by
  obtain ⟨t, h3, h4⟩ := hadm τ hτ
  refine hch n G hmin hmax (fun v => tb G v τ) a₃ a₄ t ?_ ?_
  · intro v hv
    have hk : nbrCount G v 4 ≤ 3 := hv ▸ nbrCount_le_degree v 4
    have := h3 _ hk
    simpa [tb, hv] using this
  · intro v hv
    have hk : nbrCount G v 3 ≤ 4 := hv ▸ nbrCount_le_degree v 3
    have := h4 _ hk
    have hv3 : ¬ G.degree v = 3 := by omega
    simpa [tb, hv3] using this

theorem degreeCount_add (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G) :
    degreeCount G 3 + degreeCount G 4 = n := by
  unfold degreeCount
  have : (Finset.univ.filter fun v : Fin n => G.degree v = 4) =
      Finset.univ.filter fun v : Fin n => ¬ G.degree v = 3 := by
    apply Finset.filter_congr
    intro v _
    rcases deg_cases hmin hmax v with h | h <;> simp [h]
  rw [this, Finset.card_filter_add_card_filter_not]
  simp

/-- The per-vertex bound at grid levels, in terms of types. -/
theorem prob_outer_le_tb (hS : HetStarClaim) {K : ℕ} {vec : Fin n → GaussianField.Sample n}
    (hs : Sch G K vec) (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G)
    {η δ : ℝ} (hη0 : 0 < η) (hη1 : η < 1)
    (he3 : ∀ k : ℕ, k ≤ 3 → ∀ r' : Fin 3 → ℝ,
        (∀ i, (1 - η) * floorsThree k i ≤ r' i ∧ r' i ≤ floorsThree k i) →
        ∀ τ ∈ Set.Icc (-3 : ℝ) 3, starBound r' τ ≤ starBound (floorsThree k) τ + δ)
    (he4 : ∀ k : ℕ, k ≤ 4 → ∀ r' : Fin 4 → ℝ,
        (∀ i, (1 - η) * floorsFour k i ≤ r' i ∧ r' i ≤ floorsFour k i) →
        ∀ τ ∈ Set.Icc (-3 : ℝ) 3, starBound r' τ ≤ starBound (floorsFour k) τ + δ)
    (hedge : ∀ u v, G.Adj u v →
      (1 - η) * edgeFloor (G.degree u) (G.degree v) ≤ ⟪vec u, vec v⟫)
    (v : Fin n) {τ : ℝ} (hτ : τ ∈ Set.Icc (-3 : ℝ) 3) :
    (stdGaussian (GaussianField.Sample n)).real (outerEv G vec τ v) ≤ tb G v τ + δ := by
  rcases deg_cases hmin hmax v with hv | hv
  · have h1 := prob_outer_le_three hS hs hmin hmax hη0 hη1 hedge v hv τ
    have h2 := he3 (nbrCount G v 4) (hv ▸ nbrCount_le_degree v 4)
      (fun i => (1 - η) * floorsThree (nbrCount G v 4) i)
      (fun i => ⟨le_refl _, by
        have := floorsThree_pos (nbrCount G v 4) i
        nlinarith⟩) τ hτ
    simpa [tb, hv] using h1.trans h2
  · have h1 := prob_outer_le_four hS hs hmin hmax hη0 hη1 hedge v hv τ
    have h2 := he4 (nbrCount G v 3) (hv ▸ nbrCount_le_degree v 3)
      (fun i => (1 - η) * floorsFour (nbrCount G v 3) i)
      (fun i => ⟨le_refl _, by
        have := floorsFour_pos (nbrCount G v 3) i
        nlinarith⟩) τ hτ
    have hv3 : ¬ G.degree v = 3 := by omega
    simpa [tb, hv3] using h1.trans h2

theorem sum_outer_le_count (hS : HetStarClaim) (hch : ChargingClaim) {a₃ a₄ : ℝ}
    (hadm : AdmissiblePair a₃ a₄) {K : ℕ} {vec : Fin n → GaussianField.Sample n}
    (hs : Sch G K vec) (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G)
    {η δ : ℝ} (hη0 : 0 < η) (hη1 : η < 1)
    (he3 : ∀ k : ℕ, k ≤ 3 → ∀ r' : Fin 3 → ℝ,
        (∀ i, (1 - η) * floorsThree k i ≤ r' i ∧ r' i ≤ floorsThree k i) →
        ∀ τ ∈ Set.Icc (-3 : ℝ) 3, starBound r' τ ≤ starBound (floorsThree k) τ + δ)
    (he4 : ∀ k : ℕ, k ≤ 4 → ∀ r' : Fin 4 → ℝ,
        (∀ i, (1 - η) * floorsFour k i ≤ r' i ∧ r' i ≤ floorsFour k i) →
        ∀ τ ∈ Set.Icc (-3 : ℝ) 3, starBound r' τ ≤ starBound (floorsFour k) τ + δ)
    (hedge : ∀ u v, G.Adj u v →
      (1 - η) * edgeFloor (G.degree u) (G.degree v) ≤ ⟪vec u, vec v⟫)
    {τ : ℝ} (hτ : τ ∈ Set.Icc (-3 : ℝ) 3) :
    ∑ v, (stdGaussian (GaussianField.Sample n)).real (outerEv G vec τ v) ≤
      a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) + n * δ := by
  calc _ ≤ ∑ v : Fin n, (tb G v τ + δ) :=
        Finset.sum_le_sum fun v _ => prob_outer_le_tb hS hs hmin hmax hη0 hη1 he3 he4 hedge v hτ
    _ = ∑ v, tb G v τ + n * δ := by
        rw [Finset.sum_add_distrib]; simp
    _ ≤ _ := by
        have := sum_tb_le hch hadm hmin hmax hτ
        linarith

theorem cellLo_mem {q i : ℕ} (hq : 0 < q) (hi : i < 2 * (3 * q)) :
    cellLo (3 * q) q i ∈ Set.Icc (-3 : ℝ) 3 := by
  have hq' : (0 : ℝ) < q := by exact_mod_cast hq
  have hi' : (i : ℝ) < 2 * (3 * q) := by exact_mod_cast hi
  unfold cellLo
  push_cast
  constructor
  · rw [le_div_iff₀ hq']
    have : (0 : ℝ) ≤ i := Nat.cast_nonneg i
    linarith
  · rw [div_le_iff₀ hq']
    linarith

end GLC

open GLC in

/-- **Good labels, degree-count form.** -/
theorem goodLabelsCount_of (hL : DegreeLabelsClaim) (hS : HetStarClaim)
    (hC : StarBoundContClaim) (hch : ChargingClaim) {a₃ a₄ : ℝ}
    (hadm : AdmissiblePair a₃ a₄) (htail : 4 * Phi (-3) ≤ a₃) (h34 : a₃ ≤ a₄) :
    GoodLabelsCount a₃ a₄ := by
  intro ε hε
  obtain ⟨η, hη0, hη1, he3, he4⟩ := eta_exists 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 : ℕ := ⌈8 / ε⌉₊ + 1 with hq
  set M : ℕ := 3 * q with hM
  set D : ℝ := L4.depBound (K + 1) with hDdef
  set Mc : ℝ := 4 * (M : ℝ) + 2 with hMc
  refine ⟨⌈D * (10 * Mc / ε) ^ 2⌉₊ + 1, ?_⟩
  intro n hn G hmin hmax
  obtain ⟨vec, hnorm, hcorr, hloc, hinj⟩ := hK n G hmin hmax
  have hs : 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ε : 2 / (q : ℝ) ≤ ε / 4 := by
    have h1 : (8 / ε : ℝ) ≤ q := by
      have := Nat.le_ceil (8 / ε)
      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 := L4.depBound_pos _
  have hMpos : 0 < Mc := by positivity
  have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  have hnD : D * (10 * Mc / ε) ^ 2 ≤ n := by
    have := Nat.le_ceil (D * (10 * Mc / ε) ^ 2)
    have : (⌈D * (10 * Mc / ε) ^ 2⌉₊ : ℝ) + 1 ≤ n := by exact_mod_cast hn
    linarith
  have hsqrt : Mc * Real.sqrt (n * D) ≤ ε / 10 * n := by
    have hs' : Real.sqrt (n * D) ≤ ε * n / (10 * Mc) := by
      rw [Real.sqrt_le_iff]
      refine ⟨by positivity, ?_⟩
      have e : (ε * n / (10 * Mc)) ^ 2 = n * (n * (ε / (10 * Mc)) ^ 2) := by ring
      rw [e]
      apply mul_le_mul_of_nonneg_left _ hn0
      have e2 : D = D * (10 * Mc / ε) ^ 2 * (ε / (10 * 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 / (10 * Mc)) :=
          mul_le_mul_of_nonneg_left hs' hMpos.le
      _ = ε / 10 * n := by field_simp
  -- a good sample
  obtain ⟨x, hxN, hx⟩ := exists_notMem_null_le_integral
    (integrable_devTotal G vec M q 3) (lab_injective_ae hs)
  set dev := devTotal G vec M q 3 x with hdev_def
  have hdev : dev ≤ ε / 10 * n := by
    have h1 := devTotal_integral_le G vec hs hmax M q 3
    exact hx.trans (h1.trans hsqrt)
  have hinjx : Function.Injective (lab vec x) := by
    by_contra h'
    exact hxN h'
  refine ⟨lab vec x, hinjx, ?_⟩
  intro t
  -- the count identity
  have hcount := degreeCount_add hmin hmax
  have hcountR : (degreeCount G 3 : ℝ) + (degreeCount G 4 : ℝ) = 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 hAn : a₃ * n ≤ a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) := by
    rw [← hcountR]
    nlinarith
  by_cases htlow : t ≤ -3
  · -- far below
    have h1 := L4.outer_tail_low4 G hmax (lab vec x) htlow
    have heq : (Finset.univ.filter fun v => lab vec x v ≤ -3) =
        Finset.univ.filter fun v => x ∈ lowTailEv vec 3 v :=
      Finset.filter_congr fun v _ => Iff.rfl
    rw [heq] at h1
    have h2' := L4.card_le_sum_add_dev (lowTailEv vec 3) x
    have h3' := sum_lowTail_eq G vec hs 3
    have h4 := (dev_tail_le (G := G) (vec := vec) (M := M) (q := q) (T := 3) x).1
    have h1' : ((C3.outerFrontier G (lab vec x) t).card : ℝ) ≤
        4 * ((Finset.univ.filter fun v => x ∈ lowTailEv vec 3 v).card : ℝ) := by
      exact_mod_cast h1
    have e3 : (n : ℝ) * (4 * 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 (lab vec x) hthigh.le
    have heq : (Finset.univ.filter fun v => (3 : ℝ) < lab vec x v) =
        Finset.univ.filter fun v => x ∈ highTailEv vec 3 v :=
      Finset.filter_congr fun v _ => Iff.rfl
    rw [heq] at h1
    have h2' := L4.card_le_sum_add_dev (highTailEv vec 3) x
    have h3' := sum_highTail_le G vec hs 3
    have h4 := (dev_tail_le (G := G) (vec := vec) (M := M) (q := q) (T := 3) x).2
    have h1' : ((C3.outerFrontier G (lab vec x) t).card : ℝ) ≤
        ((Finset.univ.filter fun v => x ∈ 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 := L4.outer_grid4 G hmax (lab vec x) hlo hhi
    rw [outerFrontier_eq, outerFrontier_eq, cellSet_eq] at hg
    have hg' : ((Finset.univ.filter fun v => x ∈ outerEv G vec t v).card : ℝ) ≤
        ((Finset.univ.filter fun v => x ∈ outerEv G vec (cellLo M q i) v).card : ℝ) +
        4 * ((Finset.univ.filter fun v =>
          x ∈ cellEv vec (cellLo M q i) (cellHi M q i) v).card : ℝ) := by
      exact_mod_cast hg
    have a1 := L4.card_le_sum_add_dev (outerEv G vec (cellLo M q i)) x
    have a2 := sum_outer_le_count hS hch hadm hs hmin hmax hη0 hη1 he3 he4 hcorr
      (cellLo_mem hq0 hi)
    have a3 := dev_outer_le (G := G) (vec := vec) (q := q) (T := 3) x hi
    have b1 := L4.card_le_sum_add_dev (cellEv vec (cellLo M q i) (cellHi M q i)) x
    have hw : cellHi M q i - cellLo M q i = 1 / q := by
      unfold cellHi cellLo
      field_simp
      ring
    have b2 := sum_cell_le G vec hs (a := cellLo M q i) (b := cellHi M q i)
      (by rw [← sub_nonneg, hw]; positivity)
    have b3 := dev_cell_le (G := G) (vec := vec) (M := M) (q := q) (T := 3) x hi
    rw [hw] at b2
    rw [outerFrontier_eq]
    have e4 : (n : ℝ) * (2 / q) ≤ n * (ε / 4) := mul_le_mul_of_nonneg_left hqε hn0
    have e5 : (n : ℝ) * (1 / q / 2) = n * (2 / q) / 4 := by ring
    nlinarith

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.goodLabelsCount_of