CubicPathwidth.Sw4.GoodLabelsB

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

import CubicPathwidth.Sw4.GoodLabelsA
import CubicPathwidth.T3.GoodLabelsCount5
import CubicPathwidth.T3.Constants
import CubicPathwidth.T2.Charging

/-!
# Good labels for the switched layout: per-vertex bounds and charging

For each vertex `v` of a graph with all degrees in `{3,4}`, the neighbors are listed with
the degree-3 ones first (`vertex_enum`), so that the edge floors of `T2.degreeLabels`
become `typeFloors d k₃ k₄` for the type `(d; k₃, k₄)` of `v`. The events of `v` are then
contained in those of `zeroProb`, `zeroProb'` and `frontierProb` with `a = vec v` and
`b` the listed neighbor vectors. `T2.charging` sums the per-type bounds
`C_v + λ_T(t) ≤ a_d + δ` to `∑ C_v ≤ c₃ n₃ + a_M n₄ + n δ`.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace Sw4
namespace SwL

open T2 T2.GLC T3

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

/-! ## Floors and neighbor types -/

theorem edgeFloor_eq_rFloor {i j : ℕ} (hi : i = 3 ∨ i = 4) (hj : j = 3 ∨ j = 4) :
    edgeFloor i j = rFloor i j := by
  rcases hi with rfl | rfl <;> rcases hj with rfl | rfl <;>
    simp [edgeFloor, T3.rFloor_33, T3.rFloor_34, T3.rFloor_43, T3.rFloor_44]

theorem maxDeg5 (hmax : MaxDegreeAtMost 4 G) : MaxDegreeAtMost 5 G := by
  unfold MaxDegreeAtMost at *
  intro v
  exact (hmax v).trans (by norm_num)

theorem nbrCount_add (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G) (v : Fin n) :
    nbrCount G v 3 + nbrCount G v 4 = G.degree v := by
  have h := T3.GLC5.nbrCount_sum hmin (maxDeg5 hmax) v
  have h5 : nbrCount G v 5 = 0 := by
    rw [GLC.nbrCount_eq, Finset.card_eq_zero, Finset.filter_eq_empty_iff]
    intro u _
    rcases GLC.deg_cases hmin hmax u with h' | h' <;> omega
  omega

/-- The neighbors of `v`, degree-3 ones first, with inner products above the type floors. -/
theorem vertex_enum (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G) {η η' : ℝ}
    (hedge : ∀ u v, G.Adj u v →
      (1 - η) * edgeFloor (G.degree u) (G.degree v) ≤ ⟪vec u, vec v⟫)
    (hηη : η ≤ η') (v : Fin n) :
    ∃ f : Fin (G.degree v) → Fin n, (∀ i, G.Adj v (f i)) ∧ (∀ z, G.Adj v z → ∃ i, f i = z) ∧
      ∀ i, (1 - η') * typeFloors (G.degree v) (nbrCount G v 3) (nbrCount G v 4) i ≤
        ⟪vec v, vec (f i)⟫ := by
  have hcard : (G.neighborFinset v).card = G.degree v := G.card_neighborFinset_eq_degree v
  have hk : ∀ a ∈ G.neighborFinset v, G.degree a = 3 ∨ G.degree a = 4 ∨ G.degree a = 5 :=
    fun a _ => (T3.GLC5.deg_cases5 hmin (maxDeg5 hmax) a)
  obtain ⟨f, hfm, hfs, hfp⟩ :=
    T3.GLC5.exists_enum3 (G.neighborFinset v) (fun a => G.degree a) _ hcard hk
  refine ⟨f, fun i => (G.mem_neighborFinset v _).mp (hfm i),
    fun z hz => hfs z ((G.mem_neighborFinset v z).mpr hz), fun i => ?_⟩
  have hadj : G.Adj v (f i) := (G.mem_neighborFinset v _).mp (hfm i)
  have h := hedge v (f i) hadj
  have hpos := T3.GLC5.typeFloors_pos (G.degree v) (nbrCount G v 3) (nbrCount G v 4) i
  have hlow : (1 - η') * typeFloors (G.degree v) (nbrCount G v 3) (nbrCount G v 4) i ≤
      (1 - η) * typeFloors (G.degree v) (nbrCount G v 3) (nbrCount G v 4) i := by nlinarith
  refine hlow.trans (le_trans (le_of_eq ?_) h)
  congr 1
  rw [edgeFloor_eq_rFloor (GLC.deg_cases hmin hmax v) (GLC.deg_cases hmin hmax (f i))]
  obtain ⟨p3, p4, p5⟩ := hfp i
  have e3 : nbrCount G v 3 = ((G.neighborFinset v).filter fun a => G.degree a = 3).card :=
    GLC.nbrCount_eq v 3
  have e4 : nbrCount G v 4 = ((G.neighborFinset v).filter fun a => G.degree a = 4).card :=
    GLC.nbrCount_eq v 4
  rw [typeFloors, e3, e4]
  by_cases h1 : (i : ℕ) < ((G.neighborFinset v).filter fun a => G.degree a = 3).card
  · simp only [h1, ↓reduceIte, p3 h1]
  · simp only [h1, ↓reduceIte]
    by_cases h2 : (i : ℕ) <
        ((G.neighborFinset v).filter fun a => G.degree a = 3).card +
          ((G.neighborFinset v).filter fun a => G.degree a = 4).card
    · simp only [h2, ↓reduceIte, p4 (not_lt.mp h1) h2]
    · exfalso
      have := p5 (not_lt.mp h2)
      rcases GLC.deg_cases hmin hmax (f i) with h' | h' <;> omega

/-! ## Per-vertex event inclusions -/

theorem card_filter_nbr_le {v : Fin n} {d : ℕ} {f : Fin d → Fin n}
    (hfs : ∀ z, G.Adj v z → ∃ i, f i = z) (p : Fin n → Prop) :
    ((G.neighborFinset v).filter p).card ≤ (Finset.univ.filter fun i => p (f i)).card := by
  have hsub : (G.neighborFinset v).filter p ⊆
      (Finset.univ.filter fun i => p (f i)).image f := by
    intro z hz
    rw [Finset.mem_filter, G.mem_neighborFinset] at hz
    obtain ⟨i, rfl⟩ := hfs z hz.1
    exact Finset.mem_image.mpr ⟨i, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hz.2⟩, rfl⟩
  exact (Finset.card_le_card hsub).trans Finset.card_image_le

variable {d : ℕ} {f : Fin d → Fin n}

theorem prob_zero_le (v : Fin n)
    (hfs : ∀ z, G.Adj v z → ∃ i, f i = z) :
    (stdGaussian (GaussianField.Sample n)).real (innerEv G vec 0 v) +
        (stdGaussian (GaussianField.Sample n)).real (crossPosEv G vec v) ≤
      zeroProb (vec v) (fun i => vec (f i)) := by
  unfold zeroProb
  apply add_le_add
  · refine measureReal_mono ?_ (measure_ne_top _ _)
    intro x hx
    simp only [innerEv, Set.mem_ofPred_eq, C3.mem_innerFrontier] at hx ⊢
    obtain ⟨hv, w, hw, hwt⟩ := hx
    obtain ⟨i, rfl⟩ := hfs w hw
    exact ⟨hv, i, hwt⟩
  · refine measureReal_mono ?_ (measure_ne_top _ _)
    intro x hx
    simp only [crossPosEv, Set.mem_ofPred_eq, mem_hatD] at hx ⊢
    obtain ⟨hd, hv⟩ := hx
    rcases hd with ⟨h1, -⟩ | ⟨-, h2⟩
    · exact absurd hv (not_lt.mpr h1)
    · refine ⟨hv, h2.trans ?_⟩
      convert card_filter_nbr_le hfs (fun z => lab vec x z ≤ 0)
      all_goals rfl

theorem prob_zero'_le (v : Fin n)
    (hfs : ∀ z, G.Adj v z → ∃ i, f i = z) :
    (stdGaussian (GaussianField.Sample n)).real (outerEv G vec 0 v) +
        (stdGaussian (GaussianField.Sample n)).real (crossNegEv G vec v) ≤
      zeroProb' (vec v) (fun i => vec (f i)) := by
  unfold zeroProb'
  apply add_le_add
  · refine measureReal_mono ?_ (measure_ne_top _ _)
    intro x hx
    simp only [outerEv, Set.mem_ofPred_eq, C3.mem_outerFrontier] at hx ⊢
    obtain ⟨hv, w, hw, hwt⟩ := hx
    obtain ⟨i, rfl⟩ := hfs w hw
    exact ⟨hv, i, hwt⟩
  · refine measureReal_mono ?_ (measure_ne_top _ _)
    intro x hx
    simp only [crossNegEv, Set.mem_ofPred_eq, mem_hatD] at hx ⊢
    obtain ⟨hd, hv⟩ := hx
    rcases hd with ⟨-, h1⟩ | ⟨h2, -⟩
    · refine ⟨hv, h1.trans ?_⟩
      convert card_filter_nbr_le hfs (fun z => 0 < lab vec x z)
      all_goals rfl
    · exact absurd hv (not_le.mpr h2)

theorem prob_inner_le (v : Fin n) (hfs : ∀ z, G.Adj v z → ∃ i, f i = z) {τ : ℝ} (hτ : τ < 0) :
    (stdGaussian (GaussianField.Sample n)).real (innerEv G vec τ v) ≤
      frontierProb τ (vec v) (fun i => vec (f i)) := by
  unfold frontierProb
  simp only [not_lt.mpr hτ.le, ↓reduceIte]
  refine measureReal_mono ?_ (measure_ne_top _ _)
  intro x hx
  simp only [innerEv, Set.mem_ofPred_eq, C3.mem_innerFrontier] at hx ⊢
  obtain ⟨hv, w, hw, hwt⟩ := hx
  obtain ⟨i, rfl⟩ := hfs w hw
  exact ⟨hv, i, hwt⟩

theorem prob_outer_le (v : Fin n) (hfs : ∀ z, G.Adj v z → ∃ i, f i = z) {τ : ℝ} (hτ : 0 < τ) :
    (stdGaussian (GaussianField.Sample n)).real (outerEv G vec τ v) ≤
      frontierProb τ (vec v) (fun i => vec (f i)) := by
  unfold frontierProb
  simp only [hτ, ↓reduceIte]
  refine measureReal_mono ?_ (measure_ne_top _ _)
  intro x hx
  simp only [outerEv, Set.mem_ofPred_eq, C3.mem_outerFrontier] at hx ⊢
  obtain ⟨hv, w, hw, hwt⟩ := hx
  obtain ⟨i, rfl⟩ := hfs w hw
  exact ⟨hv, i, hwt⟩

/-! ## Charging -/

theorem sum_le_charge (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G)
    (C : Fin n → ℝ) (t δ : ℝ)
    (h : ∀ v, C v + transferTerm (G.degree v) (nbrCount G v 3) (nbrCount G v 4) 0 t 0 0 ≤
      coeff C3.c3 aM 0 (G.degree v) + δ) :
    ∑ v, C v ≤ C3.c3 * (degreeCount G 3 : ℝ) + aM * (degreeCount G 4 : ℝ) + n * δ := by
  have hc := T2.charging n G hmin hmax (fun v => C v - δ) C3.c3 aM t ?_ ?_
  · rw [Finset.sum_sub_distrib] at hc
    simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] at hc
    linarith
  · intro v hv
    have := h v
    rw [hv] at this
    simp only [transferTerm, coeff, ↓reduceIte] at this
    linarith
  · intro v hv
    have := h v
    rw [hv] at this
    simp only [transferTerm, coeff, show (4 : ℕ) ≠ 3 by norm_num, ↓reduceIte] at this
    linarith

/-! ## Summed bounds from the two vertex claims -/

variable {η : ℝ}

theorem sum_zero_le (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G)
    (hs : Sch G K vec)
    (hedge : ∀ u v, G.Adj u v →
      (1 - η) * edgeFloor (G.degree u) (G.degree v) ≤ ⟪vec u, vec v⟫)
    {η₁ δ : ℝ} (hη : η ≤ η₁)
    (hz : ∀ (m d k₃ k₄ : ℕ) (a : GaussianField.Sample m) (b : Fin d → GaussianField.Sample m),
      (d = 3 ∨ d = 4) → k₃ + k₄ = d → ‖a‖ = 1 → (∀ i, ‖b i‖ = 1) →
      (∀ i, (1 - η₁) * typeFloors d k₃ k₄ i ≤ ⟪a, b i⟫) →
        zeroProb a b + transferTerm d k₃ k₄ 0 sM 0 0 ≤ coeff C3.c3 aM 0 d + δ ∧
        zeroProb' a b + transferTerm d k₃ k₄ 0 sM 0 0 ≤ coeff C3.c3 aM 0 d + δ) :
    (∑ v, (stdGaussian (GaussianField.Sample n)).real (innerEv G vec 0 v) +
        ∑ v, (stdGaussian (GaussianField.Sample n)).real (crossPosEv G vec v) ≤
      C3.c3 * (degreeCount G 3 : ℝ) + aM * (degreeCount G 4 : ℝ) + n * δ) ∧
    (∑ v, (stdGaussian (GaussianField.Sample n)).real (outerEv G vec 0 v) +
        ∑ v, (stdGaussian (GaussianField.Sample n)).real (crossNegEv G vec v) ≤
      C3.c3 * (degreeCount G 3 : ℝ) + aM * (degreeCount G 4 : ℝ) + n * δ) := by
  rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
  constructor
  · refine sum_le_charge hmin hmax _ sM δ fun v => ?_
    obtain ⟨f, -, hfs, hfl⟩ := vertex_enum hmin hmax hedge hη v
    have h1 := (hz n _ _ _ (vec v) (fun i => vec (f i)) (GLC.deg_cases hmin hmax v)
      (nbrCount_add hmin hmax v) (hs.norm v) (fun i => hs.norm _) hfl).1
    have h2 := prob_zero_le (vec := vec) v hfs
    linarith
  · refine sum_le_charge hmin hmax _ sM δ fun v => ?_
    obtain ⟨f, -, hfs, hfl⟩ := vertex_enum hmin hmax hedge hη v
    have h1 := (hz n _ _ _ (vec v) (fun i => vec (f i)) (GLC.deg_cases hmin hmax v)
      (nbrCount_add hmin hmax v) (hs.norm v) (fun i => hs.norm _) hfl).2
    have h2 := prob_zero'_le (vec := vec) v hfs
    linarith

theorem sum_front_le (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G)
    (hs : Sch G K vec)
    (hedge : ∀ u v, G.Adj u v →
      (1 - η) * edgeFloor (G.degree u) (G.degree v) ≤ ⟪vec u, vec v⟫)
    {η₂ δ : ℝ} (hη : η ≤ η₂)
    (hf : ∀ τ : ℝ, τ ≠ 0 → ∃ t₃₄ : ℝ,
      ∀ (m d k₃ k₄ : ℕ) (a : GaussianField.Sample m) (b : Fin d → GaussianField.Sample m),
        (d = 3 ∨ d = 4) → k₃ + k₄ = d → ‖a‖ = 1 → (∀ i, ‖b i‖ = 1) →
        (∀ i, (1 - η₂) * typeFloors d k₃ k₄ i ≤ ⟪a, b i⟫) →
          frontierProb τ a b + transferTerm d k₃ k₄ 0 t₃₄ 0 0 ≤ coeff C3.c3 aM 0 d + δ)
    {τ : ℝ} (hτ : τ ≠ 0) :
    (τ < 0 → ∑ v, (stdGaussian (GaussianField.Sample n)).real (innerEv G vec τ v) ≤
      C3.c3 * (degreeCount G 3 : ℝ) + aM * (degreeCount G 4 : ℝ) + n * δ) ∧
    (0 < τ → ∑ v, (stdGaussian (GaussianField.Sample n)).real (outerEv G vec τ v) ≤
      C3.c3 * (degreeCount G 3 : ℝ) + aM * (degreeCount G 4 : ℝ) + n * δ) := by
  obtain ⟨t, ht⟩ := hf τ hτ
  constructor
  · intro hneg
    refine sum_le_charge hmin hmax _ t δ fun v => ?_
    obtain ⟨f, -, hfs, hfl⟩ := vertex_enum hmin hmax hedge hη v
    have h1 := ht n _ _ _ (vec v) (fun i => vec (f i)) (GLC.deg_cases hmin hmax v)
      (nbrCount_add hmin hmax v) (hs.norm v) (fun i => hs.norm _) hfl
    have h2 := prob_inner_le (vec := vec) v hfs hneg
    linarith
  · intro hpos
    refine sum_le_charge hmin hmax _ t δ fun v => ?_
    obtain ⟨f, -, hfs, hfl⟩ := vertex_enum hmin hmax hedge hη v
    have h1 := ht n _ _ _ (vec v) (fun i => vec (f i)) (GLC.deg_cases hmin hmax v)
      (nbrCount_add hmin hmax v) (hs.norm v) (fun i => hs.norm _) hfl
    have h2 := prob_outer_le (vec := vec) v hfs hpos
    linarith

end SwL
end Sw4
end CubicPathwidth