# mathlib3documentation

measure_theory.tactic

# Tactics for measure theory #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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. 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.

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.

Version of measurability for use with auto_param.

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.