CubicPathwidth.CutSweep.Defs

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

import CubicPathwidth.CutSweepSpec
import CubicPathwidth.BisectionLimit
import CubicPathwidth.GaussianField

/-!
# Plan interfaces for the cut sweep (not the approval surface)

Every `...Claim` below is a proposition DEFINED here, not assumed. Theorems
that use one take it as an explicit hypothesis and are conditional until it is
proved. No axiom is introduced.

The children follow Section 3 (`sec:warmup`) of the manuscript:
* `ConstantClaim` (N1): `c_* = (3/(2π)) arcsin(1/3)` and `c_* < 1/6`
  (the constant paragraph of Section 3 (`sec:warmup`), by the triple-angle formula);
* `LayoutClaim` (L1): pathwidth is at most cutwidth (Lemma 3.2, `lem:warmup-layout`);
* `OrderingClaim` (L2): ordering by distinct labels has every prefix cut equal
  to a threshold count `crossCount` (the conclusion of Section 3 (`sec:warmup`));
* `CrossingClaim` (G2): two unit-variance Gaussians with correlation `ρ` are on
  opposite sides of a threshold with probability at most `arccos ρ / π`
  (`lem:crossing`(b));
* `SweepClaim` (C1, C2): at a fixed radius `R ≥ 1`, for large `n`, some
  injective labeling has every threshold count at most `(β_R + ε) n`, where
  `β_R = radiusCoefficient R` (the grid and concentration steps of Section 3 (`sec:warmup`)).
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory

namespace CubicPathwidth
namespace CutSweep

variable {n : ℕ}

/-- The vertices with label at most `t`, the set `S_t` of Section 3 (`sec:warmup`). -/
def levelSet (y : Fin n → ℝ) (t : ℝ) : Finset (Fin n) :=
  Finset.univ.filter (fun v => y v ≤ t)

/-- `e_t = e(S_t)`, the number of edges crossing the threshold `t`. -/
def crossCount (G : SimpleGraph (Fin n)) (y : Fin n → ℝ) (t : ℝ) : ℕ :=
  cutSize G (levelSet y t)

/-- (N1) The constant, in the manuscript's form, is below `1/6`. -/
def ConstantClaim : Prop :=
  bisectionCoefficient = (3 / (2 * Real.pi)) * Real.arcsin (1 / 3) ∧
    bisectionCoefficient < (1 : ℝ) / 6

/-- (L1) Lemma 3.2 (`lem:warmup-layout`): pathwidth is at most cutwidth, for every graph. -/
def LayoutClaim : Prop :=
  ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (w : ℝ),
    HasCutwidthAtMost G w → HasPathwidthAtMost G w

/-- (L2) Ordering by distinct labels: if every threshold count is at most `w`,
the cutwidth is at most `w`. -/
def OrderingClaim : Prop :=
  ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (y : Fin n → ℝ), Function.Injective y →
    ∀ w : ℝ, (∀ t : ℝ, (crossCount G y t : ℝ) ≤ w) → HasCutwidthAtMost G w

/-- (G2) Lemma 3.3 (`lem:crossing`)(b) for projections of a standard Gaussian onto unit
vectors `a` and `b`, whose correlation is `⟪a, b⟫`. -/
def CrossingClaim : Prop :=
  ∀ (m : ℕ) (a b : GaussianField.Sample m), ‖a‖ = 1 → ‖b‖ = 1 → ∀ t : ℝ,
    (stdGaussian (GaussianField.Sample m)).real
        {x | min ⟪a, x⟫ ⟪b, x⟫ ≤ t ∧ t < max ⟪a, x⟫ ⟪b, x⟫} ≤
      Real.arccos ⟪a, b⟫ / Real.pi

/-- (C1, C2) Good labels at a fixed radius. -/
def SweepClaim : Prop :=
  ∀ R : ℕ, 0 < R → ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
    ∀ G : SimpleGraph (Fin n), IsSubcubic G →
      ∃ y : Fin n → ℝ, Function.Injective y ∧
        ∀ t : ℝ, (crossCount G y t : ℝ) ≤ (radiusCoefficient R + ε) * n

end CutSweep
end CubicPathwidth
Back to top