CubicPathwidth.T2.Defs

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

import CubicPathwidth.T2Spec
import CubicPathwidth.C3.Defs

/-!
# Plan interfaces for Theorem 2 (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.

Part (a), plain sweep with labels of base `3^{-1/2}`:
* `PlainLayoutClaim` (O1): injective labels whose frontiers all have at most
  `w` vertices give a path decomposition of width at most `w`.
* `StarFourClaim` (O2–O5): the frontier probability of a vertex star with
  incident correlations at least `r` is at most `f_{4,r}(τ)`. To be derived
  from `SimplexFourClaim`.
* `GoodLabels4 R` (O6, O8): at radius `R`, for large `n`, some injective
  labeling has every frontier of size at most `(idealSup (r_R) + ε) n`.
* `IdealLimitClaim` (O7): `idealSup (r_R) → F₄` as `R → ∞`.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Filter Topology

namespace CubicPathwidth
namespace T2

/-- Correlation floor of the base-`3^{-1/2}` labels at radius `R`. -/
def radiusCorr4 (R : ℕ) : ℝ := r44 * (1 - 1 / (R : ℝ))

/-- `sup_τ f_{4,r}(τ)`. -/
def idealSup (r : ℝ) : ℝ := sSup (Set.range fun τ : ℝ => idealStarFn 4 r τ)

theorem idealSup_r44 : idealSup r44 = F4 := rfl

/-- (O1) Plain-sweep layout. `C3.outerFrontier G y t` is
`{v | t < y v ∧ ∃ u, G.Adj u v ∧ y u ≤ t}`, the frontier `Fr(t)`. -/
def PlainLayoutClaim : Prop :=
  ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (y : Fin n → ℝ), Function.Injective y →
    ∀ w : ℝ, (∀ t : ℝ, ((C3.outerFrontier G y t).card : ℝ) ≤ w) →
      HasPathwidthAtMost G w

/-- (O2–O5) Star comparison for at most four neighbors, every threshold. -/
def StarFourClaim : Prop :=
  ∀ (m : ℕ) (r : ℝ), 0 < r → r < 1 →
    ∀ (a : GaussianField.Sample m) (d : ℕ), d ≤ 4 →
      ∀ b : Fin d → GaussianField.Sample m,
        ‖a‖ = 1 → (∀ i, ‖b i‖ = 1) → (∀ i, r ≤ ⟪a, b i⟫) →
        ∀ τ : ℝ,
          (stdGaussian (GaussianField.Sample m)).real
              {x | τ < ⟪a, x⟫ ∧ ∃ i, ⟪b i, x⟫ ≤ τ} ≤ idealStarFn 4 r τ

/-- (O6, O8) Good labels at a fixed radius. -/
def GoodLabels4 (R : ℕ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
    ∀ G : SimpleGraph (Fin n), MaxDegreeAtMost 4 G →
      ∃ y : Fin n → ℝ, Function.Injective y ∧
        ∀ t : ℝ, ((C3.outerFrontier G y t).card : ℝ) ≤ (idealSup (radiusCorr4 R) + ε) * n

/-! ## Shared analytic leaves -/

/-- Gram matrix of finitely many vectors. -/
def gram {m k : ℕ} (w : Fin k → GaussianField.Sample m) : Matrix (Fin k) (Fin k) ℝ :=
  fun i j => ⟪w i, w j⟫

/-- (O2) Bridge: `N(0, Gram w)` is the law of `(⟨w_j, x⟩)_j` for standard
Gaussian `x`. Connects `gaussProb` (approval surface) with the inner-product
model used by the C3 development. -/
def BridgeClaim : Prop :=
  ∀ (m k : ℕ) (w : Fin k → GaussianField.Sample m) (A : Set (EuclideanSpace ℝ (Fin k))),
    MeasurableSet A →
      gaussProb (gram w) A =
        (stdGaussian (GaussianField.Sample m)).real
          {x | (WithLp.toLp 2 fun j => ⟪w j, x⟫ : EuclideanSpace ℝ (Fin k)) ∈ A}

/-- (O3) Slepian's inequality for upper orthants, in the inner-product model.
Equal variances; every off-diagonal covariance of `a` at most that of `b`.
Singular configurations are included. -/
def SlepianClaim : Prop :=
  ∀ (m k : ℕ) (a b : Fin k → GaussianField.Sample m),
    (∀ i, ‖a i‖ = ‖b i‖) → (∀ i j, i ≠ j → ⟪a i, a j⟫ ≤ ⟪b i, b j⟫) →
    ∀ t : Fin k → ℝ,
      (stdGaussian (GaussianField.Sample m)).real {x | ∀ i, t i < ⟪a i, x⟫} ≤
        (stdGaussian (GaussianField.Sample m)).real {x | ∀ i, t i < ⟪b i, x⟫}

/-- (O7) Continuity of the ideal supremum at `r₄₄` from below. -/
def IdealLimitClaim : Prop :=
  Tendsto (fun R : ℕ => idealSup (radiusCorr4 R)) atTop (𝓝 F4)

end T2
end CubicPathwidth
Back to top