`prior_holds`

proved

show as: view math explainer →

module: IndisputableMonolith.Information.CompressionPrior
domain: Information
line: 22 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.CompressionPrior on GitHub at line 22.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  19noncomputable def coding_length (events : ℕ) : ℝ := Cost.Jcost (events : ℝ)
  20
  21/-- Theorem: φ-prior holds as unique MDL from T5 J-unique. -/
  22theorem prior_holds : ∀ model, mdl_prior model = Cost.Jcost := by
  23  intro model
  24  simp [mdl_prior]
  25
  26end Information
  27end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.