CubicPathwidth.T2.Concentration4

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

import CubicPathwidth.T2.Labels4
import CubicPathwidth.C3.Grid

/-!
# Concentration of local counts and the outer grid comparison for `Δ ≤ 4`

* `integral_abs_centeredCount_le4`: for events local at radius `r`, the centered
  count has `E|S| ≤ √(n · D)` with `D = 2 · 3^(2r)` (ball sizes for `Δ ≤ 4`).
* `outer_grid4`, `outer_tail_low4`: deterministic comparisons for outer
  frontiers; neighbors of a vertex number at most four.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace T2
namespace L4

variable {n : ℕ}

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

theorem depBound_pos (r : ℕ) : 0 < depBound r := by
  unfold depBound; positivity

/-- Concentration of a local count. -/
theorem integral_abs_centeredCount_le4 (G : SimpleGraph (Fin n)) (hG : MaxDegreeAtMost 4 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 * depBound 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))
    (depBound r)
  · intro v
    have h : ((Locality.ball G v (2 * r)).card : ℝ) + 1 ≤ 2 * (3 : ℝ) ^ (2 * r) := by
      exact_mod_cast ball_card_add_one_le G hG v (2 * r)
    dsimp [depBound]
    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 -/

variable (G : SimpleGraph (Fin n))

/-- At most four vertices are adjacent to each vertex of `C`. -/
theorem card_adj_le4 (hG : MaxDegreeAtMost 4 G) (C : Finset (Fin n)) :
    (Finset.univ.filter fun v => ∃ z ∈ C, G.Adj v z).card ≤ 4 * 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, 4 :=
        Finset.sum_le_sum fun z _ => card_neighborFinset_le G hG z
    _ = 4 * C.card := by rw [Finset.sum_const, smul_eq_mul, mul_comm]

theorem outer_grid4 (hG : MaxDegreeAtMost 4 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 + 4 * (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_le4 G hG _) _))

/-- Below `-T`, a frontier vertex has a neighbor with label at most `-T`. -/
theorem outer_tail_low4 (hG : MaxDegreeAtMost 4 G) (y : Fin n → ℝ) {t T : ℝ} (ht : t ≤ -T) :
    (C3.outerFrontier G y t).card ≤ 4 * (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_le4 G hG _)

end L4
end T2
end CubicPathwidth
Back to top