OAI/Probability/DilutedSpin/ProxyRateIncrement.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.UniversalDictionary.energyCavityIncrement_proxy_bound line 13
2. lemma OAI.DilutedSpinGlass.pressure_le_variationalValue_exact line 54

   Source documentation

   The upper comparison for the exact arity and first-moment hypotheses of main:theorem; no bounded representative is assumed.

   lemma pressure_le_variationalValue_exact {p N : ℕ} (M : Model p)
       (hM : Admissible M) (hN : 0<N) : pressure M N ≤ variationalValue M := by
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.Admissible, OAI.DilutedSpinGlass.pressure, OAI.DilutedSpinGlass.variationalValue

3. lemma OAI.DilutedSpinGlass.variationalValue_le_functional_exact line 63