CubicPathwidth.T3.GoodLabelsCount5A

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

import CubicPathwidth.T3.Defs
import CubicPathwidth.T2.GoodLabelsCountA

/-!
# Concentration and grid comparison for maximum degree 5

Degree-5 versions of the ball bound, the concentration of local counts, the outer
grid comparison and the total deviation of `T2/GoodLabelsCountA.lean`.

* `|B_r| + 1 ≤ 2 · 4^r` for `Δ ≤ 5`; dependence bound `2 · 4^(2r)`;
* `outer_grid5`, `outer_tail_low5` with multiplicity five.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace T3
namespace GLC5

open T2

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

theorem card_neighborFinset_le5 (hG : MaxDegreeAtMost 5 G) (v : Fin n) :
    (G.neighborFinset v).card ≤ 5 := by
  have hd := hG v
  change (G.neighborFinset v).card ≤ 5 at hd
  exact hd

theorem next_neighbors_card_le5 (hG : MaxDegreeAtMost 5 G) (v : Fin n) {j : ℕ}
    (hj : 0 < j) {u : Fin n} (hu : u ∈ Locality.sphere G v j) :
    ((G.neighborFinset u) ∩ Locality.sphere G v (j + 1)).card ≤ 4 := by
  classical
  obtain ⟨hvu, hdu⟩ := (Locality.mem_sphere G v u j).mp hu
  obtain ⟨p, hup, hvp, hdp⟩ := Locality.exists_predecessor G hvu (by omega)
  have hpN : p ∈ G.neighborFinset u := (G.mem_neighborFinset u p).mpr hup
  have hsub : (G.neighborFinset u) ∩ Locality.sphere G v (j + 1) ⊆
      (G.neighborFinset u).erase p := by
    intro w hw
    obtain ⟨hwN, hwS⟩ := Finset.mem_inter.mp hw
    apply Finset.mem_erase.mpr
    refine ⟨?_, hwN⟩
    intro heq
    subst w
    have := ((Locality.mem_sphere G v p (j + 1)).mp hwS).2
    omega
  have hc := Finset.card_le_card hsub
  rw [Finset.card_erase_of_mem hpN] at hc
  have hd := card_neighborFinset_le5 G hG u
  omega

theorem sphere_card_succ_le5 (hG : MaxDegreeAtMost 5 G) (v : Fin n) {j : ℕ}
    (hj : 0 < j) :
    (Locality.sphere G v (j + 1)).card ≤ 4 * (Locality.sphere G v j).card := by
  classical
  have hsub : Locality.sphere G v (j + 1) ⊆ (Locality.sphere G v j).biUnion
      (fun u => (G.neighborFinset u) ∩ Locality.sphere G v (j + 1)) := by
    intro w hw
    obtain ⟨hvw, hdw⟩ := (Locality.mem_sphere G v w (j + 1)).mp hw
    obtain ⟨u, hwu, hvu, hdu⟩ := Locality.exists_predecessor G hvw (by omega)
    refine Finset.mem_biUnion.mpr ⟨u, (Locality.mem_sphere G v u j).mpr ⟨hvu, by omega⟩, ?_⟩
    exact Finset.mem_inter.mpr ⟨(G.mem_neighborFinset u w).mpr hwu.symm, hw⟩
  calc
    (Locality.sphere G v (j + 1)).card ≤ ((Locality.sphere G v j).biUnion
        (fun u => (G.neighborFinset u) ∩ Locality.sphere G v (j + 1))).card :=
      Finset.card_le_card hsub
    _ ≤ ∑ u ∈ Locality.sphere G v j,
        ((G.neighborFinset u) ∩ Locality.sphere G v (j + 1)).card :=
      Finset.card_biUnion_le
    _ ≤ ∑ u ∈ Locality.sphere G v j, 4 :=
      Finset.sum_le_sum fun u hu => next_neighbors_card_le5 G hG v hj hu
    _ = 4 * (Locality.sphere G v j).card := by simp [mul_comm]

theorem sphere_card_le5 (hG : MaxDegreeAtMost 5 G) (v : Fin n) (j : ℕ) :
    (Locality.sphere G v (j + 1)).card ≤ 5 * 4 ^ j := by
  induction j with
  | zero => simpa [Locality.sphere_one] using card_neighborFinset_le5 G hG v
  | succ j ih =>
    have h := sphere_card_succ_le5 G hG v (j := j + 1) (by omega)
    calc
      (Locality.sphere G v (j + 1 + 1)).card ≤ 4 * (Locality.sphere G v (j + 1)).card := h
      _ ≤ 4 * (5 * 4 ^ j) := Nat.mul_le_mul_left 4 ih
      _ = 5 * 4 ^ (j + 1) := by ring

/-- `|B_r| + 1 ≤ 2 · 4^r`. -/
theorem ball_card_add_one_le5 (hG : MaxDegreeAtMost 5 G) (v : Fin n) (r : ℕ) :
    (Locality.ball G v r).card + 1 ≤ 2 * 4 ^ r := by
  classical
  induction r with
  | zero => simp
  | succ r ih =>
    have h := sphere_card_le5 G hG v r
    rw [Locality.ball_succ]
    have hc := Finset.card_union_le (Locality.ball G v r) (Locality.sphere G v (r + 1))
    have hp : 1 ≤ 4 ^ r := Nat.one_le_pow _ _ (by norm_num)
    rw [pow_succ]
    omega

/-- The number of vertices potentially dependent on one local event. -/
def depBound5 (r : ℕ) : ℝ := 2 * (4 : ℝ) ^ (2 * r)

theorem depBound5_pos (r : ℕ) : 0 < depBound5 r := by
  unfold depBound5; positivity

/-- Concentration of a local count, maximum degree 5. -/
theorem integral_abs_centeredCount_le5 (hG : MaxDegreeAtMost 5 G)
    (r : ℕ) {E : Fin n → Set (GaussianField.Sample n)} (hE : ∀ v, MeasurableSet (E v))
    (hloc : C3.IsLocal G r E) :
    ∫ x, |C3.centeredCount E x| ∂stdGaussian (GaussianField.Sample n) ≤
      Real.sqrt (n * depBound5 r) := by
  refine (integral_abs_le_sqrt_secondMoment (C3.memLp_centeredCount hE)).trans
    (Real.sqrt_le_sqrt ?_)
  apply secondMoment_sum_le _ (fun v => C3.measurable_centered_term (hE v))
    (fun v x => C3.abs_centered_term_le (E v) x) (fun v => Locality.ball G v (2 * r))
    (depBound5 r)
  · intro v
    have h : ((Locality.ball G v (2 * r)).card : ℝ) + 1 ≤ 2 * (4 : ℝ) ^ (2 * r) := by
      exact_mod_cast ball_card_add_one_le5 G hG v (2 * r)
    dsimp [depBound5]
    linarith
  intro u v huv
  have hd := Locality.disjoint_balls_of_not_mem G huv
  rw [C3.integral_mul_of_disjoint hd (C3.measurable_centered_term (hE u))
    (C3.measurable_centered_term (hE v)) ?_ ?_, C3.integral_centered_term (hE u), zero_mul]
  · intro x x' hxx'
    have := hloc u x x' hxx'
    by_cases hx : x ∈ E u
    · simp [Set.indicator_of_mem hx, Set.indicator_of_mem (this.mp hx)]
    · simp [Set.indicator_of_notMem hx, Set.indicator_of_notMem (fun h => hx (this.mpr h))]
  · intro x x' hxx'
    have := hloc v x x' hxx'
    by_cases hx : x ∈ E v
    · simp [Set.indicator_of_mem hx, Set.indicator_of_mem (this.mp hx)]
    · simp [Set.indicator_of_notMem hx, Set.indicator_of_notMem (fun h => hx (this.mpr h))]

/-! ## Deterministic grid comparison -/

/-- At most five vertices are adjacent to each vertex of `C`. -/
theorem card_adj_le5 (hG : MaxDegreeAtMost 5 G) (C : Finset (Fin n)) :
    (Finset.univ.filter fun v => ∃ z ∈ C, G.Adj v z).card ≤ 5 * C.card := by
  have hsub : (Finset.univ.filter fun v => ∃ z ∈ C, G.Adj v z) ⊆
      C.biUnion fun z => G.neighborFinset z := by
    intro v hv
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hv
    obtain ⟨z, hz, hvz⟩ := hv
    exact Finset.mem_biUnion.mpr ⟨z, hz, (G.mem_neighborFinset z v).mpr hvz.symm⟩
  refine (Finset.card_le_card hsub).trans ((Finset.card_biUnion_le).trans ?_)
  calc ∑ z ∈ C, (G.neighborFinset z).card ≤ ∑ _z ∈ C, 5 :=
        Finset.sum_le_sum fun z _ => card_neighborFinset_le5 G hG z
    _ = 5 * C.card := by rw [Finset.sum_const, smul_eq_mul, mul_comm]

theorem outer_grid5 (hG : MaxDegreeAtMost 5 G) (y : Fin n → ℝ) {a t b : ℝ} (hat : a < t)
    (htb : t ≤ b) :
    (C3.outerFrontier G y t).card ≤
      (C3.outerFrontier G y a).card + 5 * (C3.cellSet y a b).card := by
  have hsub : C3.outerFrontier G y t ⊆ C3.outerFrontier G y a ∪
      Finset.univ.filter fun v => ∃ z ∈ C3.cellSet y a b, G.Adj v z := by
    intro v hv
    rw [C3.mem_outerFrontier] at hv
    obtain ⟨hvt, u, hu, hut⟩ := hv
    by_cases hua : y u ≤ a
    · exact Finset.mem_union_left _
        ((C3.mem_outerFrontier G y a v).mpr ⟨by linarith, u, hu, hua⟩)
    · refine Finset.mem_union_right _ ?_
      simp only [Finset.mem_filter, Finset.mem_univ, true_and, C3.cellSet]
      exact ⟨u, ⟨not_le.mp hua, by linarith⟩, hu⟩
  exact (Finset.card_le_card hsub).trans ((Finset.card_union_le _ _).trans
    (Nat.add_le_add_left (card_adj_le5 G hG _) _))

/-- Below `-T`, a frontier vertex has a neighbor with label at most `-T`. -/
theorem outer_tail_low5 (hG : MaxDegreeAtMost 5 G) (y : Fin n → ℝ) {t T : ℝ} (ht : t ≤ -T) :
    (C3.outerFrontier G y t).card ≤ 5 * (Finset.univ.filter fun v => y v ≤ -T).card := by
  have hsub : C3.outerFrontier G y t ⊆
      Finset.univ.filter fun v => ∃ z ∈ (Finset.univ.filter fun v => y v ≤ -T), G.Adj v z := by
    intro v hv
    rw [C3.mem_outerFrontier] at hv
    obtain ⟨-, u, hu, hut⟩ := hv
    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
    exact ⟨u, by linarith, hu⟩
  exact (Finset.card_le_card hsub).trans (card_adj_le5 G hG _)

/-! ## Total deviation -/

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

theorem devTotal_integral_le5 (hs : GLC.Sch G K vec) (hG : MaxDegreeAtMost 5 G) (M q : ℕ)
    (T : ℝ) :
    ∫ x, GLC.devTotal G vec M q T x ∂stdGaussian (GaussianField.Sample n) ≤
      (4 * M + 2 : ℝ) * Real.sqrt (n * depBound5 (K + 1)) := by
  set s := Real.sqrt (n * depBound5 (K + 1))
  have hb : ∀ {E : Fin n → Set (GaussianField.Sample n)}, (∀ v, MeasurableSet (E v)) →
      C3.IsLocal G (K + 1) E →
      ∫ x, |C3.centeredCount E x| ∂stdGaussian (GaussianField.Sample n) ≤ s :=
    fun hE hl => integral_abs_centeredCount_le5 G hG (K + 1) hE hl
  have hi1 := fun i : ℕ => L4.integrable_abs_cc (GLC.mset_outerEv G vec (GLC.cellLo M q i))
  have hi2 := fun i : ℕ => L4.integrable_abs_cc
    (GLC.mset_cellEv vec (GLC.cellLo M q i) (GLC.cellHi M q i))
  have hl1 := L4.integrable_abs_cc (GLC.mset_lowTailEv vec T)
  have hl2 := L4.integrable_abs_cc (GLC.mset_highTailEv vec T)
  unfold GLC.devTotal
  rw [integral_add, integral_add, integral_add,
    integral_finsetSum _ (fun i _ => hi1 i), integral_finsetSum _ (fun i _ => hi2 i)]
  · have e1 : ∑ i ∈ Finset.range (2 * M), ∫ x,
        |C3.centeredCount (GLC.outerEv G vec (GLC.cellLo M q i)) x|
        ∂stdGaussian (GaussianField.Sample n) ≤ (2 * M) * s := by
      refine (Finset.sum_le_sum fun i _ =>
        hb (GLC.mset_outerEv G vec _) (GLC.local_outerEv hs _)).trans ?_
      simp
    have e2 : ∑ i ∈ Finset.range (2 * M), ∫ x,
        |C3.centeredCount (GLC.cellEv vec (GLC.cellLo M q i) (GLC.cellHi M q i)) x|
        ∂stdGaussian (GaussianField.Sample n) ≤ (2 * M) * s := by
      refine (Finset.sum_le_sum fun i _ =>
        hb (GLC.mset_cellEv vec _ _) (GLC.local_cellEv hs _ _)).trans ?_
      simp
    have e3 := hb (GLC.mset_lowTailEv vec T) (GLC.local_lowTailEv hs T)
    have e4 := hb (GLC.mset_highTailEv vec T) (GLC.local_highTailEv hs T)
    push_cast at e1 e2
    nlinarith
  all_goals (repeat' apply Integrable.add) <;> first
    | exact integrable_finsetSum _ (fun i _ => hi1 i)
    | exact integrable_finsetSum _ (fun i _ => hi2 i)
    | assumption

end GLC5
end T3
end CubicPathwidth