OAI/Probability/DilutedSpin/RegularScheduleShift.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.ReducedTopology.admissible_order_map line 15

   Source documentation

   An order-preserving re-assignment of every actual branching vertex preserves the strict ancestral schedule.

   lemma admissible_order_map (S : ReducedTopology) (q q' : S.Vertex → ℕ)
       {lo lo' hi hi' : ℕ} (hq : Admissible S q lo hi)
       (hl : ∀ v, lo' ≤ q' v) (hu : ∀ v, q' v < hi')
       (ho : ∀ u v, q u < q v → q' u < q' v) : Admissible S q' lo' hi' := by
   …

   Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible

2. lemma OAI.DilutedSpinGlass.ReducedTopology.regular_depth_gap line 33
3. lemma OAI.DilutedSpinGlass.ReducedTopology.shifted_val_bounds line 51
4. theorem OAI.DilutedSpinGlass.ReducedTopology.admissible_regular_shift line 66

   Source documentation

   All intermediate positive one-step shifts of a regular admissible assignment are genuine admissible shapes, with the original horizon.

   theorem admissible_regular_shift (S : ReducedTopology) {η : ℝ}
       (hlarge : 1<η*(L:ℝ)) (q : S.Vertex → Fin L)
       {lo : ℕ} (hq : Admissible S (fun v => (q v).val) lo L) (hr : DepthAverage.Regular η q)
       (s : S.Vertex → Bool) :
       Admissible S (fun v => (DepthAverage.shiftPerm (s v) (q v)).val) lo L := by
   …

   Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.DepthAverage.Regular, OAI.DilutedSpinGlass.DepthAverage.shiftPerm