OAI/Probability/DilutedSpin/ScheduledRegularFrame.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.DepthAverage.regular_no_adjacent_values line 11
2. lemma OAI.DilutedSpinGlass.ReducedTopology.branching_depth_assigned_at line 34
3. lemma OAI.DilutedSpinGlass.ReducedTopology.realize_no_adjacent_at line 44
4. theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_regular_old_count line 54

   Source documentation

   Genuine interior regular assignments discharge the old frame's charging geometry, including arbitrary retained evaluation prefixes and terminal reserve.

   theorem scheduled_regular_old_count {α : Type} [Fintype α] [DecidableEq α]
       (H r d : ℕ) (k : ℕ+) (hk : 2≤(k:ℕ)) (a : α)
       (C : Fin k → ReducedTopology) (e : (j : Fin k) → (C j).Vertex → {j : α // j≠a})
       (Q : α → Fin (H+1+1+r+1+d)) (ha : (Q a).val=r+1+d)
       (had : ∀ j, Admissible (C j) (fun v => (Q (e j v)).val) (r+1+d+1) (r+1+d+1+H))
       {η : ℝ} (hlarge : 1<η*(H+1+1+r+1+d:ℕ)) (hr : DepthAverage.Regular η Q) :
       let Base := PrescribedTree.node k (fun j => realize H (r+1+d+1) (C j) (fun v => (Q (e j v)).val))
   …

   Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.DepthAverage.Regular, OAI.DilutedSpinGlass.ReducedTopology.realize