Arithmetic simplification for ENNReal

ENNReal appears frequently in Mathlib's probability theory and measure theory. This library provides a convenience tactic eq_as_reals for ENNReal (extended non-negative real) numbers or arithmetic expressions.

Installation

Add this project as a dependency to your lakefile.toml:

[[require]]
scope = "wvhulle"
name = "ennreal-arith"
rev = "main" # or a specific commit

Or if you use leanfile.lean,

import Lake
open Lake DSL 

require «ennreal-arith» from git
  "https://github.com/wvhulle/ennreal-arith.git" @ "[COMMIT_HASH]"

Usage

Import in your Lean files:

import ENNRealArith

Use the eq_as_reals tactic to prove equality of probabilities (ENNReal in Mathlib4), lifted into the real numbers:

example : (↑2 : ENNReal) * 1 + ↑3 * 0 + ↑5 = ↑7 := by eq_as_reals

example (a : ℕ) (ha : a ≠ 0) : (↑a : ENNReal) / ↑a = 1 := by eq_as_reals

example (a b c : ℕ) (hc : c ≠ 0) : 
  (↑(a * c) : ENNReal) / (↑(b * c)) = ↑a / ↑b := by eq_as_reals

Testing

To run unit and integration tests, use the following command:

lake test