CubicPathwidth.CutSweep.SweepMean

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

import CubicPathwidth.CutSweep.SweepGrid
import CubicPathwidth.C3.Families

/-!
# Expectations of the sweep counts (`sec:warmup`, eq. Equation (3.1) (`eq:warmup-mean`))

With the standardized labels `Y_v = label G R x v` under the standard Gaussian,
the pair count of `S` is `∑_v termFn S v`, where
`termFn S v x = ∑_{u ∈ N(v)} 1[(Y_v, Y_u) ∈ S] ∈ [0, 3]`.

* `sum_integral_termFn_cross_le`: `E e_t ≤ β_R n` (from `CrossingClaim`, the
  correlation floor `r_R` and monotonicity of `arccos`);
* `sum_integral_termFn_cell_le`: `E pairCount (cellSet a b) ≤ 3 n (b - a)/2`;
* `sum_integral_termFn_low_le`, `sum_integral_termFn_high_le`: `≤ 3 n / T²`.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace CutSweep

open C3.Labels

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

local notation "μ" => stdGaussian (GaussianField.Sample n)

/-- The contribution of `v` to the pair count of `S`. -/
def termFn (S : Set (ℝ × ℝ)) (v : Fin n) (x : GaussianField.Sample n) : ℝ :=
  ∑ u ∈ G.neighborFinset v, S.indicator (fun _ => (1 : ℝ)) (label G R x v, label G R x u)

theorem pairCount_label_eq (S : Set (ℝ × ℝ)) (x : GaussianField.Sample n) :
    (pairCount G (label G R x) S : ℝ) = ∑ v, termFn G R S v x := by
  unfold pairCount termFn
  push_cast
  refine Finset.sum_congr rfl fun v _ => ?_
  rw [Finset.card_filter]
  push_cast
  refine Finset.sum_congr rfl fun u _ => ?_
  by_cases h : (label G R x v, label G R x u) ∈ S <;> simp [h]

theorem termFn_nonneg (S : Set (ℝ × ℝ)) (v : Fin n) (x : GaussianField.Sample n) :
    0 ≤ termFn G R S v x :=
  Finset.sum_nonneg fun _ _ => Set.indicator_nonneg (fun _ _ => zero_le_one) _

theorem card_neighborFinset_le (hG : IsSubcubic G) (v : Fin n) :
    (G.neighborFinset v).card ≤ 3 := by
  rw [G.card_neighborFinset_eq_degree]
  convert hG v

theorem termFn_le_three (hG : IsSubcubic G) (S : Set (ℝ × ℝ)) (v : Fin n)
    (x : GaussianField.Sample n) : termFn G R S v x ≤ 3 := by
  unfold termFn
  calc _ ≤ ∑ _u ∈ G.neighborFinset v, (1 : ℝ) :=
        Finset.sum_le_sum fun _ _ => Set.indicator_le_self' (fun _ _ => zero_le_one) _
    _ = (G.neighborFinset v).card := by simp
    _ ≤ 3 := by exact_mod_cast card_neighborFinset_le G hG v

theorem measurableSet_pair {S : Set (ℝ × ℝ)} (hS : MeasurableSet S) (v u : Fin n) :
    MeasurableSet {x : GaussianField.Sample n | (label G R x v, label G R x u) ∈ S} :=
  ((measurable_label G R v).prodMk (measurable_label G R u)) hS

theorem termFn_eq_indicator (S : Set (ℝ × ℝ)) (v : Fin n) :
    termFn G R S v = fun x => ∑ u ∈ G.neighborFinset v,
      {x : GaussianField.Sample n | (label G R x v, label G R x u) ∈ S}.indicator
        (fun _ => (1 : ℝ)) x := by
  funext x
  unfold termFn
  refine Finset.sum_congr rfl fun u _ => ?_
  by_cases h : (label G R x v, label G R x u) ∈ S <;> simp [h]

theorem measurable_termFn {S : Set (ℝ × ℝ)} (hS : MeasurableSet S) (v : Fin n) :
    Measurable (termFn G R S v) := by
  rw [termFn_eq_indicator]
  exact Finset.measurable_sum _ fun u _ =>
    measurable_const.indicator (measurableSet_pair G R hS v u)

/-- `termFn S v` depends only on the coordinates in `ball v (R + 1)`. -/
theorem termFn_local (S : Set (ℝ × ℝ)) {v : Fin n} {x x' : GaussianField.Sample n}
    (h : ∀ w ∈ Locality.ball G v (R + 1), x w = x' w) :
    termFn G R S v x = termFn G R S v x' := by
  obtain ⟨h1, h2⟩ := label_local G R h
  unfold termFn
  refine Finset.sum_congr rfl fun u hu => ?_
  rw [h1, h2 u ((G.mem_neighborFinset v u).mp hu)]

theorem integral_termFn {S : Set (ℝ × ℝ)} (hS : MeasurableSet S) (v : Fin n) :
    ∫ x, termFn G R S v x ∂μ = ∑ u ∈ G.neighborFinset v,
      (μ).real {x : GaussianField.Sample n | (label G R x v, label G R x u) ∈ S} := by
  rw [termFn_eq_indicator, integral_finsetSum]
  · refine Finset.sum_congr rfl fun u _ => ?_
    rw [integral_indicator_const _ (measurableSet_pair G R hS v u), smul_eq_mul, mul_one]
  · intro u _
    exact (integrable_const _).indicator (measurableSet_pair G R hS v u)

/-- If every neighbor probability is at most `p`, the mean count is at most `3 n p`. -/
theorem sum_integral_termFn_le (hG : IsSubcubic G) {S : Set (ℝ × ℝ)} (hS : MeasurableSet S)
    {p : ℝ} (hp : 0 ≤ p)
    (h : ∀ v u, G.Adj v u →
      (μ).real {x : GaussianField.Sample n | (label G R x v, label G R x u) ∈ S} ≤ p) :
    ∑ v, ∫ x, termFn G R S v x ∂μ ≤ 3 * p * n := by
  calc ∑ v, ∫ x, termFn G R S v x ∂μ ≤ ∑ _v : Fin n, 3 * p := by
        refine Finset.sum_le_sum fun v _ => ?_
        rw [integral_termFn G R hS]
        calc _ ≤ ∑ _u ∈ G.neighborFinset v, p :=
              Finset.sum_le_sum fun u hu => h v u ((G.mem_neighborFinset v u).mp hu)
          _ = (G.neighborFinset v).card * p := by simp
          _ ≤ 3 * p := by
              have := card_neighborFinset_le G hG v
              have h3 : ((G.neighborFinset v).card : ℝ) ≤ 3 := by exact_mod_cast this
              nlinarith
    _ = 3 * p * n := by simp [mul_comm]

/-! ## Vertex-type counts -/

theorem prob_label_mem (v : Fin n) {s : Set ℝ} (hs : MeasurableSet s) :
    (μ).real {x : GaussianField.Sample n | label G R x v ∈ s} = (gaussianReal 0 1).real s :=
  C3.real_unit_projection (norm_unitVec G R v) hs

theorem sum_integral_termFn_cell_le (hG : IsSubcubic G) {a b : ℝ} (hab : a ≤ b) :
    ∑ v, ∫ x, termFn G R (cellSet a b) v x ∂μ ≤ 3 * ((b - a) / 2) * n := by
  refine sum_integral_termFn_le G R hG (measurableSet_cellSet a b) (by linarith) ?_
  intro v u _
  have hset : {x : GaussianField.Sample n | (label G R x v, label G R x u) ∈ cellSet a b} =
      {x | label G R x v ∈ Set.Ioc a b} := by
    ext x; simp [cellSet]
  rw [hset, prob_label_mem G R v measurableSet_Ioc]
  exact C3.gaussianReal_Ioc_le hab

theorem sum_integral_termFn_low_le (hG : IsSubcubic G) {T : ℝ} (hT : 0 < T) :
    ∑ v, ∫ x, termFn G R (lowSet T) v x ∂μ ≤ 3 * (1 / T ^ 2) * n := by
  refine sum_integral_termFn_le G R hG (measurableSet_lowSet T) (by positivity) ?_
  intro v u _
  have hset : {x : GaussianField.Sample n | (label G R x v, label G R x u) ∈ lowSet T} =
      {x | label G R x v ∈ Set.Iic (-T)} := by
    ext x; simp [lowSet]
  rw [hset, prob_label_mem G R v measurableSet_Iic]
  exact C3.gaussianReal_Iic_neg_le hT

theorem sum_integral_termFn_high_le (hG : IsSubcubic G) {T : ℝ} (hT : 0 < T) :
    ∑ v, ∫ x, termFn G R (highSet T) v x ∂μ ≤ 3 * (1 / T ^ 2) * n := by
  refine sum_integral_termFn_le G R hG (measurableSet_highSet T) (by positivity) ?_
  intro v u _
  have hset : {x : GaussianField.Sample n | (label G R x v, label G R x u) ∈ highSet T} =
      {x | label G R x u ∈ Set.Ioi T} := by
    ext x; simp [highSet]
  rw [hset, prob_label_mem G R u measurableSet_Ioi]
  exact C3.gaussianReal_Ioi_le hT

/-! ## The threshold count (Equation (3.1), `eq:warmup-mean`) -/

/-- Summing a function over ordered adjacent pairs is symmetric. -/
theorem sum_neighbor_swap (F : Fin n → Fin n → ℝ) :
    ∑ v, ∑ u ∈ G.neighborFinset v, F v u = ∑ v, ∑ u ∈ G.neighborFinset v, F u v := by
  have h : ∀ (H : Fin n → Fin n → ℝ) (v : Fin n),
      ∑ u ∈ G.neighborFinset v, H v u = ∑ u, if G.Adj v u then H v u else 0 := by
    intro H v
    rw [← Finset.sum_filter]
    congr 1
    ext u
    simp
  rw [Finset.sum_congr rfl fun v _ => h F v,
    Finset.sum_congr rfl fun v _ => h (fun v u => F u v) v, Finset.sum_comm]
  refine Finset.sum_congr rfl fun v _ => Finset.sum_congr rfl fun u _ => ?_
  rw [G.adj_comm]

/-- One edge, both orientations: Lemma 3.3 (`lem:crossing`)(b) with the correlation floor. -/
theorem pair_cross_le (hcross : CrossingClaim) (hG : IsSubcubic G) (hR : 0 < R)
    {v u : Fin n} (huv : G.Adj v u) (t : ℝ) :
    (μ).real {x : GaussianField.Sample n | (label G R x v, label G R x u) ∈ crossSet t} +
      (μ).real {x : GaussianField.Sample n | (label G R x u, label G R x v) ∈ crossSet t} ≤
      Real.arccos (C3.radiusCorr R) / Real.pi := by
  have hm1 := measurableSet_pair G R (measurableSet_crossSet t) v u
  have hm2 := measurableSet_pair G R (measurableSet_crossSet t) u v
  have hdisj : Disjoint
      {x : GaussianField.Sample n | (label G R x v, label G R x u) ∈ crossSet t}
      {x : GaussianField.Sample n | (label G R x u, label G R x v) ∈ crossSet t} := by
    rw [Set.disjoint_left]
    rintro x ⟨h1, h2⟩ ⟨h3, h4⟩
    simp only [Set.mem_Iic, Set.mem_Ioi] at h1 h2 h3 h4
    linarith
  rw [← measureReal_union hdisj hm2]
  have hset : {x : GaussianField.Sample n | (label G R x v, label G R x u) ∈ crossSet t} ∪
      {x : GaussianField.Sample n | (label G R x u, label G R x v) ∈ crossSet t} =
      {x | min ⟪unitVec G R v, x⟫ ⟪unitVec G R u, x⟫ ≤ t ∧
        t < max ⟪unitVec G R v, x⟫ ⟪unitVec G R u, x⟫} := by
    ext x
    simp only [crossSet, Set.mem_union, Set.mem_ofPred_eq, Set.mem_prod, Set.mem_Iic,
      Set.mem_Ioi, label, min_le_iff, lt_max_iff]
    constructor
    · rintro (⟨h1, h2⟩ | ⟨h1, h2⟩)
      · exact ⟨Or.inl h1, Or.inr h2⟩
      · exact ⟨Or.inr h1, Or.inl h2⟩
    · rintro ⟨h1 | h1, h2 | h2⟩
      · exact absurd (h1.trans_lt h2) (lt_irrefl _)
      · exact Or.inl ⟨h1, h2⟩
      · exact Or.inr ⟨h1, h2⟩
      · exact absurd (h1.trans_lt h2) (lt_irrefl _)
  rw [hset]
  refine (hcross n _ _ (norm_unitVec G R v) (norm_unitVec G R u) t).trans ?_
  exact div_le_div_of_nonneg_right
    (Real.arccos_le_arccos (radiusCorr_le_inner G R hG hR huv)) Real.pi_pos.le

theorem radiusCoefficient_eq (R : ℕ) :
    radiusCoefficient R = (3 / (2 * Real.pi)) * Real.arccos (C3.radiusCorr R) := rfl

/-- `E e_t ≤ β_R n`. -/
theorem sum_integral_termFn_cross_le (hcross : CrossingClaim) (hG : IsSubcubic G) (hR : 0 < R)
    (t : ℝ) :
    ∑ v, ∫ x, termFn G R (crossSet t) v x ∂μ ≤ radiusCoefficient R * n := by
  set P : Fin n → Fin n → ℝ := fun v u =>
    (μ).real {x : GaussianField.Sample n | (label G R x v, label G R x u) ∈ crossSet t}
  set c := Real.arccos (C3.radiusCorr R) / Real.pi
  have hc0 : 0 ≤ c := div_nonneg (Real.arccos_nonneg _) Real.pi_pos.le
  have hS : ∑ v, ∫ x, termFn G R (crossSet t) v x ∂μ =
      ∑ v, ∑ u ∈ G.neighborFinset v, P v u := by
    refine Finset.sum_congr rfl fun v _ => ?_
    rw [integral_termFn G R (measurableSet_crossSet t)]
  have hswap := sum_neighbor_swap G P
  have h2 : ∑ v, ∑ u ∈ G.neighborFinset v, (P v u + P u v) ≤ 3 * c * n := by
    calc _ ≤ ∑ v, ∑ _u ∈ G.neighborFinset v, c := by
          refine Finset.sum_le_sum fun v _ => Finset.sum_le_sum fun u hu => ?_
          exact pair_cross_le G R hcross hG hR ((G.mem_neighborFinset v u).mp hu) t
      _ ≤ ∑ _v : Fin n, 3 * c := by
          refine Finset.sum_le_sum fun v _ => ?_
          rw [Finset.sum_const, nsmul_eq_mul]
          have h3 : ((G.neighborFinset v).card : ℝ) ≤ 3 := by
            exact_mod_cast card_neighborFinset_le G hG v
          nlinarith
      _ = 3 * c * n := by simp [mul_comm]
  simp only [Finset.sum_add_distrib] at h2
  rw [hS, radiusCoefficient_eq]
  have hpi := Real.pi_pos
  have : (3 / (2 * Real.pi)) * Real.arccos (C3.radiusCorr R) = 3 / 2 * c := by
    simp only [c]; field_simp
  rw [this]
  linarith

end CutSweep
end CubicPathwidth