module module

`IndisputableMonolith.Verification.ProbabilityNormalizationCert`

show as: view Lean formalization →

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

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Measurement.BornRuleLight module_import

declarations in this module (7)

def prob_from_cost L45
lemma exp_sum_pos L49
lemma exp_sum_ne_zero L53
lemma prob_nonneg L57
lemma prob_le_one L64
theorem prob_normalization L70
structure ProbabilityNormalizationCert L77