def definition def or abbrev

`evidence`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  22def evidence (prior : ProbDist ι) (L : Likelihood ι Obs) (o : Obs) : ℝ :=

Definition body.

  23  ∑ i, prior.prob i * L.like o i
  24

From the project-wide theorem graph. These declarations reference this one in their body.

observationalStatus in IndisputableMonolith.Cosmology.CosmologicalConstant decl_use
anita_inconclusive in IndisputableMonolith.Experimental.ANITAUpgoing decl_use
ea004_certificate in IndisputableMonolith.Experimental.ANITAUpgoing decl_use
btfr_mass_velocity_relation in IndisputableMonolith.Gravity.BTFREmergence decl_use
ComplexFalsifier in IndisputableMonolith.Mathematics.ComplexNumbers decl_use
current_understanding_consistent in IndisputableMonolith.Quantum.BlackHoleInformation decl_use
validAlternativePeriods in IndisputableMonolith.RRF.Hypotheses.EightTick decl_use
BayesianFilteringCert in IndisputableMonolith.Statistics.BayesianFilteringFromVFE decl_use
bayesStep in IndisputableMonolith.Statistics.BayesianFilteringFromVFE decl_use
bayesStep_is_update in IndisputableMonolith.Statistics.BayesianFilteringFromVFE decl_use
evidence_pos in IndisputableMonolith.Statistics.BayesianFilteringFromVFE decl_use
bayesFactorThreshold_cost in IndisputableMonolith.Statistics.BayesianUpdateFromJCost decl_use

Lean names referenced from this declaration's body.

prob in IndisputableMonolith.Decision.StPetersburg decl_use
ProbDist in IndisputableMonolith.Information.ShannonEntropy decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
Likelihood in IndisputableMonolith.Statistics.BayesianFilteringFromVFE decl_use
ProbDist in IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL decl_use