OAI/Probability/DilutedSpin/RegularFrameExtraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.ReducedTopology.admissible_replace_upper line 12
2. theorem OAI.DilutedSpinGlass.ReducedTopology.regular_node_frame line 24

   Source documentation

   Every assignment in the actual regular/admissible parent domain is one of the literal frames of physical_grid_scheduled_step. The extraction keeps the complete terminal horizon, evaluation level and first branching level; it loses neither endpoint cases nor further child branching coordinates.

   theorem regular_node_frame {L : ℕ} [NeZero L] {η : ℝ} (hη : 0<η)
       (hlarge : 1<η*(L:ℝ)) (k : ℕ+) (hk : 2≤(k:ℕ)) (C : Fin k → ReducedTopology)
       (Q : Option (ReducedTopology.node k hk C).Vertex → Fin L)
       (hQ : regularShapeDomain (.node k hk C) L η Q) :
       ∃ H r d : ℕ, L=H+1+1+r+1+(d+1) ∧ (Q none).val=d+1 ∧
         (Q (some none)).val=r+1+(d+1) ∧
         ∀ j, Admissible (C j) (fun v => (Q (some (some ⟨j,v⟩))).val)
           (r+1+(d+1)+1) (r+1+(d+1)+1+H) := by
   …

   Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.regularShapeDomain, OAI.DilutedSpinGlass.ReducedTopology.Admissible