Finiteness tactic

This file implements a basic finiteness tactic, designed to solve goals of the form *** < ∞ and (equivalently) *** ≠ ∞ in the extended nonnegative reals (ENNReal, aka ℝ≥0∞).

It works recursively according to the syntax of the expression. It is implemented as an aesop rule set.

TODO: improve finiteness to also deal with other situations, such as balls in proper spaces with a locally finite measure.

Lemmas

theorem ENNReal.ofNat_ne_top (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n ≠ ⊤

theorem ENNReal.inv_ne_top' {a : ENNReal} (h : a ≠ 0) : a⁻¹ ≠ ⊤

theorem ENNReal.add_ne_top' {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a + b ≠ ⊤

Tactic implementation

def PositivityForAesop : Lean.Elab.Tactic.TacticM Unit

A version of the positivity tactic for use by aesop.

Equations

• PositivityForAesop = Lean.Elab.Tactic.liftMetaTactic fun (g : Lean.MVarId) => do Mathlib.Meta.Positivity.positivity g pure []

def finiteness : Lean.ParserDescr

Tactic to solve goals of the form *** < ∞ and (equivalently) *** ≠ ∞ in the extended nonnegative reals (ℝ≥0∞).

Equations

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

Tests