Stokes' theorem

Stream: maths

[Kevin Buzzard]

Occasionally I run into people who say "what is all this fuss about getting all of an undergraduate(UG) curriculum into Lean, basically this was already done by Mizar and pretty much all of it is in Coq". I would always forcefully argue that this was not the case -- just because there is a bunch of UG maths in these systems does not mean we have a full UG curriculum. My standard counterexample was finiteness of class group of a number field, and in fact I could even twist the knife by observing that even though some of these provers have been around for 30 or 40 years, none of them even had the definition of the class group of a number field, something which was in certain cases known to Gauss.

But I see in my ArXiv daily posting today that I am now out of date -- congratulations to Anne, Sander, Ashvni and Filippo, who have proved the class group of a number field is finite in Lean. At Imperial we also teach the result about finite generation of the unit group (this is a far-reaching generalisation of the theory of the Pell equation, at least if you state precisely how many generators the unit group has), but this result certainly looks very accessible now. My other standard counterexample was insolvability of the quintic, but this is now done in Coq by Cyril and Assia and others, and people who follow the #Berkeley Lean Seminar stream will know that they're well on the way to doing this in Lean too.

So I need a new taunt, and I'm going for Stokes' theorem, in the form I learnt it in my final year UG course, which was for smooth manifolds with boundary -- the "Stokes-Cartan" or "generalized Stokes theorem" here.

How far are we from having this in Lean? And is this already done, or being worked on, in other theorem provers?

Once this is done, we are perhaps getting to the point where perhaps the union of all theorem provers really does look like it covers the vast majority of an undergraduate pure mathematics degree (of course we can then start talking about MSc's...).

[Mario Carneiro]

Complex analysis is covered in isabelle and HOL Light but I don't know how comprehensive it is; that might be another example

[Kevin Buzzard]

I am just assuming that all complex analysis is done in these HOL systems, however my impression is that their ability to work with complex manifolds is not good, so perhaps another candidate theorem is the statement that a non-constant map between two compact Riemann surfaces has a degree, a weak form of which would be the statement that there exists some positive integer d such that away from a finite set in the target, the pre-image of a point in the target is d points in the source.

[Mario Carneiro]

what undergraduate learns that though?

[Kevin Buzzard]

I learnt that in the 3rd year Riemann surfaces course

[Mario Carneiro]

I suppose riemann surfaces are covered in a complex analysis course?

[Kevin Buzzard]

@Bhavik Mehta is this still taught in Cambridge, do you know?

[Mario Carneiro]

My university didn't have anything more specialized than "complex analysis"

[Mario Carneiro]

for undergrads, at least

[Bhavik Mehta]

Yeah, Riemann surfaces are a third-year undergraduate course in Cambridge

[Kevin Buzzard]

UK universities might be more specialised, because they are catering for people who were only doing maths and two other subjects since the age of 16 and are only doing maths courses from 18 onwards. The UK UG system is more high-powered than the US system in general. On the other hand the US PhD system is much better than the UK system, where funding runs out after 3.5 years and you're expected to basically have a thesis by then. In the US I think the average is more like 5 years. In the UK you start with an advisor on day 1.

[Johan Commelin]

I saw the degree of maps between Riemann surfaces before finishing my BSc

[Heather Macbeth]

@Yury G. Kudryashov has a baby version of Stokes' theorem, not yet PR'd. (It's for boxes in $\mathbb{R}^n$.). And in Isabelle they have Green's theorem, for some kind of domain (C^1 or piecewise C^1?) in the plane.

[Heather Macbeth]

But for "proper" Stokes' theorem, on manifolds, we'll need, among other things, a fully functioning library for tensors on manifolds. At the moment we don't even have the definition of a vector bundle ... unsurprisingly, it's not easy!

[Kevin Buzzard]

Yes I'm very very well aware that it's not at all easy. This is why it's a good challenge. I know we have Patrick's formalised definition of an UG degree (which is a very precise list of things showing up in one specific degree taught in France) but if you're prepared to use the more flexible one of "whatever someone in Cambridge or Harvard or Princeton or any one of 100 other decent institutions teach in the first three or four years" (which is I think a definition that most people in maths departments would agree was a reasonable interpretation of "an undergraduate degree") then we can see that there are still a few serious challenges left. Good challenges drive the area forwards of course.

[Adam Topaz]

Heather Macbeth said:

But for "proper" Stokes' theorem, on manifolds, we'll need, among other things, a fully functioning library for tensors on manifolds. At the moment we don't even have the definition of a vector bundle ... unsurprisingly, it's not easy!

I thought there was a PR for vector bundles somewhere?

[Adam Topaz]

I remember discussing this.

[Adam Topaz]

#4658 looks like it hasn't been touched in a little while. (and it's for topological vector bundles)

[Yury G. Kudryashov]

I'm going to rewrite my Stokes theorem to require only integrability instead of continuity, then PR it.

[Eric Wieser]

#4658 looks like it has a bunch of typeclass relaxations for dual that should be cherry picked

[Kevin Buzzard]

I bet we assumed continuity in my UG course but unfortunately all the notes are in my office and we're in lockdown in the UK...

[Filippo A. E. Nuccio]

Thanks Kevin! You mention Dirichlet's Units Theorem: indeed, we thought about this as a possible future project, we mention this in the closing remarks. We will see...

[Yury G. Kudryashov]

Hi, I've finally formalized a generalized version of Stokes' theorem. Sorry @Sebastien Gouezel and @Patrick Massot, the proof is for a kind of Henstock integral. The reason of choosing this integral is that this way we get the following statement: if f : ι → (ι → ℝ) → E is a family of functions differentiable on a box [l, c] with derivatives f' i : (ι → ℝ) →L[ℝ] E, then λ x : ι → ℝ, ∑ i, f' i x is Henstock integrable on [l, c] with integral equal to the sum of integrals of f over faces of [l, u].

[Yury G. Kudryashov]

I'm going to prove that in case of [second_countable_topology E] and a Bochner integrable f, it is Henstock integrable with the same integral, then we'll have Stokes' theorem for the Bochner integral.

[Yury G. Kudryashov]

The code is in branch#stokes-new. I'll split it into PRs tonight.

[Johan Commelin]

We really need an emoji for integrals (-;

[Johan Commelin]

Ouch, has quite a double meaning if you use it like that :oops: :see_no_evil: :rofl:

[Patrick Massot]

This is great news! Hopefully this will unlock many things, especially complex analysis whose continuing absence is more and more embarassing.

[Yury G. Kudryashov]

@Kevin Buzzard @Heather Macbeth I'm sorry it took much longer than I expected.

[Yury G. Kudryashov]

Lint catches lots of missing docstrings and a few unused [fintype ι] arguments.

[Yury G. Kudryashov]

BTW, I need a name for

def name_me {ι α : Type*} (i : ι) (x : α) (f : ({i}ᶜ : set ι) → α) : ι → α :=
λ j, if h : j = i then x else f ⟨j, h⟩

or its function.update-style dependent version.

[Sebastien Gouezel]

Directly related question: for p : ι → Prop do we already have in the library a way to break ι → α as a product, i.e.,

 ({x // p x} → α) × ({x // ¬ p x} → α) ≃ (ι → α)

?

[Mario Carneiro]

I think that will exist as two separate equivs

[Mario Carneiro]

one to split (A -> C) x (B -> C) ~= (A + B -> C) and one for {x // p x} + {x // ¬ p x} ~= ι

[Mario Carneiro]

docs#equiv.sum_compl and docs#equiv.sum_arrow_equiv_prod_arrow

[Sebastien Gouezel]

Thanks!

[Eric Wieser]

As the name for Yury: function.extend_compl, and have only the dependent version?

[Chris Birkbeck]

This is great!

[Heather Macbeth]

Congratulations @Yury G. Kudryashov! It will be great to have this in mathlib.

Yury G. Kudryashov said:

I'm going to prove that in case of [second_countable_topology E] and a Bochner integrable f, it is Henstock integrable with the same integral, then we'll have Stokes' theorem for the Bochner integral.

Looking ahead, do we want a version of this theorem which applies to an arbitrary finite-dimensional real vector space (equipped with say Haar measure), generalized from your current version which applies to ι → ℝ?

Also, I wonder what the right generalization of trace/divergence is in that context. We would like the trace of a real linear map from ι → ℝ to ι → E to be an element of E (more generally, the divergence of a differentiable function from ι → ℝ to ι → E); that's how things work in Yury's current version of Stokes. We would also like the trace of a real linear map from V to V (more generally, the divergence of a differentiable function from V to V) to live in ℝ.

Mathematically, one would say: it makes sense to consider the trace of a real linear map from A to B to live in C, if B is canonically isomorphic to $A\otimes C$. But this "canonically isomorphic" is not very Lean-friendly.

[Johan Commelin]

I've been whishing for an is_tensor_product R M N P before, which should say something like: $M \otimes_R N \stackrel{\text{can.}}{\cong} P$

[Heather Macbeth]

Ah! I did think of this but wondered if it would be too baroque. Maybe it's what we need!

[Heather Macbeth]

Do you have other use cases in mind, Johan?

[Johan Commelin]

is_tensor_product R (polynomial R) A (polynomial A)

[Johan Commelin]

and things like that

[Johan Commelin]

it would be good if we can make sure that it works for both modules and algebras

[Heather Macbeth]

For that matter, I have been wondering if it would be useful to have is_dual R M N, so that the double dual of a finite-dimensional vector space can be considered to be itself.

[Johan Commelin]

But I'm not sure if that is possible. Because saying that P is canonically isomorphic (as algebra) to the M (x) N is a stronger statement than saying it is canonically isomorphic (as module).

[Heather Macbeth]

Anyway, to make your suggestion here explicit for the Stokes situation, we would have:

• is_tensor_product ℝ (ι → ℝ) E (ι → E)
• is_tensor_product ℝ V ℝ V

The former is rather similar to your polynomial example.

[Adam Topaz]

The tensor product for modules and for algebras require different things, and this class will include data.

[Adam Topaz]

This is similar to something I was asking for about (co)limits in the category theory library here:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/limits.20as.20a.20class.3F/near/247014056

[Adam Topaz]

Bhavik wasn't happy about that ;)

[Heather Macbeth]

I suppose nobody doubts the usefulness of an internal direct sum decomposition, expressing that V is canonically isomorphic to $W_1\oplus W_2$. And this is rather analogous.

[Yury G. Kudryashov]

I'm making this branch ready for review (while moving some parts to small PRs). I'm not sure what is the better way to formulate the main theorem: use ι as the index type for the whole space and {i}ᶜ as the index type for a face, or fin (n + 1) and fin n?

[Yury G. Kudryashov]

In the latter case I'll use docs#fin.insert_nth instead of coe.

[Yury G. Kudryashov]

It looks like ι is a more general solution (that's why I used it) but I tried to transfer the result to a function defined on ℝ × ℝ and this was far from convenient.

[Heather Macbeth]

I was thinking that before transferring to ℝ × ℝ, it would be nice to state a version for a general finite-dimensional vector space, equipped with a basis of the dual.

[Heather Macbeth]

Given a volume form on a finite-dimensional vector space and an element of its dual (which determines a hyperplane, i.e. pair of sides of the box), there's an induced volume form on the hyperplane. So your Stokes can be stated in this context.

[Heather Macbeth]

By volume form I just mean top-rank docs#alternating_map

[Heather Macbeth]

(but one needs to prove that such a thing induces a measure)

[Yury G. Kudryashov]

I think that we can have this (see below) now and replace the proof with a more general one later.

lemma integral_divergence_prod_of_forall_has_deriv_within_at (f : ℝ × ℝ → E × E)
  (f' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E × E) {a b : ℝ × ℝ} (hle : a ≤ b)
  (Hd : ∀ x ∈ Icc a b, has_fderiv_within_at f (f' x) (Icc a b) x)
  (Hi : integrable_on (λ x, (f' x (1, 0)).1 + (f' x (0, 1)).2) (Icc a b)) :
  ∫ x in Icc a b, (f' x (1, 0)).1 + (f' x (0, 1)).2 =
    (∫ x in a.1..b.1, (f (x, b.2)).2) - (∫ x in a.1..b.1, (f (x, a.2)).2) +
      (∫ y in a.2..b.2, (f (b.1, y)).1) - ∫ y in a.2..b.2, (f (a.1, y)).1 :=

[Yury G. Kudryashov]

It's in branch#stokes-new

[Yury G. Kudryashov]

Now I also have

lemma integral_circle_darg_of_differentiable_on {R : ℝ} (h0 : 0 ≤ R) {f : ℂ → E}
  (hd : differentiable_on ℂ f (closed_ball 0 R)) :
  ∫ (θ : ℝ) in 0..2 * π, f (R * exp (θ * I)) = (2 * π) • f 0 :=

and

lemma integral_circle_eq_zero_of_differentiable_on {R : ℝ} (h0 : 0 ≤ R) {f : ℂ → E}
  (hd : differentiable_on ℂ f (closed_ball 0 R)) :
  ∫ (θ : ℝ) in 0..2 * π, (R * exp (θ * I) * I : ℂ) • f (R * exp (θ * I)) = 0 :=

[Yury G. Kudryashov]

As you can see, these lemmas use ∫ (θ : ℝ) in 0..2 * π, to speak about integrals over the circle.

[Yury G. Kudryashov]

This fact makes them less readable.

[Yury G. Kudryashov]

Also, I want to show

lemma integral_unit_circle_div_sub_of_differentiable_on {w : ℂ} (h : abs w < 1)
  {f : ℂ → E} (hd : differentiable_on ℂ f (closed_ball (0 : ℂ) 1)) :
  ∫ (θ : ℝ) in 0..2 * π, ((exp (θ * I) * I) / (exp (θ * I) - w) : ℂ) •
    f (exp (θ * I)) = 2 • π • I • f w :=

[Yury G. Kudryashov]

The proof I have in mind is the following one. Put $R_w(z)=\frac{z+w}{\bar wz+1}$. Then apply integral_circle_darg_of_differentiable_on to f ∘ R_w.

[Chris Birkbeck]

So, just to check I understand the statements correctly, this is Cauchy's integral formula right?

[Yury G. Kudryashov]

There are two obstacles:

1. I need some facts about automorphisms of the unit disc (e.g., I need to know that R_w maps the unit disc and the unit circle to themselves).
2. The LHS will differ from the goal by a change of variables, and I'll have to prove something about its derivative.

[Yury G. Kudryashov]

I have Cauchy's integral formula for the center of a disc, and I want it for any point in the disc.

[Chris Birkbeck]

Yury G. Kudryashov said:

The proof I have in mind is the following one. Put $R_w(z)=\frac{z+w}{\bar wz+1}$. Then apply integral_circle_darg_of_differentiable_on to f ∘ R_w.

I guess this is just a Moebius transformation, but I'm not sure if that helps

[Heather Macbeth]

It'd be nice to convert

∫ (θ : ℝ) in 0..2 * π, f (R * exp (θ * I))

to an integral over the circle

R ⁻¹ ∫ (z : sphere (0:ℂ) R), f (z)

For this we need that the docs#measure_theory.measure.map of the restriction of Lebesgue measure to $[0,2\pi]$ under the exponential map is equal to Hausdorff measure on the circle. @Alex Kontorovich and I were discussing something similar the other day, but for Haar measure.

[Yury G. Kudryashov]

Do we already have a volume on the circle? Which measure is it?

[Heather Macbeth]

In analysis/fourier I use Haar measure, but I would be glad to switch over to Hausdorff at some point.

docs#circle.measure_theory.measure_space

[Heather Macbeth]

But I don't think the rotation-invariance of Hausdorff measure is obvious from what is currently in mathlib?

[Yury G. Kudryashov]

We know that isometries preserve Hausdorff measures.

[Heather Macbeth]

Ah, then I guess it is!

[Yury G. Kudryashov]

docs#isometric.hausdorff_measure_image

[Yury G. Kudryashov]

Someone should reformulate this using map.

[Yury G. Kudryashov]

But this will be an integral over a measure, not dz.

[Heather Macbeth]

Still, good enough for most purposes.

[Yury G. Kudryashov]

It's better than with exp (θ * I) but doesn't give me change of variables "for free".

[Heather Macbeth]

By the way, could you prove the mean value property for harmonic functions in n-space by a generalization of your plane argument?

[Yury G. Kudryashov]

What do you call "your plane argument"?

[Heather Macbeth]

Pick some (volume-preserving?) parametrization of a punctured (n-1)-sphere which identifies it with a (n-1)-parallelliped.

[Yury G. Kudryashov]

I don't know.

[Yury G. Kudryashov]

Can you deduce it from some sort of Stokes' theorem?

[Heather Macbeth]

Yes

[Yury G. Kudryashov]

The we should do it this way.

[Yury G. Kudryashov]

I mean, define integrals of differential forms etc.

[Heather Macbeth]

In the long term, yes, but in the short term it would be nice to have the mean value property immediately by a trick, just as for Cauchy's formula.

[Yury G. Kudryashov]

Let me say it this way: I'm not going to work on a proof by a trick here. Anyone else is welcome to do it.

[Yury G. Kudryashov]

Pushed existing code to branch#stokes-new.

[Yury G. Kudryashov]

(done)

[Kevin Buzzard]

Are we in a position do prove that weight 2 modular forms of level Gamma with no boundedness conditions at the cusps biject with Gamma-invariant holomorphic one-forms on the upper half plane? It's an equiv of complex vector spaces and the map sends $f(z)$ to $f(z)dz$.

[Yury G. Kudryashov]

We don't have Cauchy formula yet (only a particular case).

[Yury G. Kudryashov]

@Heather Macbeth Since you've already worked on this, could you please prove some formulas for change of variables in integrals over circles in $\mathbb C$?

[Heather Macbeth]

What formulas did you have in mind?

[Yury G. Kudryashov]

I want to say that the integral $\int_{S^1} f(z)dz$ does not depend on the choice of a parametrization.

[Yury G. Kudryashov]

You can assume that $f$ is differentiable, if you want.

[Yury G. Kudryashov]

And the change of variables is a Möbius transformation (see above).

[Yury G. Kudryashov]

OMG, the diff is already 5K lines...
/me is going to make some smaller PRs to reduce the diff.

[Yury G. Kudryashov]

BTW, do we have a way to create a diffeomorph between two spheres from a local diffeomorphism between the ambient spaces?

[Heather Macbeth]

Good question. You can use docs#times_cont_mdiff.cod_restrict_sphere and docs#times_cont_mdiff_coe_sphere combined to create an times_cont_mdiff map in each direction, then check the pair are inverse to each other.

[Heather Macbeth]

See docs#times_cont_mdiff_neg_sphere for an example of creating the times_cont_mdiff map.

[Yury G. Kudryashov]

I think about introducing a definition for $\int_{S^1} f(z)\,dz$.

[Yury G. Kudryashov]

And we can use, e.g., ∮ as notation.

[Yaël Dillies]

Yury G. Kudryashov said:

As you can see, these lemmas use ∫ (θ : ℝ) in 0..2 * π, to speak about integrals over the circle.

Maybe this is time we depart from usual mathematical practice and use τ in place of π.

[Yury G. Kudryashov]

I prefer to use π. And the man problem is that I need a specific parametrization z(t) of the circle an explicit dz/dt in the integral.

[Yury G. Kudryashov]

Progress report: I have Cauchy integral formula for any point inside a circle modulo a formula for the integral ∫ dz/(z-w).

[Yury G. Kudryashov]

#9405 #9406 #9409 #9410 are some dependencies I need for this formula.

[Scott Morrison]

All on the queue now!

[Yury G. Kudryashov]

I'm going to prove that exp_map_circle sends volume to volume.

[Yury G. Kudryashov]

With current definition λ x, x * I, there is a multiplier 2π. @Heather Macbeth what do you think about changing the definition of exp_map_circle to λ x, x * 2 * π * I?

[Yury G. Kudryashov]

In this case the kernel of exp_map_circle_hom will be range (coe : int → real) and exp_map_circle will map restrict volume (Ioc 0 1) to volume.

[Yury G. Kudryashov]

cons: def must be moved after the definition of π.

[Yury G. Kudryashov]

OTOH, your exp_map_circle agrees with complex.arg.

[Yury G. Kudryashov]

Probably, we should have both.

[Heather Macbeth]

I would prefer the existing definition because it is a local isometry. But I would be happy to change docs#haar_circle to give a total measure of 2 * π for the circle, rather than 1.

[Yury G. Kudryashov]

I like to have a probability measure.

[Yury G. Kudryashov]

BTW, with the current definition of the circle, exp_map_circle is not a local isometry.

[Yury G. Kudryashov]

If you want to have a local isometry, you should define circle as $\mathbb R/\mathbb Z$.

[Yury G. Kudryashov]

I mean, currently the distance between $1$ and $-1$ is $2$, not $\pi$.

[Heather Macbeth]

Oh, I am using the intrinsic/Riemannian metric

[Yury G. Kudryashov]

But the current metric_space structure on circle uses a different metric.

[Heather Macbeth]

That's true -- I didn't mean that it was literally a local isometry in Lean, just that that's my reason for preferring the current definition.

[Yury G. Kudryashov]

About the total measure of haar_circle: what's more convenient for integration?

[Yury G. Kudryashov]

I mean, did you have to add $2\pi$ because of the current definition, or you would have to add $1/2\pi$ if we had total measure = $2\pi$?

[Yury G. Kudryashov]

AFAIR, in Fourier series it's more convenient to have total measure = 1.

[Heather Macbeth]

That's right, it was more convenient in analysis/fourier to have total measure 1. But I was being a bit lazy when I did that -- I think we should have a strong presupposition that subsets of R^n get Hausdorff measure/submanifold measure

[Heather Macbeth]

So I'd be happy to go through the Fourier file and insert $2\pi$'s everywhere

[Heather Macbeth]

For your main goal, can you follow these steps? I think they are all desirable to have individually:

1. The quotient map from $\mathbb{R}$ to $\mathbb{R}/T\mathbb{Z}$ sends volume to volume (or more precisely, sends restriction-of-volume-to-[0,T] to volume)
2. There is an isomorphism of length spaces between $\mathbb{R}/2\pi\mathbb{Z}$ and the circle
3. An isomorphism of length spaces induces an isomorphism of Hausdorff measure

[Yury G. Kudryashov]

I'm going to stick to Haar measure for now.

[Yury G. Kudryashov]

Otherwise I'll do as you suggest.

[Heather Macbeth]

I see, in that case something like

1. The quotient map from $\mathbb{R}$ to $\mathbb{R}/T\mathbb{Z}$ sends volume to volume (or more precisely, sends restriction-of-volume-to-[0,T] to volume)
2. There is an isomorphism of topological groups between $\mathbb{R}/2\pi\mathbb{Z}$ and the circle

[Heather Macbeth]

(Note that there is an open PR of one of my students containing point 2: #8559)

[Yury G. Kudryashov]

#8559 does not define a homeomorph.

[Yury G. Kudryashov]

I'm going to add lemmas about complex.angle, then merge master once #8559 is ready.

[Yury G. Kudryashov]

Hi, I moved some code from #8903 to #9496. I think that analysis/box_integral folder in #9496 is ready for review. For historical reasons, it depends on #9422 but I can drop this dependency if needed.

[Yury G. Kudryashov]

If I can somehow make reviewing these 4K lines of code easier, then tell me, please.

[Scott Morrison]

box/basic.lean and box/box_induction.lean look great. :-)

[Yury G. Kudryashov]

Rebased (squashing history) to drop dependency on #9422, fixed linter.

[Patrick Massot]

Wow, this is a 4000 lines PR!

[Yury G. Kudryashov]

And I don't think that it makes sense to split it :(

[Patrick Massot]

I hope our exotic integration theory expert will have a lot of courage ( Sébastien :looking: )

[Yury G. Kudryashov]

I remember that @Sebastien Gouezel was definitely not enthusiastic about adding Henstock integration to mathlib.

[Patrick Massot]

That's why he is our expert: he knows about Henstock integration

[Yury G. Kudryashov]

And I don't know if anyone used this version of Henstock integral in $\mathbb R^n$.

[Yury G. Kudryashov]

Most of the code is the same for all box integrals, so you only need to know about Riemann integral to review it.

[Yury G. Kudryashov]

Actually, if we have a student who wants to learn more about Riemann integral (and related definitions), then reading this PR may be a good way to do it.

[Yury G. Kudryashov]

IMHO, Henstock integral is exotic only because Riemann integral was defined much earlier. The definition is almost the same, and the proofs are either the same, or simpler.

[Sebastien Gouezel]

I'm perfectly happy to add Henstock integration to mathlib, especially with the nice applications towards complex analysis. My point was that the "main" integration theory in mathlib should remain Lebesgue integration, though, because it makes sense in a much more general setting, and has in general nicer properties.

[Yury G. Kudryashov]

Ping here

[Sebastien Gouezel]

Working on it :-)

[Yury G. Kudryashov]

Thanks a lot for a review!

[Yury G. Kudryashov]

Going through your comments, I've noticed that all of my part (box ι) are better expressed as with_bot (box ι). I'll try to change to with_bot. If it doesn't cause a large diff, then I'll push it.

[Sebastien Gouezel]

Push anyway, I think that's a good idea.

[Yury G. Kudryashov]

#9630 is a new dependency that is about finsets, not integrals, so you don't have to be Sebastien to review it.