Convergence from proved bounds

converges applies convergence and error-bound theorems, using the hypotheses in the goal. It supports contractive fixed-point iterations and strongly monotone, Lipschitz gradient-descent operators. It does not infer convexity from model syntax or claim arbitrary training converges. Use converges? to inspect the proof, or register a proved rule with @[converges].

def attrConverges : Lean.ParserDescr

Register a convergence or error-bound theorem, retaining all its hypotheses.

def tacticConverges : Lean.ParserDescr

Prove supported convergence or rate goals; fail if any hypothesis remains unproved.

def tacticConverges? : Lean.ParserDescr

Prove supported convergence or rate goals; fail if any hypothesis remains unproved.