CubicPathwidth.Sw4.GoodLabelsA

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

import CubicPathwidth.Sw4.Defs
import CubicPathwidth.T2.GoodLabelsCount

/-!
# Good labels for the switched layout: events, locality and total deviation

Labels `lab vec x v = ⟪vec v, x⟫` come from an abstract scheme (`T2.GLC.Sch`). Besides
the outer-frontier, cell and tail events of `T2.GLC`, the switched layout needs inner
frontiers (`innerEv`) and the two parts of `D̂` on either side of zero (`crossPosEv`,
`crossNegEv`). All events are local at radius `K + 1`. `devTotal` collects the absolute
deviations of all counts used; its expectation is `O(√n)` (`devTotal_integral_le`).

Counterpart of `C3.Labels` (subcubic, geometric labels) for maximum degree 4.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace Sw4
namespace SwL

open T2 T2.GLC

variable {n : ℕ}

/-! ## Membership in `D̂` -/

theorem mem_hatD (G : SimpleGraph (Fin n)) (y : Fin n → ℝ) (v : Fin n) :
    v ∈ hatD G y ↔
      (y v ≤ 0 ∧ 3 ≤ ((G.neighborFinset v).filter fun z => 0 < y z).card) ∨
        (0 < y v ∧ 3 ≤ ((G.neighborFinset v).filter fun z => y z ≤ 0).card) := by
  unfold hatD
  rw [Finset.mem_filter]
  simp only [Finset.mem_univ, true_and]

/-! ## Events -/

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

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

def crossPosEv (v : Fin n) : Set (GaussianField.Sample n) :=
  {x | v ∈ hatD G (lab vec x) ∧ 0 < lab vec x v}

def crossNegEv (v : Fin n) : Set (GaussianField.Sample n) :=
  {x | v ∈ hatD G (lab vec x) ∧ lab vec x v ≤ 0}

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

theorem mset_card_ge (v : Fin n) {p : ℝ → Prop} (hp : MeasurableSet {s : ℝ | p s}) :
    MeasurableSet {x : GaussianField.Sample n |
      3 ≤ ((G.neighborFinset v).filter fun z => p (lab vec x z)).card} := by
  have hm : Measurable fun x : GaussianField.Sample n =>
      ∑ z ∈ G.neighborFinset v, (if p (lab vec x z) then (1 : ℕ) else 0) := by
    refine Finset.measurable_sum _ fun z _ => ?_
    exact Measurable.ite ((measurable_lab vec z) hp) measurable_const measurable_const
  have e : {x : GaussianField.Sample n |
      3 ≤ ((G.neighborFinset v).filter fun z => p (lab vec x z)).card} =
      (fun x : GaussianField.Sample n =>
        ∑ z ∈ G.neighborFinset v, (if p (lab vec x z) then (1 : ℕ) else 0)) ⁻¹'
          {k : ℕ | 3 ≤ k} := by
    ext x
    simp only [Set.mem_ofPred_eq, Set.mem_preimage, Finset.card_filter]
  rw [e]
  exact hm (MeasurableSet.of_discrete)

theorem mset_cross (v : Fin n) {p : ℝ → Prop} (hp : MeasurableSet {s : ℝ | p s}) :
    MeasurableSet {x : GaussianField.Sample n | v ∈ hatD G (lab vec x) ∧ p (lab vec x v)} := by
  simp only [mem_hatD]
  have e : {x : GaussianField.Sample n |
      ((lab vec x v ≤ 0 ∧ 3 ≤ ((G.neighborFinset v).filter fun z => 0 < lab vec x z).card) ∨
        (0 < lab vec x v ∧ 3 ≤ ((G.neighborFinset v).filter fun z => lab vec x z ≤ 0).card)) ∧
      p (lab vec x v)} =
      (({x | lab vec x v ≤ 0} ∩
          {x | 3 ≤ ((G.neighborFinset v).filter fun z => 0 < lab vec x z).card}) ∪
        ({x | 0 < lab vec x v} ∩
          {x | 3 ≤ ((G.neighborFinset v).filter fun z => lab vec x z ≤ 0).card})) ∩
        {x | p (lab vec x v)} := by
    ext x
    simp only [Set.mem_ofPred_eq, Set.mem_union, Set.mem_inter_iff]
  rw [e]
  exact ((((measurable_lab vec v) measurableSet_Iic).inter
      (mset_card_ge G vec v (p := fun s => 0 < s) measurableSet_Ioi)).union
    (((measurable_lab vec v) measurableSet_Ioi).inter
      (mset_card_ge G vec v (p := fun s => s ≤ 0) measurableSet_Iic))).inter
    ((measurable_lab vec v) hp)

theorem mset_crossPosEv (v : Fin n) : MeasurableSet (crossPosEv G vec v) :=
  mset_cross G vec v (p := fun s => 0 < s) measurableSet_Ioi

theorem mset_crossNegEv (v : Fin n) : MeasurableSet (crossNegEv G vec v) :=
  mset_cross G vec v (p := fun s => s ≤ 0) measurableSet_Iic

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

variable {G vec} {K : ℕ}

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

theorem filter_nbr_congr {x x' : GaussianField.Sample n} {v : Fin n}
    (h2 : ∀ z, G.Adj v z → lab vec x z = lab vec x' z) (p : ℝ → Prop) :
    ((G.neighborFinset v).filter fun z => p (lab vec x z)) =
      ((G.neighborFinset v).filter fun z => p (lab vec x' z)) := by
  apply Finset.filter_congr
  intro z hz
  rw [h2 z ((G.mem_neighborFinset v z).mp hz)]

theorem local_cross (hs : Sch G K vec) {p : ℝ → Prop} :
    C3.IsLocal G (K + 1) (fun v => {x : GaussianField.Sample n |
      v ∈ hatD G (lab vec x) ∧ p (lab vec x v)}) := by
  apply local_of_nbr hs
  intro v x x' h1 h2 hx
  simp only [Set.mem_ofPred_eq, mem_hatD] at hx ⊢
  rw [← h1, ← filter_nbr_congr h2 (fun s => 0 < s), ← filter_nbr_congr h2 (fun s => s ≤ 0)]
  exact hx

theorem local_crossPosEv (hs : Sch G K vec) : C3.IsLocal G (K + 1) (crossPosEv G vec) :=
  local_cross hs (p := fun s => 0 < s)

theorem local_crossNegEv (hs : Sch G K vec) : C3.IsLocal G (K + 1) (crossNegEv G vec) :=
  local_cross hs (p := fun s => s ≤ 0)

/-! ## Total deviation -/

variable (G vec)

/-- Total absolute deviation of all counts used: inner frontiers at `-i/q` and outer
frontiers at `i/q` for `i ≤ M`, the `2M` cells, the two tails and the two halves of
`D̂`. -/
def devTotal (M q : ℕ) (T : ℝ) (x : GaussianField.Sample n) : ℝ :=
  (∑ i ∈ Finset.range (M + 1), |C3.centeredCount (innerEv G vec (-(i : ℝ) / q)) x|) +
  (∑ i ∈ Finset.range (M + 1), |C3.centeredCount (outerEv G vec ((i : ℝ) / q)) 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| +
  |C3.centeredCount (crossPosEv G vec) x| + |C3.centeredCount (crossNegEv G vec) 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_innerEv G vec (-(i : ℝ) / q))
  have hi2 := fun i : ℕ => L4.integrable_abs_cc (mset_outerEv G vec ((i : ℝ) / q))
  have hi3 := 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)
  have hl3 := L4.integrable_abs_cc (mset_crossPosEv G vec)
  have hl4 := L4.integrable_abs_cc (mset_crossNegEv G vec)
  unfold devTotal
  (repeat' apply Integrable.add) <;> first
    | exact integrable_finsetSum _ (fun i _ => hi1 i)
    | exact integrable_finsetSum _ (fun i _ => hi2 i)
    | exact integrable_finsetSum _ (fun i _ => hi3 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 + 6 : ℝ) * 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_innerEv G vec (-(i : ℝ) / q))
  have hi2 := fun i : ℕ => L4.integrable_abs_cc (mset_outerEv G vec ((i : ℝ) / q))
  have hi3 := 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)
  have hl3 := L4.integrable_abs_cc (mset_crossPosEv G vec)
  have hl4 := L4.integrable_abs_cc (mset_crossNegEv G vec)
  unfold devTotal
  rw [integral_add, integral_add, integral_add, integral_add, integral_add, integral_add,
    integral_finsetSum _ (fun i _ => hi1 i), integral_finsetSum _ (fun i _ => hi2 i),
    integral_finsetSum _ (fun i _ => hi3 i)]
  · have e1 : ∑ i ∈ Finset.range (M + 1),
        ∫ x, |C3.centeredCount (innerEv G vec (-(i : ℝ) / q)) x|
          ∂stdGaussian (GaussianField.Sample n) ≤ (M + 1) * s := by
      refine (Finset.sum_le_sum fun i _ =>
        hb (mset_innerEv G vec _) (local_innerEv hs _)).trans ?_
      simp
    have e2 : ∑ i ∈ Finset.range (M + 1),
        ∫ x, |C3.centeredCount (outerEv G vec ((i : ℝ) / q)) x|
          ∂stdGaussian (GaussianField.Sample n) ≤ (M + 1) * s := by
      refine (Finset.sum_le_sum fun i _ =>
        hb (mset_outerEv G vec _) (local_outerEv hs _)).trans ?_
      simp
    have e3 : ∑ 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 e4 := hb (mset_lowTailEv vec T) (local_lowTailEv hs T)
    have e5 := hb (mset_highTailEv vec T) (local_highTailEv hs T)
    have e6 := hb (mset_crossPosEv G vec) (local_crossPosEv hs)
    have e7 := hb (mset_crossNegEv G vec) (local_crossNegEv hs)
    push_cast at e1 e2 e3
    nlinarith
  all_goals (repeat' apply Integrable.add) <;> first
    | exact integrable_finsetSum _ (fun i _ => hi1 i)
    | exact integrable_finsetSum _ (fun i _ => hi2 i)
    | exact integrable_finsetSum _ (fun i _ => hi3 i)
    | assumption

/-! ## Each deviation is at most the total -/

section Terms

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

theorem devTotal_parts :
    0 ≤ ∑ i ∈ Finset.range (M + 1), |C3.centeredCount (innerEv G vec (-(i : ℝ) / q)) x| ∧
    0 ≤ ∑ i ∈ Finset.range (M + 1), |C3.centeredCount (outerEv G vec ((i : ℝ) / q)) x| ∧
    0 ≤ ∑ i ∈ Finset.range (2 * M),
      |C3.centeredCount (cellEv vec (cellLo M q i) (cellHi M q i)) x| ∧
    0 ≤ |C3.centeredCount (lowTailEv vec T) x| ∧ 0 ≤ |C3.centeredCount (highTailEv vec T) x| ∧
    0 ≤ |C3.centeredCount (crossPosEv G vec) x| ∧ 0 ≤ |C3.centeredCount (crossNegEv G vec) x| :=
  ⟨Finset.sum_nonneg fun _ _ => abs_nonneg _, Finset.sum_nonneg fun _ _ => abs_nonneg _,
    Finset.sum_nonneg fun _ _ => abs_nonneg _, abs_nonneg _, abs_nonneg _, abs_nonneg _,
    abs_nonneg _⟩

theorem dev_inner_le {i : ℕ} (hi : i ≤ M) :
    |C3.centeredCount (innerEv G vec (-(i : ℝ) / q)) x| ≤ devTotal G vec M q T x := by
  have h := Finset.single_le_sum
    (f := fun i : ℕ => |C3.centeredCount (innerEv G vec (-(i : ℝ) / q)) x|)
    (fun _ _ => abs_nonneg _) (Finset.mem_range.mpr (Nat.lt_succ_of_le hi))
  obtain ⟨-, h2, h3, h4, h5, h6, h7⟩ := devTotal_parts (G := G) (vec := vec) (M := M) (q := q)
    (T := T) x
  unfold devTotal
  linarith

theorem dev_outer_le {i : ℕ} (hi : i ≤ M) :
    |C3.centeredCount (outerEv G vec ((i : ℝ) / q)) x| ≤ devTotal G vec M q T x := by
  have h := Finset.single_le_sum
    (f := fun i : ℕ => |C3.centeredCount (outerEv G vec ((i : ℝ) / q)) x|)
    (fun _ _ => abs_nonneg _) (Finset.mem_range.mpr (Nat.lt_succ_of_le hi))
  obtain ⟨h1, -, h3, h4, h5, h6, h7⟩ := devTotal_parts (G := G) (vec := vec) (M := M) (q := q)
    (T := T) x
  unfold devTotal
  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)
  obtain ⟨h1, h2, -, h4, h5, h6, h7⟩ := devTotal_parts (G := G) (vec := vec) (M := M) (q := q)
    (T := T) x
  unfold devTotal
  linarith

theorem dev_rest_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 ∧
    |C3.centeredCount (crossPosEv G vec) x| ≤ devTotal G vec M q T x ∧
    |C3.centeredCount (crossNegEv G vec) x| ≤ devTotal G vec M q T x := by
  obtain ⟨h1, h2, h3, h4, h5, h6, h7⟩ := devTotal_parts (G := G) (vec := vec) (M := M) (q := q)
    (T := T) x
  unfold devTotal
  refine ⟨?_, ?_, ?_, ?_⟩ <;> linarith

end Terms

/-! ## Counts as filters -/

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

theorem crossPos_eq (x : GaussianField.Sample n) :
    ((hatD G (lab vec x)).filter fun v => 0 < lab vec x v) =
      Finset.univ.filter fun v => x ∈ crossPosEv G vec v := by
  ext v
  rw [Finset.mem_filter, Finset.mem_filter]
  exact ⟨fun h => ⟨Finset.mem_univ v, h⟩, fun h => h.2⟩

theorem crossNeg_eq (x : GaussianField.Sample n) :
    ((hatD G (lab vec x)).filter fun v => lab vec x v ≤ 0) =
      Finset.univ.filter fun v => x ∈ crossNegEv G vec v := by
  ext v
  rw [Finset.mem_filter, Finset.mem_filter]
  exact ⟨fun h => ⟨Finset.mem_univ v, h⟩, fun h => h.2⟩

theorem hatL0_eq (x : GaussianField.Sample n) :
    hatL0 G (lab vec x) =
      (Finset.univ.filter fun v => x ∈ innerEv G vec 0 v).card +
        (Finset.univ.filter fun v => x ∈ crossPosEv G vec v).card := by
  rw [← innerFrontier_eq, ← crossPos_eq]
  unfold hatL0
  congr 1

theorem hatL0'_eq (x : GaussianField.Sample n) :
    hatL0' G (lab vec x) =
      (Finset.univ.filter fun v => x ∈ outerEv G vec 0 v).card +
        (Finset.univ.filter fun v => x ∈ crossNegEv G vec v).card := by
  rw [← outerFrontier_eq, ← crossNeg_eq]
  unfold hatL0'
  congr 1

/-! ## Deterministic grid comparison for inner frontiers, `Δ ≤ 4` -/

theorem inner_grid4 (hG : MaxDegreeAtMost 4 G) (y : Fin n → ℝ) {a t b : ℝ} (hat : a ≤ t)
    (htb : t < b) :
    (C3.innerFrontier G y t).card ≤
      (C3.innerFrontier G y b).card + 4 * (C3.cellSet y a b).card := by
  have hsub : C3.innerFrontier G y t ⊆ C3.innerFrontier G y b ∪
      Finset.univ.filter fun v => ∃ z ∈ C3.cellSet y a b, G.Adj v z := by
    intro v hv
    rw [C3.mem_innerFrontier] at hv
    obtain ⟨hvt, z, hz, hzt⟩ := hv
    by_cases hzb : b < y z
    · exact Finset.mem_union_left _
        ((C3.mem_innerFrontier G y b v).mpr ⟨by linarith, z, hz, hzb⟩)
    · refine Finset.mem_union_right _ ?_
      simp only [Finset.mem_filter, Finset.mem_univ, true_and, C3.cellSet]
      exact ⟨z, ⟨by linarith, not_lt.mp hzb⟩, hz⟩
  exact (Finset.card_le_card hsub).trans ((Finset.card_union_le _ _).trans
    (Nat.add_le_add_left (L4.card_adj_le4 G hG _) _))

end SwL
end Sw4
end CubicPathwidth