Order-seven coefficient simplification

This module registers the dedicated simplifier used by the generated order-seven coefficient certificates.

def Parser.Attr.orderSevenCoefficient_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.orderSevenCoefficient : Lean.ParserDescr

Simplifier for order-seven coefficient expressions.

Equations

• One or more equations did not get rendered due to their size.

def orderSevenNormalizeCoeffSum : Lean.ParserDescr

Normalize the bounded convolution blocks used by order-seven coefficient certificates.

Equations

• orderSevenNormalizeCoeffSum = Lean.ParserDescr.node `orderSevenNormalizeCoeffSum 1024 (Lean.ParserDescr.nonReservedSymbol "order_seven_normalize_coefficient_sum" false)