Bounds And Inequalities

For ordinary numerical inequalities, start with leancert. Use this page when you need the dedicated controls for an interval or box.

Typical goals:

∀ x ∈ I, f x ≤ c
∀ x ∈ I, c ≤ f x
∀ x ∈ I, f x ≤ g x

Primary workflow:

leancert
leancert?

Advanced controls:

certify_bound
interval_bound_subdiv
multivariate_bound

These tactics use the configured certificate-verification route independently of their numerical backend. See the Trust model and Backend selection for those two axes.

For ergonomic raw Lean goals, start with leancert. Use certify_bound when you intentionally want the dedicated single-variable interval engine, including explicit Taylor-depth selection. certify_bound is a numerical portfolio rather than a promise of one fixed backend. Subdivision and global optimization are strategies, not backends. Without a positional Taylor depth it uses the same coordinated three-stage schedule as leancert: Dyadic precision increases from -53 through -85 to -117, while Taylor depth increases by 10 at each stage. A positional depth, for example certify_bound 20, keeps Taylor depth fixed and still adapts Dyadic precision. The final Rational fallback runs only after the Dyadic stages are exhausted.

interval_bound_subdiv depth maxDepth splits candidate boxes and certifies every retained leaf. leancert? reports its configured and deepest depths, boxes examined, certified leaves, whether the addressed frontier passed its structural check, and verification usage. The frontier check establishes a complete canonical binary frontier; the subdivision recursion maintains the association between each address and its proof leaf. See the verification-status table for the precise checker boundary and failure semantics.

Minimal example:

import LeanCert.Tactic

example : ∀ x ∈ Set.Icc (0 : ℝ) 1, Real.exp x ≤ 3 := by
  leancert

Discovery commands can help find a candidate bound before formalizing it. See Optimization and Discovery.

For the full tactic reference, see Reference → Tactics.

For troubleshooting failed interval proofs, see Troubleshooting.