CubicPathwidth.CutSweep.SweepConc

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

import CubicPathwidth.CutSweep.SweepMean

/-!
# Concentration of local sums (`lem:warmup-variance`, then Chebyshev)

For `Q = ∑_v I_v` with `I_v ∈ [0, 3]` measurable and depending only on the
coordinates in `ball v r`, the centered terms `σ_v = (I_v - E I_v)/3` satisfy
`|σ_v| ≤ 1` and are uncorrelated when the balls are disjoint, so
`E(∑ σ_v)² ≤ n · dependenceBound r` (`secondMoment_sum_le_graph`). Markov's
inequality on the square gives
`P(|Q - E Q| ≥ s) ≤ 9 n · dependenceBound r / s²`.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace CutSweep

variable {n : ℕ}

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

/-- Chebyshev for a sum of `[0,3]`-valued terms that are local at radius `r`. -/
theorem prob_dev_ge_le (G : SimpleGraph (Fin n)) (hG : IsSubcubic G) (r : ℕ)
    (f : Fin n → GaussianField.Sample n → ℝ) (hf : ∀ v, Measurable (f v))
    (h0 : ∀ v x, 0 ≤ f v x) (h3 : ∀ v x, f v x ≤ 3)
    (hloc : ∀ v (x x' : GaussianField.Sample n),
      (∀ w ∈ Locality.ball G v r, x w = x' w) → f v x = f v x')
    {s : ℝ} (hs : 0 < s) :
    (μ).real {x | s ≤ |∑ v, f v x - ∑ v, ∫ y, f v y ∂μ|} ≤
      9 * ((n : ℝ) * dependenceBound r) / s ^ 2 := by
  set m : Fin n → ℝ := fun v => ∫ y, f v y ∂μ with hm
  have hint : ∀ v, Integrable (f v) μ := fun v =>
    Integrable.of_bound (hf v).aestronglyMeasurable 3 (ae_of_all _ fun x => by
      rw [Real.norm_eq_abs, abs_of_nonneg (h0 v x)]; exact h3 v x)
  have hm0 : ∀ v, 0 ≤ m v := fun v => integral_nonneg (h0 v)
  have hm3 : ∀ v, m v ≤ 3 := fun v => by
    calc m v ≤ ∫ _y, (3 : ℝ) ∂μ := integral_mono (hint v) (integrable_const _) (h3 v)
      _ = 3 := by simp
  set σ : Fin n → GaussianField.Sample n → ℝ := fun v x => (f v x - m v) / 3 with hσ
  have hσm : ∀ v, Measurable (σ v) := fun v => ((hf v).sub measurable_const).div_const _
  have hσb : ∀ v x, |σ v x| ≤ 1 := by
    intro v x
    simp only [hσ]
    rw [abs_div, abs_of_pos (by norm_num : (0 : ℝ) < 3), div_le_one (by norm_num), abs_le]
    have := h0 v x; have := h3 v x; have := hm0 v; have := hm3 v
    constructor <;> linarith
  have hσloc : ∀ v (x x' : GaussianField.Sample n),
      (∀ w ∈ Locality.ball G v r, x w = x' w) → σ v x = σ v x' := by
    intro v x x' h
    simp only [hσ, hloc v x x' h]
  have hσ0 : ∀ v, ∫ x, σ v x ∂μ = 0 := by
    intro v
    simp only [hσ]
    rw [integral_div, integral_sub (hint v) (integrable_const _), integral_const, probReal_univ,
      one_smul, sub_self, zero_div]
  have hsec : ∫ x, (∑ v, σ v x) ^ 2 ∂μ ≤ (n : ℝ) * dependenceBound r := by
    apply secondMoment_sum_le_graph G hG r σ hσm hσb
    intro u v huv
    have hd := Locality.disjoint_balls_of_not_mem G huv
    rw [C3.integral_mul_of_disjoint hd (hσm u) (hσm v) (hσloc u) (hσloc v), hσ0 u, zero_mul]
  -- Markov on the square.
  set Z : GaussianField.Sample n → ℝ := fun x => (∑ v, σ v x) ^ 2
  have hZm : Measurable Z := (Finset.measurable_sum _ fun v _ => hσm v).pow_const 2
  have hZb : ∀ x, ‖Z x‖ ≤ (n : ℝ) ^ 2 := by
    intro x
    rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
    have : |∑ v, σ v x| ≤ n := by
      calc |∑ v, σ v x| ≤ ∑ v, |σ v x| := Finset.abs_sum_le_sum_abs _ _
        _ ≤ ∑ _v : Fin n, (1 : ℝ) := Finset.sum_le_sum fun v _ => hσb v x
        _ = n := by simp
    calc Z x = |∑ v, σ v x| ^ 2 := by simp [Z, sq_abs]
      _ ≤ (n : ℝ) ^ 2 := pow_le_pow_left₀ (abs_nonneg _) this 2
  have hZi : Integrable Z μ := Integrable.of_bound hZm.aestronglyMeasurable _ (ae_of_all _ hZb)
  have hmarkov := mul_meas_ge_le_integral_of_nonneg (ae_of_all _ fun x => sq_nonneg _) hZi
    ((s / 3) ^ 2)
  have hsub : {x | s ≤ |∑ v, f v x - ∑ v, m v|} ⊆ {x | (s / 3) ^ 2 ≤ Z x} := by
    intro x hx
    simp only [Set.mem_ofPred_eq] at hx ⊢
    have heq : ∑ v, f v x - ∑ v, m v = 3 * ∑ v, σ v x := by
      simp only [hσ, ← Finset.sum_sub_distrib, Finset.mul_sum]
      refine Finset.sum_congr rfl fun v _ => ?_
      ring
    rw [heq, abs_mul, abs_of_pos (by norm_num : (0 : ℝ) < 3)] at hx
    have h1 : s / 3 ≤ |∑ v, σ v x| := by linarith
    calc (s / 3) ^ 2 ≤ |∑ v, σ v x| ^ 2 := pow_le_pow_left₀ (by positivity) h1 2
      _ = Z x := by simp [Z, sq_abs]
  have hpos : 0 < (s / 3) ^ 2 := by positivity
  calc (μ).real {x | s ≤ |∑ v, f v x - ∑ v, m v|}
      ≤ (μ).real {x | (s / 3) ^ 2 ≤ Z x} := measureReal_mono hsub
    _ ≤ (∫ x, Z x ∂μ) / (s / 3) ^ 2 := by
        rw [le_div_iff₀ hpos]; linarith
    _ ≤ ((n : ℝ) * dependenceBound r) / (s / 3) ^ 2 :=
        div_le_div_of_nonneg_right hsec hpos.le
    _ = 9 * ((n : ℝ) * dependenceBound r) / s ^ 2 := by
        field_simp
        ring

/-- The pair counts of measurable sets concentrate. -/
theorem prob_pairCount_dev_le (G : SimpleGraph (Fin n)) (hG : IsSubcubic G) (R : ℕ)
    {S : Set (ℝ × ℝ)} (hS : MeasurableSet S) {s : ℝ} (hs : 0 < s) :
    (μ).real {x | s ≤ |(pairCount G (C3.Labels.label G R x) S : ℝ) -
        ∑ v, ∫ y, termFn G R S v y ∂μ|} ≤
      9 * ((n : ℝ) * dependenceBound (R + 1)) / s ^ 2 := by
  simp only [pairCount_label_eq]
  exact prob_dev_ge_le G hG (R + 1) (termFn G R S) (measurable_termFn G R hS)
    (termFn_nonneg G R S) (termFn_le_three G R hG S) (fun v x x' h => termFn_local G R S h) hs

end CutSweep
end CubicPathwidth
Back to top