CubicPathwidth.CutSweep.Sweep

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

import CubicPathwidth.CutSweep.SweepConc

/-!
# `SweepClaim` from `CrossingClaim` (`sec:warmup`: grid, concentration, union bound)

Fix `R ≥ 1` and `ε > 0`. Put `δ = ε/4`, choose integers `K ≥ 3/ε` and
`T ≥ max(1, 6/ε)`, and use the grid `τ_j = -T + j/K`, `j < L = 2TK`. The
`2L + 2` counts (threshold counts at `τ_j`, cell counts, two tails) each
deviate from their means by at least `δ n` with probability at most
`9 D / (δ² n)`, `D = dependenceBound (R + 1)`. For `n` large the union of these
events and the null event of coinciding labels has probability below one; at a
sample outside it every threshold count is at most `(β_R + ε) n`.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Classical

namespace CubicPathwidth
namespace CutSweep

open C3.Labels

variable {n : ℕ}

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

/-- The deviation event of the pair count of `S` at level `s`. -/
def devEv (G : SimpleGraph (Fin n)) (R : ℕ) (S : Set (ℝ × ℝ)) (s : ℝ) :
    Set (GaussianField.Sample n) :=
  {x | s ≤ |(pairCount G (label G R x) S : ℝ) - ∑ v, ∫ y, termFn G R S v y ∂μ|}

theorem pairCount_le_of_not_devEv {G : SimpleGraph (Fin n)} {R : ℕ} {S : Set (ℝ × ℝ)} {s : ℝ}
    {x : GaussianField.Sample n} (hx : x ∉ devEv G R S s) :
    (pairCount G (label G R x) S : ℝ) ≤ ∑ v, ∫ y, termFn G R S v y ∂μ + s := by
  simp only [devEv, Set.mem_ofPred_eq, not_le] at hx
  linarith [le_abs_self ((pairCount G (label G R x) S : ℝ) - ∑ v, ∫ y, termFn G R S v y ∂μ)]

theorem sweepClaim_of_crossing (hcross : CrossingClaim) : SweepClaim := by
  intro R hR ε hε
  set δ : ℝ := ε / 4 with hδ
  have hδ0 : 0 < δ := by positivity
  set K : ℕ := ⌈3 / ε⌉₊ + 1 with hK
  set T : ℕ := ⌈6 / ε⌉₊ + 1 with hT
  have hK0 : 0 < K := Nat.succ_pos _
  have hKr : (0 : ℝ) < K := by exact_mod_cast hK0
  have hT1 : (1 : ℝ) ≤ T := by
    have : 1 ≤ T := Nat.succ_le_succ (Nat.zero_le _)
    exact_mod_cast this
  have hKε : 3 / ε ≤ K := by
    have := Nat.le_ceil (3 / ε)
    rw [hK]; push_cast; linarith
  have hTε : 6 / ε ≤ T := by
    have := Nat.le_ceil (6 / ε)
    rw [hT]; push_cast; linarith
  set L : ℕ := 2 * T * K with hL
  set D : ℝ := dependenceBound (R + 1) with hD
  set X : ℝ := (2 * L + 2) * (9 * D / δ ^ 2) with hX
  refine ⟨⌈X⌉₊ + 1, fun n hn G hG => ?_⟩
  have hn1 : (1 : ℝ) ≤ n := by
    have : 1 ≤ n := le_trans (Nat.succ_le_succ (Nat.zero_le _)) hn
    exact_mod_cast this
  have hnX : X < n := by
    have h1 := Nat.le_ceil X
    have h2 : ((⌈X⌉₊ + 1 : ℕ) : ℝ) ≤ n := by exact_mod_cast hn
    push_cast at h2
    linarith
  have hn0 : (0 : ℝ) < n := by linarith
  -- Grid and the bad events.
  set τ : ℕ → ℝ := fun j => -(T : ℝ) + j / K with hτ
  set τ' : ℕ → ℝ := fun j => -(T : ℝ) + ((j : ℝ) + 1) / K with hτ'
  set s : ℝ := δ * n with hs
  have hs0 : 0 < s := by positivity
  set B : Set (GaussianField.Sample n) :=
    (⋃ j ∈ Finset.range L, devEv G R (crossSet (τ j)) s) ∪
      (⋃ j ∈ Finset.range L, devEv G R (cellSet (τ j) (τ' j)) s) ∪
      devEv G R (lowSet T) s ∪ devEv G R (highSet T) s ∪
      {x | ¬ Function.Injective (label G R x)} with hB
  set b : ℝ := 9 * ((n : ℝ) * D) / s ^ 2 with hb
  have hdev : ∀ {S : Set (ℝ × ℝ)}, MeasurableSet S → (stdGaussian (GaussianField.Sample n)).real (devEv G R S s) ≤ b :=
    fun hS => prob_pairCount_dev_le G hG R hS hs0
  have hBle : (stdGaussian (GaussianField.Sample n)).real B ≤ (2 * L + 2) * b := by
    have hinj : (stdGaussian (GaussianField.Sample n)).real {x : GaussianField.Sample n | ¬ Function.Injective (label G R x)} = 0 := by
      simp [Measure.real, label_injective_ae G R]
    have h1 : (stdGaussian (GaussianField.Sample n)).real (⋃ j ∈ Finset.range L, devEv G R (crossSet (τ j)) s) ≤ L * b := by
      refine (measureReal_biUnion_finset_le _ _).trans ?_
      calc _ ≤ ∑ _j ∈ Finset.range L, b :=
            Finset.sum_le_sum fun j _ => hdev (measurableSet_crossSet _)
        _ = L * b := by simp
    have h2 : (stdGaussian (GaussianField.Sample n)).real (⋃ j ∈ Finset.range L, devEv G R (cellSet (τ j) (τ' j)) s) ≤ L * b := by
      refine (measureReal_biUnion_finset_le _ _).trans ?_
      calc _ ≤ ∑ _j ∈ Finset.range L, b :=
            Finset.sum_le_sum fun j _ => hdev (measurableSet_cellSet _ _)
        _ = L * b := by simp
    have h3 := hdev (measurableSet_lowSet (T : ℝ))
    have h4 := hdev (measurableSet_highSet (T : ℝ))
    refine (measureReal_union_le _ _).trans ?_
    rw [hinj, add_zero]
    refine (measureReal_union_le _ _).trans ?_
    refine (add_le_add_left (measureReal_union_le _ _) _).trans ?_
    refine (add_le_add_left (add_le_add_left (measureReal_union_le _ _) _) _).trans ?_
    linarith
  have hb' : (2 * L + 2) * b = X / n := by
    rw [hb, hX, hs]
    field_simp
  have hBlt : (stdGaussian (GaussianField.Sample n)).real B < 1 := by
    calc _ ≤ _ := hBle
      _ = X / n := hb'
      _ < 1 := by rw [div_lt_one hn0]; exact hnX
  have hne : B ≠ Set.univ := by
    intro h
    rw [h, probReal_univ] at hBlt
    exact lt_irrefl _ hBlt
  obtain ⟨x, hx⟩ := (Set.ne_univ_iff_exists_notMem B).mp hne
  simp only [hB, Set.mem_union, not_or, Set.mem_iUnion, not_exists, Set.mem_ofPred_eq,
    not_not] at hx
  obtain ⟨⟨⟨⟨hxc, hxcell⟩, hxlow⟩, hxhigh⟩, hxinj⟩ := hx
  refine ⟨label G R x, hxinj, fun t => ?_⟩
  -- The bounds.
  have hβ0 : 0 ≤ radiusCoefficient R := by
    rw [radiusCoefficient_eq]
    exact mul_nonneg (div_nonneg (by norm_num) (by positivity)) (Real.arccos_nonneg _)
  have htail : 3 * (1 / (T : ℝ) ^ 2) * n + s ≤ (radiusCoefficient R + ε) * n := by
    have hT0 : (0 : ℝ) < T := by linarith
    have h1 : 1 / (T : ℝ) ^ 2 ≤ ε / 6 := by
      rw [div_le_iff₀ (by positivity)]
      have : 6 ≤ ε * T := by rw [div_le_iff₀ hε] at hTε; linarith
      nlinarith
    have : 3 * (1 / (T : ℝ) ^ 2) ≤ ε / 2 := by linarith
    rw [hs, hδ]
    nlinarith
  by_cases hlow : t < -(T : ℝ)
  · have h1 := crossCount_le_low G (label G R x) hlow.le
    have h2 := pairCount_le_of_not_devEv hxlow
    have h3 := sum_integral_termFn_low_le G R hG (T := (T : ℝ)) (by linarith)
    have h1' : (crossCount G (label G R x) t : ℝ) ≤ pairCount G (label G R x) (lowSet T) := by
      exact_mod_cast h1
    linarith
  by_cases hhigh : (T : ℝ) ≤ t
  · have h1 := crossCount_le_high G (label G R x) hhigh
    have h2 := pairCount_le_of_not_devEv hxhigh
    have h3 := sum_integral_termFn_high_le G R hG (T := (T : ℝ)) (by linarith)
    have h1' : (crossCount G (label G R x) t : ℝ) ≤ pairCount G (label G R x) (highSet T) := by
      exact_mod_cast h1
    linarith
  push Not at hlow hhigh
  obtain ⟨j, hj, hjt, htj⟩ := exists_grid_index (T := T) hK0 hlow hhigh
  have hjL : j ∈ Finset.range L := Finset.mem_range.mpr hj
  have hjt' : τ j ≤ t := hjt
  have htj' : t < τ' j := htj
  have h1 := crossCount_le_grid G (label G R x) hjt' htj'
  have h1' : (crossCount G (label G R x) t : ℝ) ≤
      crossCount G (label G R x) (τ j) + pairCount G (label G R x) (cellSet (τ j) (τ' j)) := by
    rw [← Nat.cast_add]; exact Nat.cast_le.mpr h1
  have h2 := pairCount_le_of_not_devEv (hxc j hjL)
  have h3 := pairCount_le_of_not_devEv (hxcell j hjL)
  rw [← crossCount_eq_pairCount] at h2
  have hwidth : τ' j - τ j = 1 / K := by
    simp only [hτ, hτ']; field_simp; ring
  have hab : τ j ≤ τ' j := by
    have : (0 : ℝ) ≤ 1 / K := by positivity
    linarith
  have h4 := sum_integral_termFn_cross_le G R hcross hG hR (τ j)
  have h5 := sum_integral_termFn_cell_le G R hG hab
  rw [hwidth] at h5
  have h6 : 3 * (1 / (K : ℝ) / 2) ≤ ε / 2 := by
    rw [div_le_iff₀ hε] at hKε
    rw [div_div, mul_div_assoc', div_le_iff₀ (by positivity)]
    nlinarith
  have h7 : 3 * (1 / (K : ℝ) / 2) * n ≤ ε / 2 * n := mul_le_mul_of_nonneg_right h6 hn0.le
  rw [hs, hδ] at h2 h3
  linarith

end CutSweep
end CubicPathwidth

end

#print axioms CubicPathwidth.CutSweep.sweepClaim_of_crossing