OAI/Probability/DilutedSpin/QSubtreePotential.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DilutedSpinGlass.FiniteLaw.asProbability_id_singleton line 13
  2. lemma OAI.DilutedSpinGlass.FiniteLaw.asProbability_eq_map line 20
  3. lemma OAI.DilutedSpinGlass.FiniteLaw.asProbability_pi line 31
  4. lemma OAI.DilutedSpinGlass.FiniteLaw.integral_pi_asProbability line 50
  5. def OAI.DilutedSpinGlass.PrescribedTree.subsetOverlap line 69
  6. lemma OAI.DilutedSpinGlass.PrescribedTree.SplitMap.prod_range line 73
  7. lemma OAI.DilutedSpinGlass.PrescribedTree.SplitMap.expect_subsetOverlap line 85
  8. lemma OAI.DilutedSpinGlass.PrescribedTree.subsetOverlap_bound line 101
  9. lemma OAI.DilutedSpinGlass.PrescribedTree.qEmbed_realize_le line 122
  10. def OAI.DilutedSpinGlass.PrescribedTree.subtreePotential line 150
  11. lemma OAI.DilutedSpinGlass.PrescribedTree.subtreePotential_nonneg line 156
  12. lemma OAI.DilutedSpinGlass.PrescribedTree.le_subtreePotential line 164
  13. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_subtree_depth_bound line 180
  14. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_subtree_regular_bound line 203
  15. lemma OAI.DilutedSpinGlass.logMean_constant line 228
  16. lemma OAI.DilutedSpinGlass.trialLog_constant line 239
  17. lemma OAI.DilutedSpinGlass.trialLog_sum_separate line 245
  18. def OAI.DilutedSpinGlass.blockSuccEquiv line 267

    Source documentation

    A label block split at its first interaction occurrence.

    def blockSuccEquiv (ι : Type) (k : ℕ) : ι ⊕ (Fin k × ι) ≃ Fin (k+1) × ι where
…
  19. lemma OAI.DilutedSpinGlass.trialLog_blocks line 273