evalERealToReal — Mathlib

Lean4
/-- Extension for the `positivity` tactic: projection from `EReal` to `ℝ`.

We prove that `EReal.toReal x` is nonnegative whenever `x` is nonnegative.
Since `EReal.toReal ⊤ = 0`, we cannot prove a stronger statement,
at least without relying on a tactic like `finiteness`. -/
@[positivity EReal.toReal _]
def evalERealToReal : PositivityExt where
  eval {u α} _zα _pα
    e := do
    match u, α, e with
    | 0, ~q(Real), ~q(EReal.toReal $a) =>
      assertInstancesCommute
      match (← core q(inferInstance) q(inferInstance) a).toNonneg with
      | .some pa =>
        pure (.nonnegative q(EReal.toReal_nonneg $pa))
      | _ =>
        pure .none
    | _, _, _ =>
      throwError"not EReal.toReal"
Похожие утверждения