OAI/Probability/DilutedSpin/FiniteEncoding.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DilutedSpinGlass.continuous_atomicProbability_joint line 17
  2. def OAI.DilutedSpinGlass.FiniteLaw.nnWeights line 32
  3. def OAI.DilutedSpinGlass.FiniteLaw.asProbability line 38
  4. lemma OAI.DilutedSpinGlass.FiniteLaw.integral_asProbability line 41
  5. lemma OAI.DilutedSpinGlass.FiniteLaw.measurable_asProbability line 47
  6. def OAI.DilutedSpinGlass.labelMoment line 64

    Source documentation

    The exact one-label branching spin moment at a real message or nested probability message. The last transition consists of independent q-spins.

    noncomputable def labelMoment : (r : ℕ) → PrescribedTree (r+1) → Hierarchy r → ℝ
  | 0, .node k _, x => ∏ _ : Fin k, Real.tanh x
  | r+1, .node _ C, η => ∏ j, ∫ x, labelMoment r (C j) x ∂η.toMeasure

namespace KernelTower
variable {Ω : Type} [Fintype Ω]

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.Hierarchy, OAI.DilutedSpinGlass.KernelTower

  7. def OAI.DilutedSpinGlass.KernelTower.encode line 71
  8. def OAI.DilutedSpinGlass.KernelTower.TerminalInterior line 76
  9. lemma OAI.DilutedSpinGlass.KernelTower.encode_moment line 81
  10. lemma OAI.DilutedSpinGlass.DepthAverage.average_split_regular_le line 129
  11. lemma OAI.DilutedSpinGlass.DepthAverage.weighted_sum_eq_average line 144
  12. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_depth_bound line 161
  13. def OAI.DilutedSpinGlass.PrescribedTree.shapeBadConstant line 178
  14. lemma OAI.DilutedSpinGlass.PrescribedTree.shapeBadConstant_nonneg line 181
  15. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_regular_bound line 185
  16. lemma OAI.DilutedSpinGlass.piCongrLeft_const_apply line 211
  17. lemma OAI.DilutedSpinGlass.logMean_reindex line 219
  18. lemma OAI.DilutedSpinGlass.trialLog_reindex line 238
  19. lemma OAI.DilutedSpinGlass.integral_sumPi_exp_add line 250
  20. lemma OAI.DilutedSpinGlass.logMean_sum_separate line 263