# mathlibdocumentation

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.

meta def measurability  :

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.

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

• measurable.comp_ae_measurable will always succeed on ae_measurable (λ x, f x) μ and can produce new goals (measurable (λ x, x), ae_measurable f μ) or (measurable f, ae_measurable (λ x, x) μ). We detect those by failing if a new goal can be closed by applying measurable_id or ae_measurable_id.

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.