CubicPathwidth.Sw4.GoodLabels

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

import CubicPathwidth.Sw4.GoodLabelsB
import CubicPathwidth.T2.DegreeLabels
import CubicPathwidth.C3.GoodLabels

/-!
# Q5: good labels for the switched layout (`thm:switched4`, minimum degree 3)

`goodLabelsSw_of : ZeroVertexClaim → FrontierVertexClaim → GoodLabelsSw C3.c3 aM`.

Labels are `y_v = ⟪vec v, x⟫` for the degree-sensitive unit vectors of
`T2.degreeLabels` at precision `η = min η₁ η₂`, where `η₁`, `η₂` come from the two vertex
claims at `δ = ε/4`, and `x` is a standard Gaussian sample. Per vertex, the neighbors are
listed with the degree-3 ones first, so the edge floors become `typeFloors d k₃ k₄`, and
the events of `v` lie inside those of `zeroProb`, `zeroProb'` (threshold zero) and
`frontierProb τ` (thresholds `τ = ±i/q ≠ 0`). `T2.charging` turns the per-type bounds into
`c₃ n₃ + a_M n₄ + δ n` for the expected counts. A grid with mesh `1/q` on `[-T₀, T₀]`
gives finitely many local counts; their total absolute deviation is `O(√n)` on average,
so some sample has injective labels and small deviation. Between grid points the inner
(outer) frontier is compared with the one at the next grid point towards zero, plus four
times the number of labels in the cell; beyond `±T₀` the frontier lies in a Gaussian tail
of mass at most `1/T₀²`.

Port of `C3.Labels.goodLabels_of_claims` (switched layout, subcubic) with the
degree-count bookkeeping of `T2.goodLabelsCount_of`.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace Sw4

open T2 T2.GLC T3 SwL

namespace SwL

variable {n : ℕ} {G : SimpleGraph (Fin n)} {K : ℕ} {vec : Fin n → GaussianField.Sample n}

theorem sum_lowTail_le (hs : Sch G K vec) {T : ℝ} (hT : 0 < T) :
    ∑ v, (stdGaussian (GaussianField.Sample n)).real (lowTailEv vec T v) ≤ n * (1 / T ^ 2) := by
  calc _ ≤ ∑ _v : Fin n, 1 / T ^ 2 := by
        apply Finset.sum_le_sum
        intro v _
        have : lowTailEv vec T v = {x | lab vec x v ∈ Set.Iic (-T)} := rfl
        rw [this, lab_normal hs v measurableSet_Iic]
        exact C3.gaussianReal_Iic_neg_le hT
    _ = _ := by simp

theorem sum_highTail_le (hs : Sch G K vec) {T : ℝ} (hT : 0 < T) :
    ∑ v, (stdGaussian (GaussianField.Sample n)).real (highTailEv vec T v) ≤ n * (1 / T ^ 2) := by
  calc _ ≤ ∑ _v : Fin n, 1 / T ^ 2 := by
        apply Finset.sum_le_sum
        intro v _
        have : highTailEv vec T v = {x | lab vec x v ∈ Set.Ioi T} := rfl
        rw [this, lab_normal hs v measurableSet_Ioi]
        exact C3.gaussianReal_Ioi_le hT
    _ = _ := by simp

theorem c3_nonneg : 0 ≤ C3.c3 := by
  unfold C3.c3
  have := Real.arccos_nonneg (5 / 6)
  have := Real.pi_pos
  positivity

theorem aM_nonneg : 0 ≤ aM := by
  unfold aM; norm_num

end SwL

/-- **Q5.** Good labels for the switched layout, minimum degree 3 and maximum degree 4,
conditional on the two per-vertex claims. -/
theorem goodLabelsSw_of (hz : ZeroVertexClaim) (hf : FrontierVertexClaim) :
    GoodLabelsSw C3.c3 aM := by
  intro ε hε
  obtain ⟨η₁, hη₁, hz'⟩ := hz (ε / 4) (by positivity)
  obtain ⟨η₂, hη₂, hf'⟩ := hf (ε / 4) (by positivity)
  obtain ⟨K, hK⟩ := T2.degreeLabels (min η₁ η₂) (lt_min hη₁ hη₂)
  set T₀ : ℕ := ⌈2 / ε⌉₊ + 1 with hT₀
  set q : ℕ := ⌈8 / ε⌉₊ + 1 with hq
  set M : ℕ := T₀ * q with hM
  set D : ℝ := L4.depBound (K + 1) with hDdef
  set Mc : ℝ := 4 * (M : ℝ) + 6 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 hT' : (1 : ℝ) ≤ T₀ := by exact_mod_cast (by omega : 1 ≤ T₀)
  have hTpos : (0 : ℝ) < T₀ := by linarith
  have hTε : 1 / (T₀ : ℝ) ^ 2 ≤ ε / 2 := by
    have h1 : (2 / ε : ℝ) ≤ T₀ := by
      have := Nat.le_ceil (2 / ε)
      push_cast [hT₀]
      linarith
    have h2' : 1 / (T₀ : ℝ) ^ 2 ≤ 1 / T₀ := by
      apply one_div_le_one_div_of_le hTpos
      nlinarith
    have h3' : 1 / (T₀ : ℝ) ≤ ε / 2 := by
      rw [div_le_iff₀ hTpos]
      rw [div_le_iff₀ hε] at h1
      linarith
    linarith
  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 = T₀ := 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
  -- the coefficient bound and the expected counts
  set β : ℝ := C3.c3 * (degreeCount G 3 : ℝ) + aM * (degreeCount G 4 : ℝ) with hβ
  have hβ0 : 0 ≤ β := by
    have := SwL.c3_nonneg
    have := SwL.aM_nonneg
    positivity
  have hZ := sum_zero_le hmin hmax hs hcorr (min_le_left η₁ η₂) hz'
  have hF := fun (τ : ℝ) (hτ : τ ≠ 0) =>
    sum_front_le hmin hmax hs hcorr (min_le_right η₁ η₂) hf' hτ
  have hIn : ∀ i : ℕ, ∑ v, (stdGaussian (GaussianField.Sample n)).real
      (innerEv G vec (-(i : ℝ) / q) v) ≤ β + n * (ε / 4) := by
    intro i
    rcases Nat.eq_zero_or_pos i with rfl | hi
    · simp only [Nat.cast_zero, neg_zero, zero_div]
      have h0 : 0 ≤ ∑ v, (stdGaussian (GaussianField.Sample n)).real (crossPosEv G vec v) :=
        Finset.sum_nonneg fun _ _ => measureReal_nonneg
      linarith [hZ.1]
    · have hτ : -(i : ℝ) / q < 0 := by
        apply div_neg_of_neg_of_pos _ hq'
        have : (0 : ℝ) < i := by exact_mod_cast hi
        linarith
      exact (hF _ hτ.ne).1 hτ
  have hOut : ∀ i : ℕ, ∑ v, (stdGaussian (GaussianField.Sample n)).real
      (outerEv G vec ((i : ℝ) / q) v) ≤ β + n * (ε / 4) := by
    intro i
    rcases Nat.eq_zero_or_pos i with rfl | hi
    · simp only [Nat.cast_zero, zero_div]
      have h0 : 0 ≤ ∑ v, (stdGaussian (GaussianField.Sample n)).real (crossNegEv G vec v) :=
        Finset.sum_nonneg fun _ _ => measureReal_nonneg
      linarith [hZ.2]
    · have hτ : 0 < (i : ℝ) / q := by
        have : (0 : ℝ) < i := by exact_mod_cast hi
        positivity
      exact (hF _ hτ.ne').2 hτ
  -- a good sample
  obtain ⟨x, hxN, hx⟩ := exists_notMem_null_le_integral
    (SwL.integrable_devTotal G vec M q (T₀ : ℝ)) (lab_injective_ae hs)
  set dev := SwL.devTotal G vec M q (T₀ : ℝ) x with hdev_def
  have hdev : dev ≤ ε / 10 * n :=
    hx.trans ((SwL.devTotal_integral_le G vec hs hmax M q (T₀ : ℝ)).trans hsqrt)
  have hinjx : Function.Injective (lab vec x) := by
    by_contra h'
    exact hxN h'
  refine ⟨lab vec x, hinjx, ?_, ?_, ?_, ?_⟩
  · -- inner frontiers below zero
    intro t ht
    by_cases htT : t < -(T₀ : ℝ)
    · have h1 := C3.inner_tail G (lab vec x) htT.le
      have heq : (Finset.univ.filter fun v => lab vec x v ≤ -(T₀ : ℝ)) =
          Finset.univ.filter fun v => x ∈ lowTailEv vec (T₀ : ℝ) v :=
        Finset.filter_congr fun v _ => Iff.rfl
      rw [heq] at h1
      have h2' := L4.card_le_sum_add_dev (lowTailEv vec (T₀ : ℝ)) x
      have h3' := SwL.sum_lowTail_le hs hTpos
      have h4 := (SwL.dev_rest_le (G := G) (vec := vec) (M := M) (q := q) (T := (T₀ : ℝ)) x).1
      have h1' : ((C3.innerFrontier G (lab vec x) t).card : ℝ) ≤
          ((Finset.univ.filter fun v => x ∈ lowTailEv vec (T₀ : ℝ) v).card : ℝ) := by
        exact_mod_cast h1
      have : (n : ℝ) * (1 / (T₀ : ℝ) ^ 2) ≤ n * (ε / 2) := mul_le_mul_of_nonneg_left hTε hn0
      linarith [hβ, hdev_def]
    · obtain ⟨i, hiK, hlo, hhi⟩ := C3.Labels.exists_index_neg (K := M) hq0 ht
        (by rw [neg_div, hKq]; linarith)
      have hg := SwL.inner_grid4 G hmax (lab vec x) hlo hhi
      have hcl : cellLo M q (M - 1 - i) = -((i : ℝ) + 1) / q := by
        unfold cellLo
        rw [Nat.cast_sub (by omega), Nat.cast_sub (by omega)]
        push_cast
        ring
      have hch : cellHi M q (M - 1 - i) = -(i : ℝ) / q := by
        unfold cellHi
        rw [Nat.cast_sub (by omega), Nat.cast_sub (by omega)]
        push_cast
        ring
      rw [innerFrontier_eq, innerFrontier_eq, cellSet_eq] at hg
      have hg' : ((Finset.univ.filter fun v => x ∈ innerEv G vec t v).card : ℝ) ≤
          ((Finset.univ.filter fun v => x ∈ innerEv G vec (-(i : ℝ) / q) v).card : ℝ) +
          4 * ((Finset.univ.filter fun v =>
            x ∈ cellEv vec (-((i : ℝ) + 1) / q) (-(i : ℝ) / q) v).card : ℝ) := by
        exact_mod_cast hg
      have a1 := L4.card_le_sum_add_dev (innerEv G vec (-(i : ℝ) / q)) x
      have a2 := hIn i
      have a3 := SwL.dev_inner_le (G := G) (vec := vec) (q := q) (T := (T₀ : ℝ)) x hiK.le
      have b1 := L4.card_le_sum_add_dev
        (cellEv vec (cellLo M q (M - 1 - i)) (cellHi M q (M - 1 - i))) x
      have b2 := sum_cell_le G vec hs (a := cellLo M q (M - 1 - i))
        (b := cellHi M q (M - 1 - i))
        (by rw [hcl, hch]; apply div_le_div_of_nonneg_right _ hq'.le; linarith)
      have b3 := SwL.dev_cell_le (G := G) (vec := vec) (M := M) (q := q) (T := (T₀ : ℝ)) x
        (i := M - 1 - i) (by omega)
      have hw : cellHi M q (M - 1 - i) - cellLo M q (M - 1 - i) = 1 / q := by
        rw [hcl, hch]
        field_simp
        ring
      rw [hw] at b2
      rw [hcl, hch] at b1 b2 b3
      rw [innerFrontier_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
      linarith [hβ, hdev_def]
  · -- outer frontiers above zero
    intro t ht
    by_cases htT : (T₀ : ℝ) ≤ t
    · have h1 := C3.outer_tail G (lab vec x) htT
      have heq : (Finset.univ.filter fun v => (T₀ : ℝ) < lab vec x v) =
          Finset.univ.filter fun v => x ∈ highTailEv vec (T₀ : ℝ) v :=
        Finset.filter_congr fun v _ => Iff.rfl
      rw [heq] at h1
      have h2' := L4.card_le_sum_add_dev (highTailEv vec (T₀ : ℝ)) x
      have h3' := SwL.sum_highTail_le hs hTpos
      have h4 := (SwL.dev_rest_le (G := G) (vec := vec) (M := M) (q := q) (T := (T₀ : ℝ)) x).2.1
      have h1' : ((C3.outerFrontier G (lab vec x) t).card : ℝ) ≤
          ((Finset.univ.filter fun v => x ∈ highTailEv vec (T₀ : ℝ) v).card : ℝ) := by
        exact_mod_cast h1
      have : (n : ℝ) * (1 / (T₀ : ℝ) ^ 2) ≤ n * (ε / 2) := mul_le_mul_of_nonneg_left hTε hn0
      linarith [hβ, hdev_def]
    · obtain ⟨j, hjK, hlo, hhi⟩ := C3.Labels.exists_index_pos (K := M) hq0 ht
        (by rw [hKq]; linarith)
      have hg := L4.outer_grid4 G hmax (lab vec x) hlo hhi
      have hcl : cellLo M q (M + j) = (j : ℝ) / q := by
        unfold cellLo
        push_cast
        ring
      have hch : cellHi M q (M + j) = ((j : ℝ) + 1) / q := by
        unfold cellHi
        push_cast
        ring
      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 ((j : ℝ) / q) v).card : ℝ) +
          4 * ((Finset.univ.filter fun v =>
            x ∈ cellEv vec ((j : ℝ) / q) (((j : ℝ) + 1) / q) v).card : ℝ) := by
        exact_mod_cast hg
      have a1 := L4.card_le_sum_add_dev (outerEv G vec ((j : ℝ) / q)) x
      have a2 := hOut j
      have a3 := SwL.dev_outer_le (G := G) (vec := vec) (q := q) (T := (T₀ : ℝ)) x hjK.le
      have b1 := L4.card_le_sum_add_dev (cellEv vec (cellLo M q (M + j)) (cellHi M q (M + j))) x
      have b2 := sum_cell_le G vec hs (a := cellLo M q (M + j)) (b := cellHi M q (M + j))
        (by rw [hcl, hch]; apply div_le_div_of_nonneg_right _ hq'.le; linarith)
      have b3 := SwL.dev_cell_le (G := G) (vec := vec) (M := M) (q := q) (T := (T₀ : ℝ)) x
        (i := M + j) (by omega)
      have hw : cellHi M q (M + j) - cellLo M q (M + j) = 1 / q := by
        rw [hcl, hch]
        field_simp
        ring
      rw [hw] at b2
      rw [hcl, hch] at b1 b2 b3
      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
      linarith [hβ, hdev_def]
  · -- `L̂₀`
    rw [hatL0_eq]
    push_cast
    have a1 := L4.card_le_sum_add_dev (innerEv G vec 0) x
    have a2 := L4.card_le_sum_add_dev (crossPosEv G vec) x
    have a3 := hZ.1
    have a4 := SwL.dev_inner_le (G := G) (vec := vec) (M := M) (q := q) (T := (T₀ : ℝ)) x (i := 0)
      (Nat.zero_le _)
    have a5 := (SwL.dev_rest_le (G := G) (vec := vec) (M := M) (q := q) (T := (T₀ : ℝ)) x).2.2.1
    simp only [Nat.cast_zero, neg_zero, zero_div] at a4
    rw [← hdev_def] at a4 a5
    rw [← hβ] at a3
    have s1 := add_le_add a1 a2
    have s2 : (n : ℝ) * (ε / 4) + 2 * dev ≤ ε * n := by
      have := mul_nonneg hε.le hn0
      linarith
    linarith
  · -- `L̂₀'`
    rw [hatL0'_eq]
    push_cast
    have a1 := L4.card_le_sum_add_dev (outerEv G vec 0) x
    have a2 := L4.card_le_sum_add_dev (crossNegEv G vec) x
    have a3 := hZ.2
    have a4 := SwL.dev_outer_le (G := G) (vec := vec) (M := M) (q := q) (T := (T₀ : ℝ)) x (i := 0)
      (Nat.zero_le _)
    have a5 := (SwL.dev_rest_le (G := G) (vec := vec) (M := M) (q := q) (T := (T₀ : ℝ)) x).2.2.2
    simp only [Nat.cast_zero, zero_div] at a4
    rw [← hdev_def] at a4 a5
    rw [← hβ] at a3
    have s1 := add_le_add a1 a2
    have s2 : (n : ℝ) * (ε / 4) + 2 * dev ≤ ε * n := by
      have := mul_nonneg hε.le hn0
      linarith
    linarith

end Sw4
end CubicPathwidth

#print axioms CubicPathwidth.Sw4.goodLabelsSw_of