Integral as continuous linear map on bounded continuous fns?

Stream: mathlib4

[Luigi Massacci]

Hello,

I recently proved that Radon measures give distributions, and I'm passing by the statement that integrating wrt a finite measure is a continuous linear map on bounded continuous functions, which I have formalized like this:

import Mathlib

open MeasureTheory Module

variable (𝕜 E F: Type*) [NormedField 𝕜]
variable [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E]
variable [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
        [SecondCountableTopology F] [MeasurableSpace F] [BorelSpace F]

variable (μ : Measure E)

open BoundedContinuousFunction

theorem isBDL_integral_BCF [IsFiniteMeasure μ] :
    IsBoundedLinearMap 𝕜 ((∫ x, · x ∂μ) : (E →ᵇ F) → F) := by
  constructor
  · constructor
    · refine fun f g ↦ integral_add (f.integrable μ) (g.integrable μ)
    · refine fun c f ↦ integral_smul c f
  · by_cases h : μ = 0
    · refine ⟨1, zero_lt_one, fun f ↦ by aesop⟩
    · use (measureUnivNNReal μ)
      constructor
      · exact MeasureTheory.measureUnivNNReal_pos h
      · refine fun f ↦ le_trans (f.norm_integral_le_mul_norm _) le_rfl

theorem continuous_integral_BCF [IsFiniteMeasure μ]:
    Continuous ((∫ x, · x ∂μ) : (E →ᵇ F) → F) := by
  apply IsBoundedLinearMap.continuous (isBDL_integral_BCF ℝ E F μ)

I'm wondering whether it makes sense to have these two lemmas on their own in say Mathlib.MeasureTheory.Integral.BoundedContinuousFunction, possibly changing some of the hypotheses / the way the map is written (but I'm not sure what would be the good way) or if I should keep it in my file and when I get around to PR-ing the whole thing we'll work it out.

Pinging @Michael Rothgang since you volunteered to comment, but I'd welcome feedback from anyone.

[Sébastien Gouëzel]

Instead of showing that the integral satisfies the predicate IsBoundedLinearMap, could you define a version of the integral as a continuous linear map from E →ᵇ F to F? This amounts to essentially the same mathematical content, but in practice it's more in line with the way we use continuous linear maps.

[Luigi Massacci]

You mean something like this?

import Mathlib

open MeasureTheory Module

variable (𝕜 E F: Type*) [NormedField 𝕜]
variable [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E]
variable [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
        [SecondCountableTopology F] [MeasurableSpace F] [BorelSpace F]

variable (μ : Measure E)

open BoundedContinuousFunction

noncomputable def integralFiniteMeasure [IsFiniteMeasure μ] : (E →ᵇ F) →L[𝕜] F where
  toFun := (∫ x, · x ∂μ)
  map_add' := fun f g ↦ integral_add (f.integrable μ) (g.integrable μ)
  map_smul' := fun c f ↦ integral_smul c f
  cont := by
    apply @IsBoundedLinearMap.continuous ℝ
    refine ⟨⟨?_, ?_⟩ ,  ?_⟩
    ·refine  fun f g ↦ integral_add (f.integrable μ) (g.integrable μ)
    · refine fun c f ↦ integral_smul c f
    by_cases h : μ = 0
    · refine ⟨1, zero_lt_one, fun f ↦ by aesop⟩
    · use (measureUnivNNReal μ)
      constructor
      · exact MeasureTheory.measureUnivNNReal_pos h
      · refine fun f ↦ le_trans (f.norm_integral_le_mul_norm _) le_rfl

[Sébastien Gouëzel]

Yes, something like that. You could golf it using docs#LinearMap.mkContinuous. No need to separate the zero measure, I guess.

[Luigi Massacci]

I was about to ask if there was a neat way to avoid the repetition. Thank you!

[Michael Rothgang]

#29511

[Luigi Massacci]

There is now also #29748 that does the same wrt a LocallyIntegrable function and a fixed compact. I don't think there's a terrific urgency to merge them since they'll make more sense once I start PR-ing the distributions proper in the following days, but I'm always happy with reviews. I'm not sure with how to name things in this last one in particular.

[Michael Rothgang]

Thanks! Can you add the missing docstrings, please?

[Luigi Massacci]

Oopsie :sweat_smile:

[Kalle Kytölä]

I just wanted to point out that docs#MeasureTheory.FiniteMeasure.toWeakDualBCNN does something quite related --- however with the (significant) difference of using the Lebesgue integral instead of Bochner integral and correspondingly assuming nonnegativity of the functions. (Due to the difference I think doing the argument separately in both cases is reasonable.)

But it seems worth considering whether to add the continuous dependence of your linear map on the measure (w.r.t. the topology defined in the above file).

[Luigi Massacci]

I did see that when I started working on this (I think I even mentioned it to Patrick) but it seems a bit of a deviation from my immediate needs. It can be done separably anyway?