module module

`IndisputableMonolith.Cost.Ndim.CurvatureBridge`

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.BlockReduction module_import

declarations in this module (15)

def hFull L54
def hInvFull L61
theorem hInvFull_symm L67
theorem hFull_mul_hInvFull L79
def beta L146
theorem beta_eq_zero L153
def RiemannLowerApply L164
def RiemannMixedApply L169
theorem sum_restrict_pair L179
theorem sum2_restrict_pair L192
theorem hInvFull_spectator L211
theorem dot_sharp_Dinv_twoSparse L222
theorem riemann_beta_numerator_zero L235
theorem RiemannMixedApply_reduce L265
theorem RiemannMixedApply_neg L409