feat(MeasureTheory): aesop rules for strong measurability + measurability? tactic (#5427)

This PR adds aesop tags to a few lemmas pertaining to strong measurability, allowing to prove e.g. `StronglyMeasurable Real.log` using the `measurability` tactic.

It also implements `measurability?` via `aesop?`.



Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

Author: dupuisf

Mathlib/MeasureTheory/Function/SpecialFunctions/Inner.lean

@@ -22,14 +22,26 @@ variable [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
 
 local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y
 
-@[measurability]
+@[aesop safe 20 apply (rule_sets [Measurable])]
 theorem Measurable.inner {_ : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
     [TopologicalSpace.SecondCountableTopology E] {f g : α → E} (hf : Measurable f)
     (hg : Measurable g) : Measurable fun t => ⟪f t, g t⟫ :=
   Continuous.measurable2 continuous_inner hf hg
 #align measurable.inner Measurable.inner
 
 @[measurability]
+theorem Measurable.const_inner {_ : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
+    [TopologicalSpace.SecondCountableTopology E] {c : E} {f : α → E} (hf : Measurable f) :
+    Measurable fun t => ⟪c, f t⟫ :=
+  Measurable.inner measurable_const hf
+
+@[measurability]
+theorem Measurable.inner_const {_ : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
+    [TopologicalSpace.SecondCountableTopology E] {c : E} {f : α → E} (hf : Measurable f) :
+    Measurable fun t => ⟪f t, c⟫ :=
+  Measurable.inner hf measurable_const
+
+@[aesop safe 20 apply (rule_sets [Measurable])]
 theorem AEMeasurable.inner {m : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
     [TopologicalSpace.SecondCountableTopology E] {μ : MeasureTheory.Measure α} {f g : α → E}
     (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun x => ⟪f x, g x⟫) μ := by
@@ -38,3 +50,19 @@ theorem AEMeasurable.inner {m : MeasurableSpace α} [MeasurableSpace E] [OpensMe
   dsimp only
   congr
 #align ae_measurable.inner AEMeasurable.inner
+
+set_option linter.unusedVariables false in
+@[measurability]
+theorem AEMeasurable.const_inner {m : MeasurableSpace α} [MeasurableSpace E]
+    [OpensMeasurableSpace E] [TopologicalSpace.SecondCountableTopology E]
+    {μ : MeasureTheory.Measure α} {f : α → E} {c : E} (hf : AEMeasurable f μ) :
+    AEMeasurable (fun x => ⟪c, f x⟫) μ :=
+  AEMeasurable.inner aemeasurable_const hf
+
+set_option linter.unusedVariables false in
+@[measurability]
+theorem AEMeasurable.inner_const {m : MeasurableSpace α} [MeasurableSpace E]
+    [OpensMeasurableSpace E] [TopologicalSpace.SecondCountableTopology E]
+    {μ : MeasureTheory.Measure α} {f : α → E} {c : E} (hf : AEMeasurable f μ) :
+    AEMeasurable (fun x => ⟪f x, c⟫) μ :=
+  AEMeasurable.inner hf aemeasurable_const

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -133,28 +133,28 @@ theorem AEMeasurable.mul_const [MeasurableMul M] (hf : AEMeasurable f μ) (c : M
 #align ae_measurable.mul_const AEMeasurable.mul_const
 #align ae_measurable.add_const AEMeasurable.add_const
 
-@[to_additive (attr := measurability)]
+@[to_additive (attr := aesop safe 20 apply (rule_sets [Measurable]))]
 theorem Measurable.mul' [MeasurableMul₂ M] (hf : Measurable f) (hg : Measurable g) :
     Measurable (f * g) :=
   measurable_mul.comp (hf.prod_mk hg)
 #align measurable.mul' Measurable.mul'
 #align measurable.add' Measurable.add'
 
-@[to_additive (attr := measurability)]
+@[to_additive (attr := aesop safe 20 apply (rule_sets [Measurable]))]
 theorem Measurable.mul [MeasurableMul₂ M] (hf : Measurable f) (hg : Measurable g) :
     Measurable fun a => f a * g a :=
   measurable_mul.comp (hf.prod_mk hg)
 #align measurable.mul Measurable.mul
 #align measurable.add Measurable.add
 
-@[to_additive (attr := measurability)]
+@[to_additive (attr := aesop safe 20 apply (rule_sets [Measurable]))]
 theorem AEMeasurable.mul' [MeasurableMul₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
     AEMeasurable (f * g) μ :=
   measurable_mul.comp_aemeasurable (hf.prod_mk hg)
 #align ae_measurable.mul' AEMeasurable.mul'
 #align ae_measurable.add' AEMeasurable.add'
 
-@[to_additive (attr := measurability)]
+@[to_additive (attr := aesop safe 20 apply (rule_sets [Measurable]))]
 theorem AEMeasurable.mul [MeasurableMul₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
     AEMeasurable (fun a => f a * g a) μ :=
   measurable_mul.comp_aemeasurable (hf.prod_mk hg)
@@ -216,12 +216,12 @@ section Pow
 variable {β γ α : Type _} [MeasurableSpace β] [MeasurableSpace γ] [Pow β γ] [MeasurablePow β γ]
   {m : MeasurableSpace α} {μ : Measure α} {f : α → β} {g : α → γ}
 
-@[measurability]
+@[aesop safe 20 apply (rule_sets [Measurable])]
 theorem Measurable.pow (hf : Measurable f) (hg : Measurable g) : Measurable fun x => f x ^ g x :=
   measurable_pow.comp (hf.prod_mk hg)
 #align measurable.pow Measurable.pow
 
-@[measurability]
+@[aesop safe 20 apply (rule_sets [Measurable])]
 theorem AEMeasurable.pow (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
     AEMeasurable (fun x => f x ^ g x) μ :=
   measurable_pow.comp_aemeasurable (hf.prod_mk hg)
@@ -326,28 +326,28 @@ theorem AEMeasurable.div_const [MeasurableDiv G] (hf : AEMeasurable f μ) (c : G
 #align ae_measurable.div_const AEMeasurable.div_const
 #align ae_measurable.sub_const AEMeasurable.sub_const
 
-@[to_additive (attr := measurability)]
+@[to_additive (attr := aesop safe 20 apply (rule_sets [Measurable]))]
 theorem Measurable.div' [MeasurableDiv₂ G] (hf : Measurable f) (hg : Measurable g) :
     Measurable (f / g) :=
   measurable_div.comp (hf.prod_mk hg)
 #align measurable.div' Measurable.div'
 #align measurable.sub' Measurable.sub'
 
-@[to_additive (attr := measurability)]
+@[to_additive (attr := aesop safe 20 apply (rule_sets [Measurable]))]
 theorem Measurable.div [MeasurableDiv₂ G] (hf : Measurable f) (hg : Measurable g) :
     Measurable fun a => f a / g a :=
   measurable_div.comp (hf.prod_mk hg)
 #align measurable.div Measurable.div
 #align measurable.sub Measurable.sub
 
-@[to_additive (attr := measurability)]
+@[to_additive (attr := aesop safe 20 apply (rule_sets [Measurable]))]
 theorem AEMeasurable.div' [MeasurableDiv₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
     AEMeasurable (f / g) μ :=
   measurable_div.comp_aemeasurable (hf.prod_mk hg)
 #align ae_measurable.div' AEMeasurable.div'
 #align ae_measurable.sub' AEMeasurable.sub'
 
-@[to_additive (attr := measurability)]
+@[to_additive (attr := aesop safe 20 apply (rule_sets [Measurable]))]
 theorem AEMeasurable.div [MeasurableDiv₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
     AEMeasurable (fun a => f a / g a) μ :=
   measurable_div.comp_aemeasurable (hf.prod_mk hg)
@@ -607,14 +607,14 @@ section SMul
 variable {M β α : Type _} [MeasurableSpace M] [MeasurableSpace β] [_root_.SMul M β]
   {m : MeasurableSpace α} {f : α → M} {g : α → β}
 
-@[to_additive (attr := measurability)]
+@[to_additive (attr := aesop safe 20 apply (rule_sets [Measurable]))]
 theorem Measurable.smul [MeasurableSMul₂ M β] (hf : Measurable f) (hg : Measurable g) :
     Measurable fun x => f x • g x :=
   measurable_smul.comp (hf.prod_mk hg)
 #align measurable.smul Measurable.smul
 #align measurable.vadd Measurable.vadd
 
-@[to_additive (attr := measurability)]
+@[to_additive (attr := aesop safe 20 apply (rule_sets [Measurable]))]
 theorem AEMeasurable.smul [MeasurableSMul₂ M β] {μ : Measure α} (hf : AEMeasurable f μ)
     (hg : AEMeasurable g μ) : AEMeasurable (fun x => f x • g x) μ :=
   MeasurableSMul₂.measurable_smul.comp_aemeasurable (hf.prod_mk hg)

Mathlib/MeasureTheory/Group/Arithmetic.lean

@@ -842,18 +842,18 @@ theorem measurable_pi_iff {g : α → ∀ a, π a} : Measurable g ↔ ∀ a, Mea
     MeasurableSpace.comap_comp, Function.comp, iSup_le_iff]
 #align measurable_pi_iff measurable_pi_iff
 
-@[measurability]
+@[aesop safe 100 apply (rule_sets [Measurable])]
 theorem measurable_pi_apply (a : δ) : Measurable fun f : ∀ a, π a => f a :=
   measurable_pi_iff.1 measurable_id a
 #align measurable_pi_apply measurable_pi_apply
 
-@[measurability]
+@[aesop safe 100 apply (rule_sets [Measurable])]
 theorem Measurable.eval {a : δ} {g : α → ∀ a, π a} (hg : Measurable g) :
     Measurable fun x => g x a :=
   (measurable_pi_apply a).comp hg
 #align measurable.eval Measurable.eval
 
-@[measurability]
+@[aesop safe 100 apply (rule_sets [Measurable])]
 theorem measurable_pi_lambda (f : α → ∀ a, π a) (hf : ∀ a, Measurable fun c => f c a) :
     Measurable f :=
   measurable_pi_iff.mpr hf

Mathlib/MeasureTheory/MeasurableSpace.lean

@@ -557,7 +557,7 @@ protected theorem Measurable.comp {_ : MeasurableSpace α} {_ : MeasurableSpace
 #align measurable.comp Measurable.comp
 
 -- This is needed due to reducibility issues with the `measurability` tactic.
-@[measurability]
+@[aesop safe 50 (rule_sets [Measurable])]
 protected theorem Measurable.comp' {_ : MeasurableSpace α} {_ : MeasurableSpace β}
     {_ : MeasurableSpace γ} {g : β → γ} {f : α → β} (hg : Measurable g) (hf : Measurable f) :
     Measurable (fun x => g (f x)) := Measurable.comp hg hf

Mathlib/MeasureTheory/MeasurableSpaceDef.lean

@@ -24,13 +24,21 @@ macro "measurability" : attr =>
 
 /--
 The tactic `measurability` solves goals of the form `Measurable f`, `AEMeasurable f`,
-`AEStronglyMeasurable f μ`, or `MeasurableSet s` by applying lemmas tagged with the
-`measurability` user attribute. -/
+`StronglyMeasurable f`, `AEStronglyMeasurable f μ`, or `MeasurableSet s` by applying lemmas tagged
+with the `measurability` user attribute. -/
 macro "measurability" (config)? : tactic =>
   `(tactic| aesop (options := { terminal := true }) (rule_sets [$(Lean.mkIdent `Measurable):ident]))
 
--- Todo: implement `measurability?`, `measurability!` and `measurability!?` and add configuration,
+/--
+The tactic `measurability?` solves goals of the form `Measurable f`, `AEMeasurable f`,
+`StronglyMeasurable f`, `AEStronglyMeasurable f μ`, or `MeasurableSet s` by applying lemmas tagged
+with the `measurability` user attribute, and suggests a faster proof script that can be substituted
+for the tactic call in case of success. -/
+macro "measurability?" (config)? : tactic =>
+  `(tactic| aesop? (options := { terminal := true })
+    (rule_sets [$(Lean.mkIdent `Measurable):ident]))
+
+-- Todo: implement `measurability!` and `measurability!?` and add configuration,
 -- original syntax was (same for the missing `measurability` variants):
 syntax (name := measurability!) "measurability!" (config)? : tactic
-syntax (name := measurability?) "measurability?" (config)? : tactic
 syntax (name := measurability!?) "measurability!?" (config)? : tactic

Mathlib/Tactic/Measurability.lean

@@ -5,6 +5,13 @@ Authors: Rémy Degenne
 -/
 import Mathlib.MeasureTheory.Tactic
 import Mathlib.MeasureTheory.MeasurableSpace
+import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
+import Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
+import Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
+import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
+
+open scoped BigOperators
+open MeasureTheory TopologicalSpace
 
 variable {α β : Type _} [MeasurableSpace α] [MeasurableSpace β]
   {f g : α → β} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {μ ν : MeasureTheory.Measure α}
@@ -37,7 +44,23 @@ example {ι} [Encodable ι] {S : ι → Set α} (hs : ∀ i, MeasurableSet (S i)
 example (hf : Measurable f) (hs₁ : MeasurableSet s₁) (ht₂ : MeasurableSet t₂) :
     MeasurableSet ((f ⁻¹' t₂) ∩ s₁) := by measurability
 
-/- Porting note: TODO Uncomment these
+-- Strong measurability
+section strong_measurability
+
+variable [TopologicalSpace β] [PseudoMetrizableSpace β] [BorelSpace β]
+
+-- Test the use of apply_assumption to get (h i) from a hypothesis (h : ∀ i, ...).
+
+example  {F : ℕ → α → β} (hF : ∀ i, StronglyMeasurable (F i)) : Measurable (F 0) := by
+  measurability
+
+example [Zero β] {F : ℕ → α → β} (hF : ∀ i, AEFinStronglyMeasurable (F i) μ) :
+    AEMeasurable (F 0) μ := by measurability
+
+example {ι} [Encodable ι] {S₁ S₂ : ι → Set α} (hS₁ : ∀ i, MeasurableSet (S₁ i))
+    (hS₂ : ∀ i, MeasurableSet (S₂ i)) : MeasurableSet (⋃ i, (S₁ i) ∪ (S₂ i)) := by measurability
+
+end strong_measurability
 
 /-- `ℝ` is a good test case because it verifies many assumptions, hence many lemmas apply and we
 are more likely to detect a bad lemma. In a previous version of the tactic, `measurability` got
@@ -56,10 +79,14 @@ example [Add β] [MeasurableAdd₂ β] (hf : Measurable f) (hg : AEMeasurable g
     AEMeasurable (fun x => f x + g x) μ := by measurability
 
 example [Div β] [MeasurableDiv₂ β] (hf : Measurable f) (hg : Measurable g)
-    (ht : MeasurableSet t₂): MeasurableSet ((fun x => f x / g x) ⁻¹' t₂) := by measurability
+    (ht : MeasurableSet t₂) : MeasurableSet ((fun x => f x / g x) ⁻¹' t₂) := by measurability
 
 example [AddCommMonoid β] [MeasurableAdd₂ β] {s : Finset ℕ} {F : ℕ → α → β}
-    (hF : ∀ i, AEMeasurable (F i) μ) : AEMeasurable (∑ i in s, (λ x, F (i+1) x + F i x)) μ := by
+    (hF : ∀ i, Measurable (F i)) : Measurable (∑ i in s, (fun x => F (i+1) x + F i x)) := by
+  measurability
+
+example [AddCommMonoid β] [MeasurableAdd₂ β] {s : Finset ℕ} {F : ℕ → α → β}
+    (hF : ∀ i, AEMeasurable (F i) μ) : AEMeasurable (∑ i in s, (fun x => F (i+1) x + F i x)) μ := by
   measurability
 
 -- even with many assumptions, the tactic is not trapped by a bad lemma
@@ -69,8 +96,25 @@ example [TopologicalSpace α] [BorelSpace α] [NormedAddCommGroup β] [BorelSpac
   measurability
 
 example : Measurable (fun x : ℝ => Real.exp (2 * inner x 3)) := by measurability
--/
+
+example : StronglyMeasurable (fun x : ℝ => Real.exp (2 * inner x 3)) := by measurability
+
+example {γ : MeasureTheory.Measure ℝ} :
+  AEMeasurable (fun x : ℝ => Real.exp (2 * inner x 3)) γ := by measurability
+
+example {γ : MeasureTheory.Measure ℝ} :
+  AEStronglyMeasurable (fun x : ℝ => Real.exp (2 * inner x 3)) γ := by measurability
+
+example {γ : MeasureTheory.Measure ℝ} [SigmaFinite γ] :
+  FinStronglyMeasurable (fun x : ℝ => Real.exp (2 * inner x 3)) γ := by measurability
+
+example {γ : MeasureTheory.Measure ℝ} [SigmaFinite γ] :
+  AEFinStronglyMeasurable (fun x : ℝ => Real.exp (2 * inner x 3)) γ := by measurability
 
 /-- An older version of the tactic failed in the presence of a negated hypothesis due to an
 internal call to `apply_assumption`. -/
 example {ι : Type _} (i k : ι) (hik : i ≠ k) : Measurable (id : α → α) := by measurability
+
+--This search problem loops (StronglyMeasurable -> Measurable -> StronglyMeasurable) but fails
+--quickly nevertheless.
+--example (f : ℝ → ℝ) : StronglyMeasurable f := by measurability