OAI/Probability/DilutedSpin/ScheduledSingleton.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.PrescribedTree.leafProduct_singleton line 13
2. lemma OAI.DilutedSpinGlass.PrescribedTree.childEnergy_singleton line 17
3. lemma OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt_singleton line 35
4. lemma OAI.DilutedSpinGlass.PrescribedTree.prefixEnergyAt_heightCast line 42
5. lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledShapeEnergy_leaf line 56

   Source documentation

   The base topology in the SAME scheduled covariance family is exactly the conditional singleton covariance controlled by joint_grid_selection.

   lemma scheduledShapeEnergy_leaf (d : ℕ) (hd : d<L) (q : ReducedTopology.leaf.Vertex → ℕ)
       (T : KernelTower Ω L) (f : FinitePath Ω L → Fin N → ℝ) :
       scheduledShapeEnergy L d .leaf q T f=KernelTower.prefixEnergyAt L T d f := by
   …

   Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.scheduledShapeEnergy, OAI.DilutedSpinGlass.KernelTower.prefixEnergyAt