def
definition
mdl_prior
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Information.CompressionPrior on GitHub at line 16.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
13namespace Information
14
15-- Ledger cost J as universal prior for compression
16noncomputable def mdl_prior (_model : Cost.SymmUnit (fun x => x)) : ℝ → ℝ := Cost.Jcost
17
18-- Universal coding: length = J( complexity ) for recognition events
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