CubicPathwidth.T2.GoodLabelsCountA

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

import CubicPathwidth.T2.DefsB
import CubicPathwidth.T2.GoodLabels4

/-!
# Labels from an abstract scheme: events, locality and concentration

For unit vectors `vec v` that are local at radius `K` (`vec v w = 0` outside
`ball v K`) and pairwise distinct, the labels `lab vec x v = ⟪vec v, x⟫` are
almost surely injective, events about `v` and its neighbors are local at
radius `K + 1`, and the total deviation of the grid counts is small on average
(`devTotal_integral_le`).
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace T2
namespace GLC

variable {n : ℕ}

/-- The label of `v` at the sample `x`. -/
def lab (vec : Fin n → GaussianField.Sample n) (x : GaussianField.Sample n) (v : Fin n) : ℝ :=
  ⟪vec v, x⟫

/-- Locality radius `K`, unit norm and distinctness of the vectors. -/
structure Sch (G : SimpleGraph (Fin n)) (K : ℕ) (vec : Fin n → GaussianField.Sample n) :
    Prop where
  norm : ∀ v, ‖vec v‖ = 1
  loc : ∀ v w, w ∉ Locality.ball G v K → vec v w = 0
  inj : ∀ u v, u ≠ v → vec u ≠ vec v

section Basic

variable (vec : Fin n → GaussianField.Sample n)

@[fun_prop]

theorem measurable_lab (v : Fin n) : Measurable fun x => lab vec x v := by
  unfold lab
  fun_prop

theorem lab_eq (x : GaussianField.Sample n) (v : Fin n) :
    lab vec x v = ∑ w, vec v w * x w := by
  simp [lab, PiLp.inner_apply, mul_comm]

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

theorem lab_congr (hs : Sch G K vec) {x x' : GaussianField.Sample n} {v : Fin n}
    (h : ∀ w ∈ Locality.ball G v K, x w = x' w) : lab vec x v = lab vec x' v := by
  rw [lab_eq, lab_eq]
  apply Finset.sum_congr rfl
  intro w _
  by_cases hw : w ∈ Locality.ball G v K
  · rw [h w hw]
  · simp [hs.loc v w hw]

theorem lab_normal (hs : Sch G K vec) (v : Fin n) {s : Set ℝ} (hs' : MeasurableSet s) :
    (stdGaussian (GaussianField.Sample n)).real {x | lab vec x v ∈ s} =
      (gaussianReal 0 1).real s :=
  C3.real_unit_projection (hs.norm v) hs'

theorem lab_injective_ae (hs : Sch G K vec) :
    stdGaussian (GaussianField.Sample n) {x | ¬ Function.Injective (lab vec x)} = 0 := by
  have hsub : {x : GaussianField.Sample n | ¬ Function.Injective (lab vec x)} ⊆
      ⋃ p : Fin n × Fin n, ⋃ (_ : p.1 ≠ p.2), {x | ⟪vec p.1 - vec p.2, x⟫ = 0} := by
    intro x hx
    simp only [Function.Injective, not_forall] at hx
    obtain ⟨u, v, he, hne⟩ := hx
    simp only [Set.mem_iUnion, Set.mem_ofPred_eq]
    refine ⟨(u, v), hne, ?_⟩
    rw [inner_sub_left]
    simp only [lab] at he
    linarith
  apply measure_mono_null hsub
  apply measure_iUnion_null
  intro p
  apply measure_iUnion_null
  intro hp
  exact C3.measure_inner_eq_zero (sub_ne_zero.mpr (hs.inj _ _ hp))

end Basic

/-! ## Events -/

variable (G : SimpleGraph (Fin n)) (vec : Fin n → GaussianField.Sample n)

def outerEv (τ : ℝ) (v : Fin n) : Set (GaussianField.Sample n) :=
  {x | v ∈ C3.outerFrontier G (lab vec x) τ}

def cellEv (a b : ℝ) (v : Fin n) : Set (GaussianField.Sample n) :=
  {x | a < lab vec x v ∧ lab vec x v ≤ b}

def lowTailEv (T : ℝ) (v : Fin n) : Set (GaussianField.Sample n) :=
  {x | lab vec x v ≤ -T}

def highTailEv (T : ℝ) (v : Fin n) : Set (GaussianField.Sample n) :=
  {x | T < lab vec x v}

theorem mset_exists_adj (v : Fin n) {p : ℝ → Prop} (hp : MeasurableSet {s : ℝ | p s}) :
    MeasurableSet {x : GaussianField.Sample n | ∃ w, G.Adj v w ∧ p (lab vec x w)} := by
  rw [Set.ofPred_exists]
  refine MeasurableSet.iUnion fun w => ?_
  by_cases h : G.Adj v w
  · simp only [h, true_and]
    exact (measurable_lab vec w) hp
  · simp [h]

theorem mset_outerEv (τ : ℝ) (v : Fin n) : MeasurableSet (outerEv G vec τ v) := by
  simp only [outerEv, C3.mem_outerFrontier]
  rw [Set.ofPred_and]
  exact ((measurable_lab vec v) measurableSet_Ioi).inter
    (mset_exists_adj G vec v measurableSet_Iic)

theorem mset_cellEv (a b : ℝ) (v : Fin n) : MeasurableSet (cellEv vec a b v) :=
  (measurable_lab vec v) measurableSet_Ioc

theorem mset_lowTailEv (T : ℝ) (v : Fin n) : MeasurableSet (lowTailEv vec T v) :=
  (measurable_lab vec v) measurableSet_Iic

theorem mset_highTailEv (T : ℝ) (v : Fin n) : MeasurableSet (highTailEv vec T v) :=
  (measurable_lab vec v) measurableSet_Ioi

/-! ## Locality at radius `K + 1` -/

variable {G vec} {K : ℕ}

theorem lab_local (hs : Sch G K vec) {x x' : GaussianField.Sample n} {v : Fin n}
    (h : ∀ w ∈ Locality.ball G v (K + 1), x w = x' w) :
    lab vec x v = lab vec x' v ∧ ∀ z, G.Adj v z → lab vec x z = lab vec x' z := by
  refine ⟨lab_congr hs fun w hw => h w ?_, fun z hz => lab_congr hs fun w hw =>
    h w (L4.ball_subset_of_adj G K hz hw)⟩
  obtain ⟨hr, hd⟩ := (Locality.mem_ball G v w K).mp hw
  exact (Locality.mem_ball G v w (K + 1)).mpr ⟨hr, by omega⟩

theorem local_of_nbr (hs : Sch G K vec) {E : Fin n → Set (GaussianField.Sample n)}
    (hE : ∀ v (x x' : GaussianField.Sample n), lab vec x v = lab vec x' v →
      (∀ z, G.Adj v z → lab vec x z = lab vec x' z) → (x ∈ E v → x' ∈ E v)) :
    C3.IsLocal G (K + 1) E := by
  intro v x x' h
  obtain ⟨h1, h2⟩ := lab_local hs h
  have h' : ∀ w ∈ Locality.ball G v (K + 1), x' w = x w := fun w hw => (h w hw).symm
  obtain ⟨h1', h2'⟩ := lab_local hs h'
  exact ⟨hE v x x' h1 h2, hE v x' x h1' h2'⟩

theorem local_outerEv (hs : Sch G K vec) (τ : ℝ) : C3.IsLocal G (K + 1) (outerEv G vec τ) := by
  apply local_of_nbr hs
  intro v x x' h1 h2 hx
  simp only [outerEv, Set.mem_ofPred_eq, C3.mem_outerFrontier] at hx ⊢
  obtain ⟨hv, w, hw, hwt⟩ := hx
  exact ⟨h1 ▸ hv, w, hw, (h2 w hw) ▸ hwt⟩

theorem local_cellEv (hs : Sch G K vec) (a b : ℝ) : C3.IsLocal G (K + 1) (cellEv vec a b) := by
  apply local_of_nbr hs
  intro v x x' h1 _ hx
  simp only [cellEv, Set.mem_ofPred_eq] at hx ⊢
  rw [← h1]
  exact hx

theorem local_lowTailEv (hs : Sch G K vec) (T : ℝ) :
    C3.IsLocal G (K + 1) (lowTailEv vec T) := by
  apply local_of_nbr hs
  intro v x x' h1 _ hx
  simp only [lowTailEv, Set.mem_ofPred_eq] at hx ⊢
  rw [← h1]
  exact hx

theorem local_highTailEv (hs : Sch G K vec) (T : ℝ) :
    C3.IsLocal G (K + 1) (highTailEv vec T) := by
  apply local_of_nbr hs
  intro v x x' h1 _ hx
  simp only [highTailEv, Set.mem_ofPred_eq] at hx ⊢
  rw [← h1]
  exact hx

/-! ## Total deviation -/

/-- Cell endpoints for index `i < 2M`: `((i - M)/q, (i - M + 1)/q]`. -/
def cellLo (M q : ℕ) (i : ℕ) : ℝ := ((i : ℝ) - M) / q

def cellHi (M q : ℕ) (i : ℕ) : ℝ := ((i : ℝ) - M + 1) / q

variable (G vec)

/-- Total absolute deviation of all counts used. -/
def devTotal (M q : ℕ) (T : ℝ) (x : GaussianField.Sample n) : ℝ :=
  (∑ i ∈ Finset.range (2 * M), |C3.centeredCount (outerEv G vec (cellLo M q i)) x|) +
  (∑ i ∈ Finset.range (2 * M),
    |C3.centeredCount (cellEv vec (cellLo M q i) (cellHi M q i)) x|) +
  |C3.centeredCount (lowTailEv vec T) x| + |C3.centeredCount (highTailEv vec T) x|

theorem integrable_devTotal (M q : ℕ) (T : ℝ) :
    Integrable (devTotal G vec M q T) (stdGaussian (GaussianField.Sample n)) := by
  have hi1 := fun i : ℕ => L4.integrable_abs_cc (mset_outerEv G vec (cellLo M q i))
  have hi2 := fun i : ℕ => L4.integrable_abs_cc (mset_cellEv vec (cellLo M q i) (cellHi M q i))
  have hl1 := L4.integrable_abs_cc (mset_lowTailEv vec T)
  have hl2 := L4.integrable_abs_cc (mset_highTailEv vec T)
  unfold devTotal
  (repeat' apply Integrable.add) <;> first
    | exact integrable_finsetSum _ (fun i _ => hi1 i)
    | exact integrable_finsetSum _ (fun i _ => hi2 i)
    | assumption

theorem devTotal_integral_le (hs : Sch G K vec) (hG : MaxDegreeAtMost 4 G) (M q : ℕ) (T : ℝ) :
    ∫ x, devTotal G vec M q T x ∂stdGaussian (GaussianField.Sample n) ≤
      (4 * M + 2 : ℝ) * Real.sqrt (n * L4.depBound (K + 1)) := by
  set s := Real.sqrt (n * L4.depBound (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 => L4.integral_abs_centeredCount_le4 G hG (K + 1) hE hl
  have hi1 := fun i : ℕ => L4.integrable_abs_cc (mset_outerEv G vec (cellLo M q i))
  have hi2 := fun i : ℕ => L4.integrable_abs_cc (mset_cellEv vec (cellLo M q i) (cellHi M q i))
  have hl1 := L4.integrable_abs_cc (mset_lowTailEv vec T)
  have hl2 := L4.integrable_abs_cc (mset_highTailEv vec T)
  unfold 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 (outerEv G vec (cellLo M q i)) x|
        ∂stdGaussian (GaussianField.Sample n) ≤ (2 * M) * s := by
      refine (Finset.sum_le_sum fun i _ =>
        hb (mset_outerEv G vec _) (local_outerEv hs _)).trans ?_
      simp
    have e2 : ∑ i ∈ Finset.range (2 * M), ∫ x,
        |C3.centeredCount (cellEv vec (cellLo M q i) (cellHi M q i)) x|
        ∂stdGaussian (GaussianField.Sample n) ≤ (2 * M) * s := by
      refine (Finset.sum_le_sum fun i _ =>
        hb (mset_cellEv vec _ _) (local_cellEv hs _ _)).trans ?_
      simp
    have e3 := hb (mset_lowTailEv vec T) (local_lowTailEv hs T)
    have e4 := hb (mset_highTailEv vec T) (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

section Terms

variable {G vec} {M q : ℕ} {T : ℝ} (x : GaussianField.Sample n)

theorem dev_outer_le {i : ℕ} (hi : i < 2 * M) :
    |C3.centeredCount (outerEv G vec (cellLo M q i)) x| ≤ devTotal G vec M q T x := by
  have h := Finset.single_le_sum
    (f := fun i : ℕ => |C3.centeredCount (outerEv G vec (cellLo M q i)) x|)
    (fun _ _ => abs_nonneg _) (Finset.mem_range.mpr hi)
  have h2 : 0 ≤ ∑ i ∈ Finset.range (2 * M),
      |C3.centeredCount (cellEv vec (cellLo M q i) (cellHi M q i)) x| :=
    Finset.sum_nonneg fun _ _ => abs_nonneg _
  unfold devTotal
  have := abs_nonneg (C3.centeredCount (lowTailEv vec T) x)
  have := abs_nonneg (C3.centeredCount (highTailEv vec T) x)
  linarith

theorem dev_cell_le {i : ℕ} (hi : i < 2 * M) :
    |C3.centeredCount (cellEv vec (cellLo M q i) (cellHi M q i)) x| ≤
      devTotal G vec M q T x := by
  have h := Finset.single_le_sum
    (f := fun i : ℕ => |C3.centeredCount (cellEv vec (cellLo M q i) (cellHi M q i)) x|)
    (fun _ _ => abs_nonneg _) (Finset.mem_range.mpr hi)
  have h1 : 0 ≤ ∑ i ∈ Finset.range (2 * M),
      |C3.centeredCount (outerEv G vec (cellLo M q i)) x| :=
    Finset.sum_nonneg fun _ _ => abs_nonneg _
  unfold devTotal
  have := abs_nonneg (C3.centeredCount (lowTailEv vec T) x)
  have := abs_nonneg (C3.centeredCount (highTailEv vec T) x)
  linarith

theorem dev_tail_le :
    |C3.centeredCount (lowTailEv vec T) x| ≤ devTotal G vec M q T x ∧
    |C3.centeredCount (highTailEv vec T) x| ≤ devTotal G vec M q T x := by
  have h1 : 0 ≤ ∑ i ∈ Finset.range (2 * M),
      |C3.centeredCount (outerEv G vec (cellLo M q i)) x| :=
    Finset.sum_nonneg fun _ _ => abs_nonneg _
  have h2 : 0 ≤ ∑ i ∈ Finset.range (2 * M),
      |C3.centeredCount (cellEv vec (cellLo M q i) (cellHi M q i)) x| :=
    Finset.sum_nonneg fun _ _ => abs_nonneg _
  have a1 := abs_nonneg (C3.centeredCount (lowTailEv vec T) x)
  have a2 := abs_nonneg (C3.centeredCount (highTailEv vec T) x)
  unfold devTotal
  constructor <;> linarith

end Terms

/-! ## Counts versus expectations -/

theorem outerFrontier_eq (x : GaussianField.Sample n) (τ : ℝ) :
    C3.outerFrontier G (lab vec x) τ = Finset.univ.filter fun v => x ∈ outerEv G vec τ v := by
  ext v
  rw [Finset.mem_filter]
  exact ⟨fun h => ⟨Finset.mem_univ v, h⟩, fun h => h.2⟩

theorem cellSet_eq (x : GaussianField.Sample n) (a b : ℝ) :
    C3.cellSet (lab vec x) a b = Finset.univ.filter fun v => x ∈ cellEv vec a b v := by
  ext v
  rw [Finset.mem_filter]
  simp only [C3.cellSet, Finset.mem_filter, Finset.mem_univ, true_and]
  exact ⟨fun h => h, fun h => h⟩

theorem sum_cell_le (hs : Sch G K vec) {a b : ℝ} (hab : a ≤ b) :
    ∑ v, (stdGaussian (GaussianField.Sample n)).real (cellEv vec a b v) ≤
      n * ((b - a) / 2) := by
  calc _ ≤ ∑ _v : Fin n, (b - a) / 2 := by
        apply Finset.sum_le_sum
        intro v _
        have : cellEv vec a b v = {x | lab vec x v ∈ Set.Ioc a b} := rfl
        rw [this, lab_normal hs v measurableSet_Ioc]
        exact C3.gaussianReal_Ioc_le hab
    _ = _ := by simp

theorem sum_lowTail_eq (hs : Sch G K vec) (T : ℝ) :
    ∑ v, (stdGaussian (GaussianField.Sample n)).real (lowTailEv vec T v) =
      n * Phi (-T) := by
  calc _ = ∑ _v : Fin n, Phi (-T) := by
        apply Finset.sum_congr rfl
        intro v _
        have : lowTailEv vec T v = {x | lab vec x v ∈ Set.Iic (-T)} := rfl
        rw [this, lab_normal hs v measurableSet_Iic]
        rfl
    _ = _ := by simp

theorem Phi_neg_eq_Ici (T : ℝ) : (gaussianReal 0 1).real (Set.Ici T) = Phi (-T) := by
  have h := gaussianReal_map_neg (μ := 0) (v := 1)
  rw [neg_zero] at h
  unfold Phi
  have hm : (gaussianReal 0 1).real (Set.Ici T) =
      ((gaussianReal 0 1).map (fun x : ℝ => -x)).real (Set.Ici T) := by rw [h]
  rw [hm, map_measureReal_apply (by fun_prop) measurableSet_Ici]
  congr 1
  ext x
  simp

theorem sum_highTail_le (hs : Sch G K vec) (T : ℝ) :
    ∑ v, (stdGaussian (GaussianField.Sample n)).real (highTailEv vec T v) ≤
      n * Phi (-T) := by
  calc _ ≤ ∑ _v : Fin n, Phi (-T) := 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, ← Phi_neg_eq_Ici]
        exact measureReal_mono Set.Ioi_subset_Ici_self
    _ = _ := by simp

end GLC
end T2
end CubicPathwidth