CubicPathwidth.T2.GoodLabelsCountB

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

import CubicPathwidth.T2.GoodLabelsCountA

/-!
# Floors, neighbor enumeration and the per-vertex star bound
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace T2
namespace GLC

/-! ## The floors lie in `(0, 1)` -/

theorem r33_pos : 0 < r33 := by
  unfold r33; positivity

theorem r33_lt_one : r33 < 1 := by
  unfold r33
  have h : Real.sqrt 2 < 3 / 2 := by
    rw [Real.sqrt_lt' (by norm_num)]; norm_num
  rw [div_lt_one (by norm_num)]
  linarith

theorem r44_pos : 0 < r44 := by
  unfold r44; positivity

theorem r44_lt_one : r44 < 1 := by
  unfold r44
  have h : Real.sqrt 3 < 2 := by
    rw [Real.sqrt_lt' (by norm_num)]; norm_num
  rw [div_lt_one (by norm_num)]
  exact h

theorem r34_pos : 0 < r34 := by
  unfold r34; exact one_div_pos.mpr (Real.cosh_pos _)

theorem r34_lt_one : r34 < 1 := by
  unfold r34
  have h : 1 < Real.cosh (Real.log 6 / 4) := by
    have h6 : 0 < Real.log 6 := Real.log_pos (by norm_num)
    have hx : Real.log 6 / 4 ≠ 0 := by positivity
    have h1 := Real.add_one_lt_exp hx
    have h2 := Real.add_one_lt_exp (neg_ne_zero.mpr hx)
    rw [Real.cosh_eq]
    linarith
  rw [div_lt_one (by linarith)]
  exact h

theorem edgeFloor_pos (i j : ℕ) : 0 < edgeFloor i j := by
  unfold edgeFloor
  split_ifs <;> first | exact r33_pos | exact r44_pos | exact r34_pos

theorem edgeFloor_lt_one (i j : ℕ) : edgeFloor i j < 1 := by
  unfold edgeFloor
  split_ifs <;> first | exact r33_lt_one | exact r44_lt_one | exact r34_lt_one

theorem floorsThree_pos (k : ℕ) (i : Fin 3) : 0 < floorsThree k i := by
  unfold floorsThree; split_ifs
  · exact r34_pos
  · exact r33_pos

theorem floorsThree_lt_one (k : ℕ) (i : Fin 3) : floorsThree k i < 1 := by
  unfold floorsThree; split_ifs
  · exact r34_lt_one
  · exact r33_lt_one

theorem floorsFour_pos (k : ℕ) (i : Fin 4) : 0 < floorsFour k i := by
  unfold floorsFour; split_ifs
  · exact r34_pos
  · exact r44_pos

theorem floorsFour_lt_one (k : ℕ) (i : Fin 4) : floorsFour k i < 1 := by
  unfold floorsFour; split_ifs
  · exact r34_lt_one
  · exact r44_lt_one

/-! ## Choice of `η` from the continuity claim -/

theorem eta_exists (hC : StarBoundContClaim) {δ : ℝ} (hδ : 0 < δ) :
    ∃ η : ℝ, 0 < η ∧ η < 1 ∧
      (∀ 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) τ + δ) ∧
      (∀ 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) τ + δ) := by
  have h3 : ∀ k : Fin 4, ∃ η : ℝ, 0 < η ∧ ∀ r' : Fin 3 → ℝ,
      (∀ i, (1 - η) * floorsThree k i ≤ r' i ∧ r' i ≤ floorsThree k i) →
        ∀ τ ∈ Set.Icc (-3 : ℝ) 3, starBound r' τ ≤ starBound (floorsThree k) τ + δ :=
    fun k => hC 3 (floorsThree k) (fun i => ⟨floorsThree_pos _ i, floorsThree_lt_one _ i⟩) δ hδ
  have h4 : ∀ k : Fin 5, ∃ η : ℝ, 0 < η ∧ ∀ r' : Fin 4 → ℝ,
      (∀ i, (1 - η) * floorsFour k i ≤ r' i ∧ r' i ≤ floorsFour k i) →
        ∀ τ ∈ Set.Icc (-3 : ℝ) 3, starBound r' τ ≤ starBound (floorsFour k) τ + δ :=
    fun k => hC 4 (floorsFour k) (fun i => ⟨floorsFour_pos _ i, floorsFour_lt_one _ i⟩) δ hδ
  choose e3 he3p he3 using h3
  choose e4 he4p he4 using h4
  obtain ⟨i3, -, hi3⟩ := Finset.exists_min_image Finset.univ e3 ⟨0, Finset.mem_univ _⟩
  obtain ⟨i4, -, hi4⟩ := Finset.exists_min_image Finset.univ e4 ⟨0, Finset.mem_univ _⟩
  refine ⟨min (1 / 2) (min (e3 i3) (e4 i4)), ?_, ?_, ?_, ?_⟩
  · exact lt_min (by norm_num) (lt_min (he3p _) (he4p _))
  · exact lt_of_le_of_lt (min_le_left _ _) (by norm_num)
  · intro k hk r' hr τ hτ
    have := he3 ⟨k, by omega⟩ r' ?_ τ hτ
    · simpa using this
    · intro i
      refine ⟨le_trans ?_ (hr i).1, (hr i).2⟩
      have hη : min (1 / 2) (min (e3 i3) (e4 i4)) ≤ e3 ⟨k, by omega⟩ :=
        (min_le_right _ _).trans ((min_le_left _ _).trans (hi3 _ (Finset.mem_univ _)))
      have hp := floorsThree_pos k i
      nlinarith
  · intro k hk r' hr τ hτ
    have := he4 ⟨k, by omega⟩ r' ?_ τ hτ
    · simpa using this
    · intro i
      refine ⟨le_trans ?_ (hr i).1, (hr i).2⟩
      have hη : min (1 / 2) (min (e3 i3) (e4 i4)) ≤ e4 ⟨k, by omega⟩ :=
        (min_le_right _ _).trans ((min_le_right _ _).trans (hi4 _ (Finset.mem_univ _)))
      have hp := floorsFour_pos k i
      nlinarith

/-! ## Enumeration of a finite set, a distinguished part first -/

theorem exists_enum {α : Type*} (N : Finset α) (p : α → Prop) [DecidablePred p] (d : ℕ) (hd : N.card = d) :
    ∃ f : Fin d → α, (∀ i, f i ∈ N) ∧ (∀ z ∈ N, ∃ i, f i = z) ∧
      ∀ i : Fin d, p (f i) ↔ (i : ℕ) < (N.filter p).card := by
  set A := N.filter p with hA
  set B := N.filter (fun a => ¬ p a) with hB
  set l : List α := A.toList ++ B.toList with hl
  have hcard : A.card + B.card = d := by
    rw [hA, hB, Finset.card_filter_add_card_filter_not]
    exact hd
  have hlen : l.length = d := by
    rw [hl, List.length_append, Finset.length_toList, Finset.length_toList]
    exact hcard
  have hmem : ∀ a, a ∈ l ↔ a ∈ N := by
    intro a
    rw [hl, List.mem_append, Finset.mem_toList, Finset.mem_toList, hA, hB, Finset.mem_filter,
      Finset.mem_filter]
    constructor
    · rintro (h | h)
      · exact h.1
      · exact h.1
    · intro h
      by_cases hp : p a
      · exact Or.inl ⟨h, hp⟩
      · exact Or.inr ⟨h, hp⟩
  refine ⟨fun i => l[(i : ℕ)]'(by omega), ?_, ?_, ?_⟩
  · intro i
    exact (hmem _).mp (List.getElem_mem _)
  · intro z hz
    obtain ⟨j, hj, hjz⟩ := List.getElem_of_mem ((hmem z).mpr hz)
    exact ⟨⟨j, by omega⟩, hjz⟩
  · intro i
    by_cases hi : (i : ℕ) < A.card
    · have hlt : (i : ℕ) < A.toList.length := by rwa [Finset.length_toList]
      have : l[(i : ℕ)]'(by omega) = A.toList[(i : ℕ)]'hlt :=
        List.getElem_append_left hlt
      simp only [this]
      have hmA : A.toList[(i : ℕ)]'hlt ∈ A := Finset.mem_toList.mp (List.getElem_mem _)
      exact ⟨fun _ => hi, fun _ => (Finset.mem_filter.mp hmA).2⟩
    · have hge : A.toList.length ≤ (i : ℕ) := by rw [Finset.length_toList]; omega
      have hlt : (i : ℕ) - A.toList.length < B.toList.length := by
        rw [Finset.length_toList, Finset.length_toList]; omega
      have : l[(i : ℕ)]'(by omega) = B.toList[(i : ℕ) - A.toList.length]'hlt :=
        List.getElem_append_right hge
      simp only [this]
      have hmB : B.toList[(i : ℕ) - A.toList.length]'hlt ∈ B :=
        Finset.mem_toList.mp (List.getElem_mem _)
      exact ⟨fun h => absurd h (Finset.mem_filter.mp hmB).2, fun h => absurd h hi⟩

/-! ## Per-vertex bounds -/

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

theorem prob_outer_le_aux (hS : HetStarClaim) (hs : Sch G K vec) (v : Fin n) (d : ℕ)
    (r' : Fin d → ℝ) (hr' : ∀ i, 0 < r' i ∧ r' i < 1) (f : Fin d → Fin n)
    (hf : ∀ z, G.Adj v z → ∃ i, f i = z) (hcorr : ∀ i, r' i ≤ ⟪vec v, vec (f i)⟫) (τ : ℝ) :
    (stdGaussian (GaussianField.Sample n)).real (outerEv G vec τ v) ≤ starBound r' τ := by
  have key := hS n d r' hr' (vec v) (fun i => vec (f i)) (hs.norm v) (fun i => hs.norm _) hcorr τ
  refine le_trans (measureReal_mono ?_) key
  intro x hx
  simp only [outerEv, Set.mem_ofPred_eq, C3.mem_outerFrontier] at hx ⊢
  obtain ⟨hv, u, hu, hut⟩ := hx
  obtain ⟨i, hi⟩ := hf u hu
  exact ⟨hv, i, by simpa [lab, hi] using hut⟩

theorem deg_cases (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G) (u : Fin n) :
    G.degree u = 3 ∨ G.degree u = 4 := by
  have h1 : 3 ≤ G.degree u := hmin u
  have h2 : G.degree u ≤ 4 := hmax u
  omega

theorem nbrCount_eq (v : Fin n) (d : ℕ) :
    nbrCount G v d = ((G.neighborFinset v).filter fun u => G.degree u = d).card := by
  unfold nbrCount
  congr

theorem edgeFloor_three (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G) (u : Fin n) :
    edgeFloor 3 (G.degree u) = if G.degree u = 4 then r34 else r33 := by
  rcases deg_cases hmin hmax u with h | h <;> simp [edgeFloor, h]

theorem edgeFloor_four (hmin : MinDegreeAtLeast 3 G) (hmax : MaxDegreeAtMost 4 G) (u : Fin n) :
    edgeFloor 4 (G.degree u) = if G.degree u = 3 then r34 else r44 := by
  rcases deg_cases hmin hmax u with h | h <;> simp [edgeFloor, h]

variable {η : ℝ}

theorem prob_outer_le_three (hS : HetStarClaim) (hs : Sch G K vec) (hmin : MinDegreeAtLeast 3 G)
    (hmax : MaxDegreeAtMost 4 G) (hη0 : 0 < η) (hη1 : η < 1)
    (hedge : ∀ u v, G.Adj u v →
      (1 - η) * edgeFloor (G.degree u) (G.degree v) ≤ ⟪vec u, vec v⟫)
    (v : Fin n) (hv : G.degree v = 3) (τ : ℝ) :
    (stdGaussian (GaussianField.Sample n)).real (outerEv G vec τ v) ≤
      starBound (fun i : Fin 3 => (1 - η) * floorsThree (nbrCount G v 4) i) τ := by
  have hcard : (G.neighborFinset v).card = 3 := by rw [G.card_neighborFinset_eq_degree]; exact hv
  obtain ⟨f, hfm, hfs, hfp⟩ := exists_enum (G.neighborFinset v) (fun u => G.degree u = 4) 3 hcard
  refine prob_outer_le_aux hS hs v 3 _ ?_ f
    (fun z hz => hfs z ((G.mem_neighborFinset v z).mpr hz)) ?_ τ
  · intro i
    have := floorsThree_pos (nbrCount G v 4) i
    have := floorsThree_lt_one (nbrCount G v 4) i
    constructor <;> nlinarith
  · intro i
    have hadj : G.Adj v (f i) := (G.mem_neighborFinset v _).mp (hfm i)
    have h := hedge v (f i) hadj
    rw [hv, edgeFloor_three hmin hmax] at h
    refine le_trans (le_of_eq ?_) h
    congr 1
    rw [floorsThree, nbrCount_eq]
    have := hfp i
    by_cases h4 : G.degree (f i) = 4
    · have h6 := this.mp h4
      simp only [h4, h6, ite_true]
    · have h5 : ¬ (i : ℕ) < _ := fun h => h4 (this.mpr h)
      simp only [h4, h5, ite_false]

theorem prob_outer_le_four (hS : HetStarClaim) (hs : Sch G K vec) (hmin : MinDegreeAtLeast 3 G)
    (hmax : MaxDegreeAtMost 4 G) (hη0 : 0 < η) (hη1 : η < 1)
    (hedge : ∀ u v, G.Adj u v →
      (1 - η) * edgeFloor (G.degree u) (G.degree v) ≤ ⟪vec u, vec v⟫)
    (v : Fin n) (hv : G.degree v = 4) (τ : ℝ) :
    (stdGaussian (GaussianField.Sample n)).real (outerEv G vec τ v) ≤
      starBound (fun i : Fin 4 => (1 - η) * floorsFour (nbrCount G v 3) i) τ := by
  have hcard : (G.neighborFinset v).card = 4 := by rw [G.card_neighborFinset_eq_degree]; exact hv
  obtain ⟨f, hfm, hfs, hfp⟩ := exists_enum (G.neighborFinset v) (fun u => G.degree u = 3) 4 hcard
  refine prob_outer_le_aux hS hs v 4 _ ?_ f
    (fun z hz => hfs z ((G.mem_neighborFinset v z).mpr hz)) ?_ τ
  · intro i
    have := floorsFour_pos (nbrCount G v 3) i
    have := floorsFour_lt_one (nbrCount G v 3) i
    constructor <;> nlinarith
  · intro i
    have hadj : G.Adj v (f i) := (G.mem_neighborFinset v _).mp (hfm i)
    have h := hedge v (f i) hadj
    rw [hv, edgeFloor_four hmin hmax] at h
    refine le_trans (le_of_eq ?_) h
    congr 1
    rw [floorsFour, nbrCount_eq]
    have := hfp i
    by_cases h3 : G.degree (f i) = 3
    · have h6 := this.mp h3
      simp only [h3, h6, ite_true]
    · have h5 : ¬ (i : ℕ) < _ := fun h => h3 (this.mpr h)
      simp only [h3, h5, ite_false]

end GLC
end T2
end CubicPathwidth