mathlib3 documentation

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.

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.