module module

`IndisputableMonolith.Cost.Ndim.RadicalDistribution`

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.Cost.Ndim.Hessian module_import

declarations in this module (14)

def Radical L20
def LevelSet L24
def affineShift L28
theorem mem_Radical_iff L31
theorem mem_LevelSet_iff L34
theorem zero_mem_Radical L37
theorem add_mem_Radical L42
theorem smul_mem_Radical L54
theorem sub_mem_Radical L67
theorem quadraticHessian_eq_zero_iff L74
theorem dot_affineShift L90
theorem affineShift_mem_LevelSet L103
theorem radical_integrable_by_affine_leaves L113
theorem preserves_own_leaf_iff_mem_Radical L121