module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaProbability`

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

used by (5)

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

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaAmplitude module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeAnalysis module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeStrongClosure module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ObjecthoodRegistry module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparisonExamples module_import

declarations in this module (18)

abbrev Event L34
def count L37
def eventFinset L43
def prob L49
theorem count_empty L52
theorem count_univ L56
theorem count_eq_card L60
theorem prob_empty L64
theorem prob_univ L69
theorem prob_nonneg L77
theorem prob_le_one L83
theorem count_mono L97
theorem prob_mono L106
theorem count_disjoint_or L114
theorem prob_disjoint_or L130
def expectation L139
theorem expectation_const L142
theorem delta_probability_headline L151