[Merged by Bors] - feat: continuity of primitives for parametric integrals

[grunweg]

From the sphere eversion project and generalised by sgouezel.

This is used in the sphere eversion project to show that averaging of loops is continuous (which will be PRed to mathlib at a later point).

Co-authored by: @fpvandoorn (who write this code originally, I believe)

---

[grunweg]

@lecopivo I'm trying out fun_prop on this lemma - I have two questions for you as the fun_prop expert:

• I'm tagging two lemmas with fun_prop; are these fine to tag?
• is the TODO within reach of fun_prop (i.e., replacing the "from ..." with "by fun_prop"? (If not, I'll just remove it.)

[lecopivo]

Integral is higher order function i.e. having a function as an argument. fun_prop theorems about higher order functions should be stated in "compositional form". So I would not mark continuous_parametric_primitive_of_continuous and for generality I would reformulate continuous_parametric_intervalIntegral_of_continuous as

theorem continuous_parametric_intervalIntegral_of_continuous
    (hF : Continuous fun p : X × ℝ ↦ F p.1 p.2) 
    {a b : X → ℝ} (ha : Continuous a) (hb : continuous b) :
    Continuous fun x ↦ ∫ t in a x..b x, F x t ∂μ

In the short term, making that proof working is not within the reach of fun_prop as it would require significant modification to the code which decomposes function into a composition of two functions. Unfortunately, it does not work as expected when it comes to higher order functions.

The best I can offer is this proof

theorem continuous_parametric_intervalIntegral_of_continuous {a₀ : ℝ}
    (hF : Continuous fun p : X × ℝ ↦ F p.1 p.2) {s : X → ℝ} (hs : Continuous s) :
    Continuous fun x ↦ ∫ t in a₀..s x, F x t ∂μ :=
  Continuous.comp (g:=(fun p : X × ℝ ↦ ∫ t in a₀..p.2, F p.1 t ∂μ)) (f:=fun x ↦ (x, s x))
    (by fun_prop) (by fun_prop)

The way fun_prop works now it tries to prove the continuity by decomposing the function as

    (fun x ↦ ∫ t in a₀..s x, F x t ∂μ)
    =
    (fun (f,b) => intervalIntegral f a₀ b μ) ∘ (fun x => (fun t => F x t, s x))

which is not useful.

[lecopivo]

At least I will try to think of a linter that would warn you when you tag theorem like continuous_parametric_primitive_of_continuous that you should formulate it in 'compositional form'.

The issue is that for some higher order functions stating theorems in 'uncurried form' is fine. For example, Finset.sum

open BigOperators 
@[fun_prop]
theorem sum_continuous {ι} [Fintype ι] :
   Continuous fun (f : ι → ℝ) => ∑ i, f i := ...

@[fun_prop]
theorem sum_continuous' {ι} [Fintype ι] (f : X → ι → ℝ) (hf : Continuous f) :
   Continuous fun x => ∑ i, f x i := by fun_prop

fun_prop can already prove sum_continuous' from sum_continuous.

Therefore the linter can't simple check if you are working with higher order function or not.

[grunweg]

I will get to this PR eventually, but have other higher-priority things to do right now. If you're reading this, help jumping in and fixing the above is welcome.

[loefflerd]

I left some detailed comments on the first file (Stieltjes). I've also suggested adding some explanatory comments to the big proof in DominatedConvergence yet – I haven't yet read the proof, but I'd prefer to read it with explanations than without!

[loefflerd]

A couple of afterthoughts:

• There seems to be some inconsistency of naming about what to call things like 𝓝[≥] (0 : ℝ) – I've seen both nhdsWithin_Ici and nhds_right in the library. But I think nhdsWithin_ge is not yet in use in the library, so I suggest renaming these lemmas to one of the two existing names, to avoid adding a third synonym.)
• Might it be simpler to inline the proof of tendsto_measure_Icc_nhdsWithin_gt inside tendsto_measure_Icc_nhdsWithin_ge rather than having it as a separate lemma? It's easy to go back using nhdsWithin_mono if anyone does specifically need the statement for 𝓝[>].

[grunweg]

Thanks a lot, @sgouezel, for rebasing this! This was on my list, to be done after my PhD thesis (i.e. quite soon).

[sgouezel]

@semorrison. Kim, you requested my review on this one, must I have written most code in the current version. I would be happy to merge it, but it would probably be more reasonable if someone else reviewed it...

[fpvandoorn]

I did another review

bors d+

[mathlib-bors]

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[grunweg]

Thanks for the review! Since mathlib builds, let's bors this.
bors merge

[mathlib-bors]

👎 Rejected by label

[grunweg]

The CI error was in curl - not related to this code.
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style