No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
18structure Likelihood (ι Obs : Type*) where
19 like : Obs → ι → ℝ
20 like_pos : ∀ o i, 0 < like o i
21
used by (9)
From the project-wide theorem graph. These declarations reference this one in their body.
-
eventWeight_pos
in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.BooleanRatioBridge
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
in IndisputableMonolith.Statistics.BayesianFilteringFromVFE
decl_use
-
evidence_pos
in IndisputableMonolith.Statistics.BayesianFilteringFromVFE
decl_use
-
iterFilter
in IndisputableMonolith.Statistics.BayesianFilteringFromVFE
decl_use
-
iterFilter_cons
in IndisputableMonolith.Statistics.BayesianFilteringFromVFE
decl_use
-
iterFilter_nil
in IndisputableMonolith.Statistics.BayesianFilteringFromVFE
decl_use