evalMeasureReal

Mathlib.MeasureTheory.Measure.Real

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.Positivity.evalMeasureReal

Lean4

/-- Extension for the `positivity` tactic: applications of `μ.real` are nonnegative. -/
@[positivity MeasureTheory.Measure.real _ _]
def evalMeasureReal : PositivityExt where
  eval {_ _} _zα _pα
    e := do
    let .app (.app _ a) b ← whnfR e |
      throwError"not measureReal"
    let p ← mkAppOptM ``MeasureTheory.measureReal_nonneg #[none, none, a, b]
    pure (.nonnegative p)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru