pith. machine review for the scientific record. sign in
theorem proved term proof

coercive_projection_cert

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

formal statement (Lean)

 149theorem coercive_projection_cert : CoerciveProjectionCert where
 150  coercivity_positive := c_coercive_pos

proof body

Term-mode proof.

 151  net_above_one := K_net_gt_one
 152  operator_positive := fun w f hw => energy_bounded_below w f hw (sq_nonneg f)
 153  prefactor_positive := C_ilg_prefactor_pos
 154
 155end
 156
 157end CoerciveProjection
 158end Gravity
 159end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.