OAI/Probability/DilutedSpin/ScheduledEnergyBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.FiniteLaw.centered_square_le_one line 12
2. lemma OAI.DilutedSpinGlass.FiniteLaw.covariance_sq_le_one line 26
3. lemma OAI.DilutedSpinGlass.FiniteLaw.covarianceEnergy_le_one line 34
4. lemma OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt_le_one line 52
5. lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledShapeEnergy_le_one line 70
6. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalScheduledEnergy_le_one line 89

   Source documentation

   Unit bound for the actual physical covariance, including N=0, leaves, inadmissible schedules and the countable variable-alphabet root.

   lemma physicalScheduledEnergy_le_one (M : Model p) (θB hB : ℝ) (N L : ℕ)
       (u : Spec L × ℕ → ℝ) (S : ReducedTopology) (Q : Option S.Vertex → Fin (L+1)) :
       physicalScheduledEnergy M θB hB N L u S Q≤1 := by
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.UniversalDictionary.physicalScheduledEnergy