Measurability

We define the measurability tactic using aesop.

def attrMeasurability : Lean.ParserDescr

The measurability attribute used to tag measurability statements for the measurability tactic.

Equations

• attrMeasurability = Lean.ParserDescr.node `attrMeasurability 1024 (Lean.ParserDescr.nonReservedSymbol "measurability" false)

def tacticMeasurability : Lean.ParserDescr

The tactic measurability solves goals of the form Measurable f, AEMeasurable f, StronglyMeasurable f, AEStronglyMeasurable f μ, or MeasurableSet s by applying lemmas tagged with the measurability user attribute.

Equations

• tacticMeasurability = Lean.ParserDescr.node `tacticMeasurability 1024 (Lean.ParserDescr.nonReservedSymbol "measurability" false)

def tacticMeasurability? : Lean.ParserDescr

The tactic measurability? solves goals of the form Measurable f, AEMeasurable f, StronglyMeasurable f, AEStronglyMeasurable f μ, or MeasurableSet s by applying lemmas tagged with the measurability user attribute, and suggests a faster proof script that can be substituted for the tactic call in case of success.

Equations

• tacticMeasurability? = Lean.ParserDescr.node `tacticMeasurability? 1024 (Lean.ParserDescr.nonReservedSymbol "measurability?" false)

def measurability! : Lean.ParserDescr

Equations

• measurability! = Lean.ParserDescr.node `measurability! 1024 (Lean.ParserDescr.nonReservedSymbol "measurability!" false)

def measurability!? : Lean.ParserDescr

Equations

• measurability!? = Lean.ParserDescr.node `measurability!? 1024 (Lean.ParserDescr.nonReservedSymbol "measurability!?" false)