CubicPathwidth.T2.DegreeLabelsAmp

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

import CubicPathwidth.T2.DefsB
import CubicPathwidth.GraphLocality

/-!
# Walk amplitudes for degree-sensitive labels

Fix a scale `sc x ∈ [0, 1]` at every vertex. The weight of a walk is the
product of the scales at the heads of its darts, and the amplitude
`amp u w` is the supremum of the weights of walks from `w` to `u`.
With `sc x = (d_x - 1)^{-1/2}`, `amp u w = e^{-D(u,w)}` where `D` is the
directed distance with arc lengths `ℓ(x → y) = ½ ln (d_x - 1)` (the walk from
`w` to `u` is read backwards).

* `amp_self`: `amp u u = 1`;
* `amp_ge_cons`: for every edge `wx`, `sc x * amp u x ≤ amp u w`;
* `amp_tight`: for `w ≠ u` with a neighbor, some neighbor `x` attains
  `amp u w = sc x * amp u x` (a tight parent);
* `amp_concat`: for an edge `uv`, `sc v * amp u w ≤ amp v w`;
* `amp_le_pow_dist`, `reachable_of_amp_pos`: locality.
-/

noncomputable section
open scoped BigOperators
open Classical

namespace CubicPathwidth
namespace T2
namespace DL

variable {n : ℕ} (G : SimpleGraph (Fin n)) (sc : Fin n → ℝ)

/-- Weight of a walk: the product of the scales at the heads of its darts. -/
def wt {a b : Fin n} (p : G.Walk a b) : ℝ := (p.darts.map fun d => sc d.snd).prod

/-- Amplitude at `w` seen from the source `u`. -/
def amp (u w : Fin n) : ℝ := ⨆ p : G.Walk w u, wt G sc p

@[simp] theorem wt_nil (a : Fin n) : wt G sc (SimpleGraph.Walk.nil : G.Walk a a) = 1 := by
  simp [wt]

@[simp] theorem wt_cons {a b c : Fin n} (h : G.Adj a b) (q : G.Walk b c) :
    wt G sc (SimpleGraph.Walk.cons h q) = sc b * wt G sc q := by
  simp [wt]

theorem wt_concat {a b c : Fin n} (p : G.Walk a b) (h : G.Adj b c) :
    wt G sc (p.concat h) = wt G sc p * sc c := by
  simp [wt, SimpleGraph.Walk.darts_concat, List.concat_eq_append]

variable {G sc}

theorem wt_nonneg (h0 : ∀ x, 0 ≤ sc x) {a b : Fin n} (p : G.Walk a b) : 0 ≤ wt G sc p := by
  induction p with
  | nil => simp
  | cons h q ih => rw [wt_cons]; exact mul_nonneg (h0 _) ih

theorem wt_le_pow {σ : ℝ} (h0 : ∀ x, 0 ≤ sc x) (hσ : ∀ x, sc x ≤ σ) {a b : Fin n}
    (p : G.Walk a b) : wt G sc p ≤ σ ^ p.length := by
  induction p with
  | nil => simp
  | cons h q ih =>
    rw [wt_cons, SimpleGraph.Walk.length_cons, pow_succ']
    exact mul_le_mul (hσ _) ih (wt_nonneg h0 q) ((h0 a).trans (hσ a))

theorem wt_le_one (h0 : ∀ x, 0 ≤ sc x) (h1 : ∀ x, sc x ≤ 1) {a b : Fin n}
    (p : G.Walk a b) : wt G sc p ≤ 1 := by
  simpa using wt_le_pow h0 h1 p

theorem bddAbove_wt (h0 : ∀ x, 0 ≤ sc x) (h1 : ∀ x, sc x ≤ 1) (a b : Fin n) :
    BddAbove (Set.range fun p : G.Walk a b => wt G sc p) :=
  ⟨1, by rintro _ ⟨p, rfl⟩; exact wt_le_one h0 h1 p⟩

theorem amp_nonneg (h0 : ∀ x, 0 ≤ sc x) (u w : Fin n) : 0 ≤ amp G sc u w :=
  Real.iSup_nonneg fun p => wt_nonneg h0 p

theorem amp_le_one (h0 : ∀ x, 0 ≤ sc x) (h1 : ∀ x, sc x ≤ 1) (u w : Fin n) :
    amp G sc u w ≤ 1 :=
  Real.iSup_le (fun p => wt_le_one h0 h1 p) zero_le_one

theorem le_amp (h0 : ∀ x, 0 ≤ sc x) (h1 : ∀ x, sc x ≤ 1) {u w : Fin n} (p : G.Walk w u) :
    wt G sc p ≤ amp G sc u w :=
  le_ciSup (bddAbove_wt h0 h1 w u) p

theorem amp_self (h0 : ∀ x, 0 ≤ sc x) (h1 : ∀ x, sc x ≤ 1) (u : Fin n) :
    amp G sc u u = 1 := by
  apply le_antisymm (amp_le_one h0 h1 u u)
  have := le_amp h0 h1 (SimpleGraph.Walk.nil : G.Walk u u)
  simpa using this

/-- Extending walks by a first step. -/
theorem amp_ge_cons (h0 : ∀ x, 0 ≤ sc x) (h1 : ∀ x, sc x ≤ 1) {u w x : Fin n}
    (h : G.Adj w x) : sc x * amp G sc u x ≤ amp G sc u w := by
  unfold amp
  rw [Real.mul_iSup_of_nonneg (h0 x)]
  refine Real.iSup_le (fun q => ?_) (amp_nonneg h0 u w)
  rw [← wt_cons G sc h q]
  exact le_amp h0 h1 _

/-- Changing the source along an edge `uv`. -/
theorem amp_concat (h0 : ∀ x, 0 ≤ sc x) (h1 : ∀ x, sc x ≤ 1) {u v : Fin n}
    (h : G.Adj u v) (w : Fin n) : sc v * amp G sc u w ≤ amp G sc v w := by
  unfold amp
  rw [Real.mul_iSup_of_nonneg (h0 v)]
  refine Real.iSup_le (fun p => ?_) (amp_nonneg h0 v w)
  rw [mul_comm, ← wt_concat G sc p h]
  exact le_amp h0 h1 _

/-- Every vertex other than the source has a neighbor attaining the bound
`amp u w ≤ sc x * amp u x`. -/
theorem amp_le_parent (h0 : ∀ x, 0 ≤ sc x) (h1 : ∀ x, sc x ≤ 1) {u w : Fin n}
    (hne : (G.neighborFinset w).Nonempty) (hwu : w ≠ u) :
    ∃ x, G.Adj w x ∧ amp G sc u w ≤ sc x * amp G sc u x := by
  obtain ⟨x, hx, hmax⟩ := Finset.exists_max_image _ (fun x => sc x * amp G sc u x) hne
  refine ⟨x, (G.mem_neighborFinset w x).mp hx, ?_⟩
  refine Real.iSup_le (fun p => ?_) (mul_nonneg (h0 x) (amp_nonneg h0 u x))
  cases p with
  | nil => exact absurd rfl hwu
  | cons h q =>
    rw [wt_cons]
    exact (mul_le_mul_of_nonneg_left (le_amp h0 h1 q) (h0 _)).trans
      (hmax _ ((G.mem_neighborFinset _ _).mpr h))

theorem amp_tight (h0 : ∀ x, 0 ≤ sc x) (h1 : ∀ x, sc x ≤ 1) {u w : Fin n}
    (hne : (G.neighborFinset w).Nonempty) (hwu : w ≠ u) :
    ∃ x, G.Adj w x ∧ amp G sc u w = sc x * amp G sc u x := by
  obtain ⟨x, hx, hle⟩ := amp_le_parent h0 h1 hne hwu
  exact ⟨x, hx, le_antisymm hle (amp_ge_cons h0 h1 hx)⟩

theorem amp_le_pow_dist {σ : ℝ} (h0 : ∀ x, 0 ≤ sc x) (hσ : ∀ x, sc x ≤ σ)
    (hσ1 : σ ≤ 1) (u w : Fin n) : amp G sc u w ≤ σ ^ G.dist u w := by
  have hσ0 : 0 ≤ σ := (h0 u).trans (hσ u)
  refine Real.iSup_le (fun p => ?_) (pow_nonneg hσ0 _)
  refine (wt_le_pow h0 hσ p).trans (pow_le_pow_of_le_one hσ0 hσ1 ?_)
  rw [G.dist_comm]
  exact G.dist_le p

theorem reachable_of_amp_pos {u w : Fin n} (h : 0 < amp G sc u w) : G.Reachable u w := by
  by_contra hr
  have : IsEmpty (G.Walk w u) := not_nonempty_iff.mp fun hp => hr (SimpleGraph.Reachable.symm hp)
  have h0 : amp G sc u w = 0 := Real.iSup_of_isEmpty _
  linarith

end DL
end T2
end CubicPathwidth
Back to top