module module

`IndisputableMonolith.Information.NESSConditionalIndependenceMeasure`

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

declarations in this module (11)

structure BlanketProjection L31
def atomSet L37
def internalBlanketSet L42
def blanketExternalSet L47
def blanketSet L52
def CondIndepGivenBlanket L57
def LedgerBoundarySparsity L69
theorem ledger_sparsity_implies_measure_condIndep L77
theorem conditional_product_form L87
structure NESSMeasureCert L97
theorem nessMeasureCert_holds L111