ScheduledContinuity.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.ReducedTopology.realize_stem line 13
Source documentation
Before its first scheduled branching, the realized topology is exactly an initial unary stem; all later vertex assignments are unchanged.
```
lemma realize_stem (n r d : ℕ) (S : ReducedTopology) (q : S.Vertex → ℕ)
    (hq : ∀ v, d+r ≤ q v) :
    realize (n+r) d S q = PrescribedTree.stem (realize n (d+r) S q) r := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.realize, OAI.DilutedSpinGlass.PrescribedTree.stem
def OAI.DilutedSpinGlass.ReducedTopology.rootSchedule line 35
Source documentation
One assigned branching coordinate and all its later child coordinates.
```
def rootSchedule {k : ℕ+} {hk : 2 ≤ (k:ℕ)} {C : Fin k → ReducedTopology}
    (t : ℕ) (Q : (i : Fin k) → (C i).Vertex → ℕ) : (node k hk C).Vertex → ℕ :=
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex
theorem OAI.DilutedSpinGlass.ReducedTopology.realize_splitFamily line 43
Source documentation
The realized topology with one ranged root depth is the literal split family, not just an isomorphic unordered or unlabeled tree.
```
theorem realize_splitFamily (k : ℕ+) (hk : 2 ≤ (k:ℕ)) (C : Fin k → ReducedTopology)
    (Q : (i : Fin k) → (C i).Vertex → ℕ) (n r d : ℕ)
    (hQ : ∀ i v, d+r+1 ≤ Q i v) (t : Fin (r+1)) :
    realize (n+r+1) d (node k hk C) (rootSchedule (d+t.val) Q) =
      PrescribedTree.splitFamily k (fun i => realize n (d+r+1) (C i) (Q i)) r t := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.realize, OAI.DilutedSpinGlass.ReducedTopology.rootSchedule, OAI.DilutedSpinGlass.PrescribedTree.splitFamily
theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_split_energy_le line 80
Source documentation
Genuine one-coordinate energy bound for a scheduled reduced topology. Every descendant depth is held fixed while the current branching depth is ranged over the full available interval. All transition kernels are arbitrary.
```
theorem scheduled_split_energy_le (k : ℕ+) (hk : 2 ≤ (k:ℕ)) (C : Fin k → ReducedTopology)
    (Q : (i : Fin k) → (C i).Vertex → ℕ) (n r d : ℕ)
    (hQ : ∀ i v, d+r+1 ≤ Q i v)
    (T : KernelTower Ω (n+r+1)) (f : FinitePath Ω (n+r+1) → ℝ)
    (hf : ∀ x, |f x| ≤ 1) :
    (∑ t : Fin r,
      (PrescribedTree.treeMean
        (realize (n+r+1) d (node k hk C) (rootSchedule (d+t.val) Q)) T f -
       PrescribedTree.treeMean
        (realize (n+r+1) d (node k hk C) (rootSchedule (d+t.val+1) Q)) T f)^2) ≤ (k:ℝ)^2 := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.treeMean, OAI.DilutedSpinGlass.ReducedTopology.realize, OAI.DilutedSpinGlass.ReducedTopology.rootSchedule