OAI/Probability/DilutedSpin/QTreeLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.qExpect line 11
2. theorem OAI.DilutedSpinGlass.PrescribedTree.qExpect_const line 16
3. theorem OAI.DilutedSpinGlass.PrescribedTree.qExpect_mono line 27
4. theorem OAI.DilutedSpinGlass.PrescribedTree.abs_qExpect_le line 37
5. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_nonneg line 49
6. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_sum line 57
7. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_mul_const line 64
8. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_mono_leaves line 72

   Source documentation

   Only the genuine reachable terminal leaf number is required.

   lemma qExpect_mono_leaves {n : ℕ} (m : Fin (n+1) → ℝ)
       (hm : Monotone m) (hpos : ∀ j, 0 ≤ m j) (F G : PrescribedTree n → ℝ)
       (k : ℕ) (S : PrescribedTree n)
       (hFG : ∀ T, T.leaves=S.leaves+k → F T≤G T) :
       qExpect m F k S≤qExpect m G k S := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.qExpect

9. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_grid_le_historyMass line 90
10. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_grid_branching line 112