module module

`IndisputableMonolith.Information.FEPBridgeFromJCost`

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 (2)

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

IndisputableMonolith.Information module_import
IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (16)

def klQuadratic L34
theorem jcost_log_exact L37
theorem klQuadratic_zero L42
theorem hasDerivAt_klQuadratic L46
theorem deriv_klQuadratic_zero L55
theorem hasDerivAt_deriv_klQuadratic_zero L59
theorem hasDerivAt_deriv_Jlog_zero L68
theorem jcost_kl_same_second_order_at_equilibrium L79
inductive FEPStateClass L94
abbrev Coupling L102
def HasMarkovBlanketSparsity L107
def HasLedgerBoundarySparsity L114
theorem markov_blanket_sparsity_iff_ledger_boundary_sparsity L124
structure FEPBridgeLocalCert L129
def fepBridgeLocalCert L139
theorem fep_bridge_local_cert_holds L144