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.

User attribute used to mark tactics used by measurability.

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.

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.

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.

List of tactics used by measurability internally.

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

Version of measurability for use with auto_param.