OAI/Probability/DilutedSpin/ScheduledGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.ReducedTopology.vertex_card_add_one_le_leaf_card line 12
2. lemma OAI.DilutedSpinGlass.ReducedTopology.branching_depth_assigned line 25
3. theorem OAI.DilutedSpinGlass.ReducedTopology.realize_no_adjacent line 37

   Source documentation

   Exact geometric justification of the shifted charging hypothesis for all admissible regular assignments of any reduced topology.

   theorem realize_no_adjacent {L : ℕ} [NeZero L] (S : ReducedTopology)
       (q : S.Vertex → Fin L) (hq : Admissible S (fun v => (q v).val) 0 L)
       {η : ℝ} (hlarge : 1<η*(L:ℝ)) (hr : DepthAverage.Regular η q) :
       PrescribedTree.NoAdjacentBranchDepths (realize L 0 S (fun v => (q v).val)) := by
   …

   Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.DepthAverage.Regular, OAI.DilutedSpinGlass.PrescribedTree.NoAdjacentBranchDepths, OAI.DilutedSpinGlass.ReducedTopology.realize

4. theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_shifted_counts line 61

   Source documentation

   The two aligned target copies contribute two occurrences of EVERY branching vertex. The old tree has none at the shifted depths.

   theorem scheduled_shifted_counts {L : ℕ} [NeZero L] (S : ReducedTopology)
       (q : S.Vertex → Fin L) (hq : Admissible S (fun v => (q v).val) 0 L)
       {η : ℝ} (hlarge : 1<η*(L:ℝ)) (hr : DepthAverage.Regular η q) :
       let T := realize L 0 S (fun v => (q v).val)
   …

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