gcongr and notation

Stream: mathlib4

[Kalle Kytölä]

This is not urgent at all, but something I think should be solved at some point.

Currently we cannot tag the lemma lintegral_mono with the gcongr-attribute, although that should be an extremely natural use case:

import Mathlib.MeasureTheory.Integral.Lebesgue

open MeasureTheory
open scoped ENNReal

attribute [gcongr] lintegral_mono
    -- @[gcongr] attribute only applies to lemmas proving
    -- x₁ ~₁ x₁' → ... xₙ ~ₙ xₙ' → f x₁ ... xₙ ∼ f x₁' ... xₙ',
    -- got ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
    -- ⦃f g : α → ℝ≥0∞⦄, f ≤ g → ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ

@Anatole Dedecker showed me a solution, below. If I'm not mistaken, it indicates that the only problem is that the integral notation prevents tagging the lemma with the attribute.

import Mathlib.MeasureTheory.Integral.Lebesgue

open MeasureTheory
open scoped ENNReal

-- This would solve it!

lemma MeasureTheory.lintegral_mono'' {α : Type} {m : MeasurableSpace α}
    {μ : MeasureTheory.Measure α} {f g : α → ℝ≥0∞} (hfg : f ≤ g) :
    lintegral μ f ≤ lintegral μ g :=
  lintegral_mono hfg

attribute [gcongr] MeasureTheory.lintegral_mono'' -- works

#check lintegral_mono
#check lintegral_mono'' -- same except from the use of notation

I assume we don't want to be adding duplicate lemmas that avoid notation, and that we don't want this issue to hold back the full power of the great gcongr tactic.

Does someone understand how difficult it would be to solve this issue? (Again, not urgent, just asking!)

[Jireh Loreaux]

docs#MeasureTheory.lintegral_mono

[Jireh Loreaux]

From what I understand of the gcongr tactic, this shouldn't be an issue at all, which makes me suspect that there is a separate problem in the above example. Have you managed to use the double prime version successfully (as opposed to just tagging it)? If you can, does it work with or without notation, or both?

[Kalle Kytölä]

I think I have... (But maybe the type ascription was particularly explicit or something.) Let me dig up an example.

[Kalle Kytölä]

import Mathlib.MeasureTheory.Integral.Bochner
import Mathlib.Topology.ContinuousFunction.Bounded

open MeasureTheory
open scoped ENNReal BoundedContinuousFunction

-- This would solve it!

lemma MeasureTheory.lintegral_mono'' {α : Type} {m : MeasurableSpace α}
    {μ : MeasureTheory.Measure α} {f g : α → ℝ≥0∞} (hfg : f ≤ g) :
    lintegral μ f ≤ lintegral μ g :=
  lintegral_mono hfg

attribute [gcongr] MeasureTheory.lintegral_mono''

variable {X : Type*} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X]

variable {E : Type*} [NormedAddCommGroup E] [TopologicalSpace.SecondCountableTopology E]
variable [MeasurableSpace E] [BorelSpace E]

lemma BoundedContinuousFunction.integrable (μ : Measure X) [IsFiniteMeasure μ] (f : X →ᵇ E) :
    Integrable f μ := by
  refine ⟨f.continuous.measurable.aestronglyMeasurable, (hasFiniteIntegral_def _ _).mp ?_⟩
  calc  ∫⁻ x, ‖f x‖₊ ∂μ
    _ ≤ ∫⁻ _, ‖f‖₊ ∂μ                       := ?_
    _ = ‖f‖₊ * (μ Set.univ)                 := by rw [lintegral_const]
    _ < ∞                                   := ENNReal.mul_lt_top
                                                ENNReal.coe_ne_top (measure_ne_top μ Set.univ)
  · gcongr
    exact fun x ↦ ENNReal.coe_le_coe.mpr (nnnorm_coe_le_nnnorm f x)

[Jireh Loreaux]

@Heather Macbeth the above seems like a bug in the tooling for gcongr to correctly identify lemmas that have the required form in the presence of notation. It's weird to me because notation is just a macro, so I would have expected it to see right through it. But you probably know more.

[Kalle Kytölä]

Sorry, the above example had a missing import and a missing open scoped. Fixed now.

[Kyle Miller]

I think this isn't a problem of notation per se -- there's a difference between ∫⁻ (a : α), f a ∂μ and lintegral μ f in that the former is lintegral μ (fun a => f a).

I'm not sure how much it makes sense, but something that'd fix the problem is if gcongr were to be able to eta-unexpand terms in the conclusion of a theorem. (For example, turning fun a => f a into f.)

[Heather Macbeth]

I think it's not the notation per se, but the difference between f and fun x ↦ f x. The integral notation uses the latter, gcongr requires the former. At least, this was the situation for sums, see docs#GCongr.sum_le_sum

[Kalle Kytölä]

Sorry, my example still had a missing variable and was not working. Now it in fact fails... I thought I had it working before... I'll try to make a #mwe or tell if @Jireh Loreaux is right and only the tagging works.

(It indeed works in a different file, but not in my minimal example above...)

[Heather Macbeth]

It has been on my to-do list to go through the library and write variants like docs#GCongr.sum_le_sum for tsum, lintegral, integral, ..., but I haven't got around to it yet. Someone else is very welcome to do it, or to implement Kyle's idea for a cleverer fix!

[Jireh Loreaux]

Ah, got it. The function is eta-expanded in notation.

[Kalle Kytölä]

For some reason I'm struggling to create a #mwe. I only have a working example which is not minimal and a minimal example which is not working.

But since clever people above understood the issue, maybe it doesn't matter that my minimal example didn't work --- the possibility to tag perhaps already indicates an issue in some way.

For now, I'm happy to know that solutions exist.

[Frédéric Dupuis]

I also had the same issue with big-O notation a while back (see here).