mathlib documentation

measure_theory.tactic

Tactics for measure theory #

Currently we have one domain-specific tactic for measure theory: measurability.

This tactic is to a large extent a copy of the continuity tactic by Reid Barton.

measurability tactic #

Automatically solve goals of the form measurable f, ae_measurable f μ and measurable_set s.

Mark lemmas with @[measurability] to add them to the set of lemmas used by measurability. Note: to_additive doesn't know yet how to copy the attribute to the additive version.

source
meta def measurability  :
(user_attribute unit)

User attribute used to mark tactics used by measurability.

source
meta def tactic.apply_measurable.comp  :
tactic unit

Tactic to apply measurable.comp when appropriate.

Applying measurable.comp is not always a good idea, so we have some extra logic here to try to avoid bad cases.

  • If the function we're trying to prove measurable is actually constant, and that constant is a function application f z, then measurable.comp would produce new goals measurable f, measurable (λ _, z), which is silly. We avoid this by failing if we could apply measurable_const.

  • measurable.comp will always succeed on measurable (λ x, f x) and produce new goals measurable (λ x, x), measurable f. We detect this by failing if a new goal can be closed by applying measurable_id.

source
meta def tactic.apply_measurable.comp_ae_measurable  :
tactic unit

Tactic to apply measurable.comp_ae_measurable when appropriate.

Applying measurable.comp_ae_measurable is not always a good idea, so we have some extra logic here to try to avoid bad cases.

source
meta def tactic.goal_is_not_measurable  :
tactic unit

We don't want the intro1 tactic to apply to a goal of the form measurable f, ae_measurable f μ or measurable_set s. This tactic tests the target to see if it matches that form.

source
meta def tactic.measurability_tactics (md : tactic.transparency := tactic.transparency.semireducible) :
list (tactic string)

List of tactics used by measurability internally. The option use_exfalso := ff is passed to the tactic apply_assumption in order to avoid loops in the presence of negated hypotheses in the context.

source
meta def tactic.interactive.measurability (bang : interactive.parse (optional (lean.parser.tk "!"))) (trace : interactive.parse (optional (lean.parser.tk "?"))) (cfg : tactic.tidy.cfg := {trace_result := bool.ff, trace_result_prefix := "Try this: ", tactics := tactic.tidy.default_tactics}) :
tactic unit

Solve goals of the form measurable f, ae_measurable f μ, ae_strongly_measurable f μ or measurable_set s. measurability? reports back the proof term it found.

source
meta def tactic.interactive.measurability'  :
tactic unit

Version of measurability for use with auto_param.

source
def tactic_doc.tactic.measurability / measurability'  :
tactic_doc_entry

measurability solves goals of the form measurable f, ae_measurable f μ, ae_strongly_measurable f μ or measurable_set s by applying lemmas tagged with the measurability user attribute.

You can also use measurability!, which applies lemmas with { md := semireducible }. The default behaviour is more conservative, and only unfolds reducible definitions when attempting to match lemmas with the goal.

measurability? reports back the proof term it found.