AdmissibleInterval.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.ReducedTopology.admissible_update_between line 14
Source documentation
With every other depth fixed, admissible values of one branching coordinate form an interval. No spacing or regularity is needed here.
```
lemma admissible_update_between (S : ReducedTopology) (q : S.Vertex → ℕ) (v : S.Vertex)
    {a b t lo hi : ℕ} (hat : a≤t) (htb : t≤b)
    (ha : Admissible S (updateCoordinate q v a) lo hi)
    (hb : Admissible S (updateCoordinate q v b) lo hi) :
    Admissible S (updateCoordinate q v t) lo hi := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.updateCoordinate

theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_vertex_Ico_energy_le line 44

Source documentation

Interval form of the literal one-vertex Dirichlet-energy estimate.

theorem scheduled_vertex_Ico_energy_le {Ω : Type} [Fintype Ω]
    (H d : ℕ) (S : ReducedTopology) (q : S.Vertex → ℕ) (v : S.Vertex)
    (a b : ℕ) (hab : a≤b)
    (ha : Admissible S (updateCoordinate q v a) d (d+H))
    (hb : Admissible S (updateCoordinate q v b) d (d+H))
    (T : KernelTower Ω H) (f : FinitePath Ω H → ℝ) (hf : ∀ x, |f x| ≤ 1) :
    (∑ t ∈ Finset.Ico a b,
      (PrescribedTree.treeMean (realize H d S (updateCoordinate q v t)) T f-
       PrescribedTree.treeMean (realize H d S (updateCoordinate q v (t+1))) T f)^2) ≤
      (vertexArity S v:ℝ)^2 := by
…

Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.updateCoordinate, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.treeMean, OAI.DilutedSpinGlass.ReducedTopology.realize, OAI.DilutedSpinGlass.ReducedTopology.vertexArity

theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_vertex_subset_energy_le line 71

Source documentation

Restriction to ANY set of allowed one-step shifts cannot raise the single-coordinate energy. The proof uses the actual admissible hull.

theorem scheduled_vertex_subset_energy_le {Ω : Type} [Fintype Ω]
    (H d : ℕ) (S : ReducedTopology) (q : S.Vertex → ℕ) (v : S.Vertex)
    (I : Finset ℕ)
    (ha : ∀ t ∈ I, Admissible S (updateCoordinate q v t) d (d+H) ∧
      Admissible S (updateCoordinate q v (t+1)) d (d+H))
    (T : KernelTower Ω H) (f : FinitePath Ω H → ℝ) (hf : ∀ x, |f x| ≤ 1) :
    (∑ t ∈ I,
      (PrescribedTree.treeMean (realize H d S (updateCoordinate q v t)) T f-
       PrescribedTree.treeMean (realize H d S (updateCoordinate q v (t+1))) T f)^2) ≤
      (vertexArity S v:ℝ)^2 := by
…