OAI/Probability/DilutedSpin/UpperInsertion.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.abs_integral_le_bound_ae line 12
2. lemma OAI.DilutedSpinGlass.UniversalDictionary.randomInsertionOn_comparison_tendsto_ae line 22
3. lemma OAI.DilutedSpinGlass.UniversalDictionary.poissonInsertionOn_comparison_tendsto_ae line 50
4. def OAI.DilutedSpinGlass.PrescribedTree.referenceD line 92
5. def OAI.DilutedSpinGlass.PrescribedTree.mixedNormalizedAvg line 95
6. lemma OAI.DilutedSpinGlass.PrescribedTree.mixedNormalizedAvg_bound line 101
7. lemma OAI.DilutedSpinGlass.PrescribedTree.mixedNormalizedAvg_limit line 132
8. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_mixedNormalizedAvg line 156
9. lemma OAI.DilutedSpinGlass.PrescribedTree.integrable_mixedNormalizedAvg line 165
10. def OAI.DilutedSpinGlass.PrescribedTree.regularization line 176
11. lemma OAI.DilutedSpinGlass.PrescribedTree.regularization_nonneg line 178
12. lemma OAI.DilutedSpinGlass.PrescribedTree.regularization_lt_one line 183
13. lemma OAI.DilutedSpinGlass.PrescribedTree.regularization_limit line 187
14. lemma OAI.DilutedSpinGlass.PrescribedTree.integral_mixedNormalizedAvg_limit line 192
15. lemma OAI.DilutedSpinGlass.PrescribedTree.integral_mixedEnergy_combination_nonpos line 215

    Source documentation

    First-moment common-tree insertion inequality (unregularized).

    lemma integral_mixedEnergy_combination_nonpos (M : Model p) (hM : Admissible M)
        (T : KernelTower Ω n) (Q : FiniteLaw R) (U : R → KernelTower Λ n)
        (V : FinitePath Ω n → Fin N → Spin) (x : R → FinitePath Λ n → ℝ)
        (m : Fin (n+1) → ℝ) (hm : Monotone m) (hpos : ∀ j, 0 ≤ m j)
        (hstrict : ∀ j : Fin n,0 < m j.succ) (hroot : m 0=0) (hend : m (Fin.last n)=1)
        (j : Fin p) :
        (∫ z,mixedEnergyAvg T Q U V x m z (fun _ => true) ∂M.disorder.toMeasure)-
          (p:ℝ)*(∫ z,mixedEnergyAvg T Q U V x m z (fun l => decide (l=j)) ∂M.disorder.toMeasure)+
          ((p-1:ℕ):ℝ)*(∫ z,mixedEnergyAvg T Q U V x m z (fun _ => false) ∂M.disorder.toMeasure) ≤0 := by
    …

    Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.Admissible, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.PrescribedTree.mixedEnergyAvg

16. lemma OAI.DilutedSpinGlass.mixedSpinLaw_single line 261
17. lemma OAI.DilutedSpinGlass.mixedEnergy_single line 271
18. lemma OAI.DilutedSpinGlass.mixedEnergy_last line 278