Tasks and claims

Stream: Brownian motion

[Etienne Marion]

I am very happy that this project is happening! So if I understand correctly I can just claim a lemma from the blueprint here? If so I'll try lemma 1.10.

[Rémy Degenne]

Yes that's the idea! Thanks for joining the project! The numbering might change as we add lemmas to the blueprint as needed, so it's better to specify the lemma name as well as the number. That's covInnerBilin_map

[Rémy Degenne]

Feel free to claim larger parts (several lemmas at once) as well if you are experienced and have time to do it.

[Markus Himmel]

I'd like to claim lemmas 5.12 to 5.15 (edist_chainingSequence lemmas).

[David Ledvinka]

Markus Himmel said:

I'd like to claim lemmas 5.12 to 5.15 (edist_chainingSequence lemmas).

FYI I was taking a look at that section and as far as I can tell there is a discrepancy between the blueprint and the lean file where a bunch of the lemmas and definitions in the blueprint assume the covering set is contained in $A$ (but the lean statements don't).

[Etienne Marion]

I'd like to claim Lemma 1.12 covMatrix_map.

[Rémy Degenne]

David Ledvinka said:

Markus Himmel said:

I'd like to claim lemmas 5.12 to 5.15 (edist_chainingSequence lemmas).

FYI I was taking a look at that section and as far as I can tell there is a discrepancy between the blueprint and the lean file where a bunch of the lemmas and definitions in the blueprint assume the covering set is contained in $A$ (but the lean statements don't).

Add the assumption to the Lean statements wherever it is needed!

[Jonas Bayer]

I'd like to claim Lemma 2.4 (lem:Indistinguishable.Modification). I've already started to play around with this and it seems that to show that $\{ ω | X _t (ω) = Y_t (ω) \}$ is measurable one needs that the diagonal is measurable. Which assumptions should we use to formalize this?

Or am I being stupid overlooking something?

[David Ledvinka]

Im going to work on the lemmas in LogSizeBallSequence.lean

[Jonas Bayer]

Actually, I'd like to extend the claim to include the other lemmas from chapter 2.

[Markus Himmel]

I'll work on the two scale_change lemmas (5.35 and 5.36).

[Rémy Degenne]

Jonas Bayer said:

I'd like to claim Lemma 2.4 (lem:Indistinguishable.Modification). I've already started to play around with this and it seems that to show that $\{ ω | X _t (ω) = Y_t (ω) \}$ is measurable one needs that the diagonal is measurable. Which assumptions should we use to formalize this?

In my mind Indistinguishable.Modification was simply a filter_upwards application. Why do you need measurability of that set?

[Rémy Degenne]

import Mathlib
open MeasureTheory
example {T Ω E : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    {X Y : T → Ω → E} (h : ∀ᵐ ω ∂P, ∀ t, X t ω = Y t ω) :
    ∀ t, ∀ᵐ ω ∂P, X t ω = Y t ω := by
  intro t
  filter_upwards [h] with ω hω using hω t

[Rémy Degenne]

@Jonas Bayer there is currently no Lean file (and no formalized definitions or statements) for that chapter 2. Please create a new file.

[Rémy Degenne]

Or I could do that now and formalize a few statements (with sorry proofs) if you prefer

[Jonas Bayer]

I didn't know about filter_upwards, thanks! (I'm fairly new to the Measure theory API)

[Jonas Bayer]

If that's fine I'd also like to formalise the statements myself and then we can iterate if something is not very idiomatic for his API.

[MohanadAhmed]

Hi Everyone,
I am hoping to contribute but I realized I need to learn a bit about the MeasureTheory API. Is there a document which outlines its architecture or some brief intro to the main concepts around which the API is centered?

[Jérémy Scanvic]

Fantastic project! I'll start working on Lemma 3.3 / centralMoment_two_mul_gaussianReal.

[Markus Himmel]

I'll have a look at the Kolmogorov condition distance bounds (lemmas 5.33 and 5.34).

[Rémy Degenne]

Thanks everyone for all the work you are already putting into the project! I made the mistake of launching the project just before a week-end and I have little time to keep up with the progress right now, but I'll post an update tomorrow about what was already done and what is currently claimed.

[Rémy Degenne]

@MohanadAhmed there is a short chapter in Mathematics in Lean: https://leanprover-community.github.io/mathematics_in_lean/C13_Integration_and_Measure_Theory.html
Note that this chapter talks about the Bochner integral but we will mostly use the Lebesgue integral.

Apart from that I guess you can start proving something, and look at the docs (or leansearch, loogle, etc.) whenever you are missing a def?

[Etienne Marion]

I'll have a go at lemmas 3.14 to 3.16, about gaussian characteristic function.

[Markus Himmel]

I'll work on lintegral_sup_rpow_edist_cover_of_dist_le now (lemma 5.37)
Edit: next lintegral_sup_rpow_edist_succ (lemma 5.39)

[Etienne Marion]

Is it fine to create an auxiliary file containing general API lemmas to be upstreamed to Mathlib later?

[Rémy Degenne]

Yes, please create one or more files for those. Ideally files with lemmas grouped by topics (like an ENNReal.lean file for generic ENNReal lemmas, etc.).

[Notification Bot]

26 messages were moved here from #Brownian motion > Status of the project by Rémy Degenne.

[Rémy Degenne]

Etienne Marion said:

I'll have a go at lemmas 3.14 to 3.16, about gaussian characteristic function.

One unresolved question in my mind about that part of the blueprint is whether working with covInnerBilin would be better than covMatrix. The blueprint uses matrices but it might be easier to use the bilinear map formulation. Feel free to switch to whatever is more convenient.

[Etienne Marion]

Rémy Degenne said:

Etienne Marion said:

I'll have a go at lemmas 3.14 to 3.16, about gaussian characteristic function.

One unresolved question in my mind about that part of the blueprint is whether working with covInnerBilin would be better than covMatrix. The blueprint uses matrices but it might be easier to use the bilinear map formulation. Feel free to switch to whatever is more convenient.

I've been wondering about that, because it certainly is easier to manipulate the bilinear form directly as it does not require to use all the decomposition in bases machinery. So if you say it's ok then i'll probably switch to bilinear forms indeed.

[Etienne Marion]

In fact I just realized that we don't seem to have a definition for positive semi-definite bilinear form. I think I'll write an API for those because bilinear forms do seem nicer to me.

[Peter Pfaffelhuber]

Thanks, Rémy for setting all this up, and for all the contributions already! I would like to work on isProjectiveMeasureFamily_gaussianProjectiveFamily (Lemma 4.9).
I have a realted question: There does not seem to be the notion of a (linear) _projection_ in mathlib, at least I cannot find one, which I find hard to believe. Am I missing something here?

[Rémy Degenne]

In the context of that lemma, Set.restrict should be the way to expressed the $\pi_{IJ}$ map described in the blueprint. Is that function what you meant by projection?

[Etienne Marion]

If you deal with finsets I'd rather recommend Finset.restrict because otherwise you can encounter some strange behaviour. If you are looking for idempotent linear maps, there is LinearMap.IsProj.

[Rémy Degenne]

The proof in the blueprint needs that function packaged as a ContinuousLinearMap (because that interacts well with Gaussians). I'm not sure that we have it with that type.

[Etienne Marion]

Do you mean for Finset.restrict or Set.restrict? Or both? For the former I'm pretty sure we don't, for the latter I don't think either but I'm not sure.

[Peter Pfaffelhuber]

Ah, thanks! I see there is Pi.continuous_restrict showing continuity as well as LinearMap.restrict showing linearity. Hope I can combine them to a ContinuousLinearMap.

[Etienne Marion]

I'll take on lemmas 3.19 (integral_eval_pi) to 3.25 ("The covariance matrix of the standard Gaussian measure is the identity matrix.").

[Rémy Degenne]

Here is a sample of open tasks that are not claimed yet. Anyone can pick one!

• integral_sup_dist_le_sum_rpow An application of Minkowski's inequality
• internalCoveringNumber_eq_one_of_diam_le The covering number is 1 if the radius is larger than the diameter of the set
• L_lt_top A particular (slightly ugly) sum is finite
• borel_eq_iSup_comap_eval Two sigma-algebras (product sigma algebra and Borel sigma-algebra for the continuous functions with the compact-open topology) are equal. No detailed proof in the blueprint, but a link to a stackexchange question.
• integral_div_dist_le_sum_integral_dist_le Upper bound on the expectation of a ratio, obtained by cutting the space into pieces depending on the value of the denominator

They are many other lemmas that are ready to be formalized below integral_sup_dist_le_sum_rpow, in the Kolmogorov-Chentsov proof.

[Markus Himmel]

I'll do integral_sup_dist_le_sum_rpow. @Rémy Degenne, is it acceptable to take $p \ge 1$ as a hypothesis to be able to apply Minkowski? It feels a lot stronger than the $p>0$ from the previous lemmas, but if I understand correctly, the final application will have $p$ and $q$ natural anyway.

[Rémy Degenne]

Thanks for raising the issue with the blueprint proof (and for the PR!). I'd like to keep the $p > 0$ hypothesis. I looked at the original paper, and I don't see how they deal with the possibility of $p < 1$ there.
For $p < 1$ we could apply ENNReal.lintegral_Lp_add_le_of_le_one, which is similar but loses a $2^{1/p-1}$ factor. That turns into a factor 2 in the final inequality, which would need to be propagated everywhere but is probably not important. See the PR https://github.com/RemyDegenne/brownian-motion/pull/57

[Markus Himmel]

Sorry if I'm missing something obvious here, but do we get a suitable version of docs#ENNReal.lintegral_Lp_add_le_of_le_one for an arbitrary finite sum? The simple induction proof I used to derive the Finset.sum version from the add version for $p \ge 1$ no longer works because we would get an additional factor of $2^{1/p - 1}$ in every step of the induction. Looking at the proof, the factor $2$ seems to come from docs#ENNReal.rpow_add_le_mul_rpow_add_rpow, and if we use something like docs#ENNReal.rpow_arith_mean_le_arith_mean_rpow, then the factor in the final result will be $k - m$ instead of $2$.

[Rémy Degenne]

Ah sorry you're right, my fix is not right either. I did that too quickly while trying to prepare dinner at the same time. I don't know then. I'll need to look at it more carefully. It corresponds to a step in the proof of lemma 6.2 in the paper

[Rémy Degenne]

The solution might just be an alternative proof in the case $p < 1$ (not to this lemma only, but to the next few lemmas as well) based on Real.rpow_add_le_add_rpow. It's getting late here but I'll investigate that tomorrow.

[Rémy Degenne]

Yes that seems to work. In the end you can assume $p \ge 1$ in the lemma you were proving and in the next two (which means that your current PR is already fine), and I am adding versions of these 3 lemmas that take a slightly different route for $p < 1$.

[Markus Himmel]

Awesome, thanks for the quick fix!

[Rémy Degenne]

By the way you were right when you wrote that in the current project the only application is for p a natural number with $p \ge 1$. We don't really need such a general Kolmogorov-Chentsov theorem for building the Brownian motion on $\mathbb{R}_+$, but we thought it would be nice to use the opportunity of that project to get a more general result.

[Lorenzo Luccioli]

Alessio Rondelli (not yet on zulip) and I claim internalCoveringNumber_eq_one_of_diam_le.

[Markus Himmel]

Claiming lintegral_sup_rpow_edist_le_sum_rpow_of_le_one.

[Peter Pfaffelhuber]

I am claiming isGaussian_multivariateGaussian, since I need to get used to the API of IsGaussian.

[Rémy Degenne]

The API of IsGaussian is very young and is missing important results. In particular in Mathlib there is API for the general Banach space case but no specializations to Hilbert spaces. Etienne added lemmas towards that in the project (In Gaussian/Gaussian.lean, notably). Don't hesitate to add supporting lemmas as the need arises.

[Rémy Degenne]

I claim lintegral_sup_rpow_edist_le_sum_of_le_one(5.46)

[Rémy Degenne]

and lintegral_sup_rpow_edist_le_sum

[Rémy Degenne]

and lintegral_sup_rpow_edist_le_of_minimal_cover_of_le_one

[Rémy Degenne]

and lintegral_sup_rpow_edist_le_of_minimal_cover

[Jérémy Scanvic]

I'm claiming L_lt_top

[Rémy Degenne]

There is a small issue in the blueprint statement of integral_sup_rpow_dist_cover_rescale. There is a condition $\delta \le 4\varepsilon_0$ missing, which will require some adaptation at the point where the lemma is used. I am currently fixing the blueprint.

[Etienne Marion]

Is variance_dual_stdGaussian in the file MultivariateGaussian supposed to be used somewhere? I proved it because it was in the file but it does not appear in the blueprint nor anywhere else in the code. Should I add it to the blueprint?

[Rémy Degenne]

I thought it would be useful for isGaussian_stdGaussian. That variance appears in the goal where I left a sorry in isGaussian_stdGaussian. But perhaps you already proved that one by another mean?

[Rémy Degenne]

As for the blueprint, I'd add it if you use it for something.

[Etienne Marion]

Ok I see, in the blueprint there was the lemma giving the charFun of stdGaussian before (but it wasn't in the lean file), so I proved it too and then for isGaussian_stdGaussian I simply used isGaussian_iff_gaussian_charFun (I introduced a ContinuousBilinForm version of the inner product). I didn't realize that your comment before the sorry referred to variance_dual_stdGaussian.
In the end I still proved variance_dual_stdGaussian, and to do so I wrote a few lemmas to prove that random variables defined on different probability spaces were independent once they were seen as random variables on the product space, which could be interesting for Mathlib. But I think the route using charFun instead of charFunDual is easier.

[Rémy Degenne]

Well it sounds like you proved many interesting lemmas, and that's great! Sorry for the confusion.

[Rémy Degenne]

Rémy Degenne said:

There is a small issue in the blueprint statement of integral_sup_rpow_dist_cover_rescale. There is a condition $\delta \le 4\varepsilon_0$ missing, which will require some adaptation at the point where the lemma is used. I am currently fixing the blueprint.

I pushed the blueprint changes.

[Etienne Marion]

I claim lemma 5.7 about the covering of the unit interval.

[David Ledvinka]

I claim integral_div_dist_le_sum_integral_dist_le

[Markus Himmel]

Claiming integral_sup_rpow_dist_cover_rescale

[Notification Bot]

17 messages were moved from this topic to #Brownian motion > Suprema and subtypes by Rémy Degenne.

[Markus Himmel]

Claiming integral_sup_rpow_edist_le_of_minimal_cover_two.

[Rémy Degenne]

I claim isGaussian_gaussianProjectiveFamily, which is apparently a lemma in the code but does not correspond to anything in the blueprint. Well I prove that.

[Rémy Degenne]

@Peter Pfaffelhuber in the PR https://github.com/RemyDegenne/brownian-motion/pull/71 I changed the definition of gaussianProjectiveFamily to use a map by a continuous linear equivalence instead of merely a measurable equivalence, since that interacts better with Gaussians.
That's relevant for the task isProjectiveMeasureFamily_gaussianProjectiveFamily that you claimed.

[Rémy Degenne]

I claim finite_set_bound_of_edist_le

[Rémy Degenne]

and finite_set_bound_of_edist_le_of_le_diam'

[David Ledvinka]

I claim lintegral_sup_rpow_edist_le_of_minimal_cover_two

[Markus Himmel]

David Ledvinka said:

I claim lintegral_sup_rpow_edist_le_of_minimal_cover_two

@David Ledvinka I have already claimed this! See my message from a few days ago.

Markus Himmel said:

Claiming integral_sup_rpow_edist_le_of_minimal_cover_two.

[David Ledvinka]

Oops my apologies somehow I saw your claim before that and totally missed your recent one. No worries!

[Rémy Degenne]

I think the current unfinished claims are those:

• Jérémy Scanvic: L_lt_top
• Markus Himmel: integral_sup_rpow_dist_cover_rescale, integral_sup_rpow_edist_le_of_minimal_cover_two
• Peter Pfaffelhuber: isProjectiveMeasureFamily_gaussianProjectiveFamily

[Rémy Degenne]

I claim integral_id_multivariateGaussian

[Peter Pfaffelhuber]

Question, given that all the characteristic functions are now available. Don't you think it would be beneficial to show how moments can be computed from the chatacteristic function using derivatives?

[Rémy Degenne]

Yes, that would be generally useful.

[Rémy Degenne]

Rémy Degenne said:

I claim integral_id_multivariateGaussian

I'm also claiming the covariance and characteristic function of the multivariate Gaussian.

[Peter Pfaffelhuber]

Would there be any harm to define multvariateGaussian on a general Fintype rather than on Fin d?

noncomputable
def multivariateGaussian' {ι : Type*} [Fintype ι] [DecidableEq ι] (μ : EuclideanSpace ℝ ι)
    (S : Matrix ι ι ℝ) (hS : S.PosSemidef) : Measure (EuclideanSpace ℝ ι) :=
  (stdGaussian (EuclideanSpace ℝ ι)).map (fun x ↦ μ + toEuclideanCLM (𝕜 := ℝ) hS.sqrt x)

That way we would not need gaussianProjectiveFamilyAux, because the gaussianProjectiveFamily can be defined as a multivariateGaussian, I think.

[Etienne Marion]

I personally think it should be defined for an arbitrary fintype.

[Rémy Degenne]

Peter Pfaffelhuber said:

Would there be any harm to define multvariateGaussian on a general Fintype rather than on Fin d?

noncomputable
def multivariateGaussian' {ι : Type*} [Fintype ι] [DecidableEq ι] (μ : EuclideanSpace ℝ ι)
    (S : Matrix ι ι ℝ) (hS : S.PosSemidef) : Measure (EuclideanSpace ℝ ι) :=
  (stdGaussian (EuclideanSpace ℝ ι)).map (fun x ↦ μ + toEuclideanCLM (𝕜 := ℝ) hS.sqrt x)

That way we would not need gaussianProjectiveFamilyAux, because the gaussianProjectiveFamily can be defined as a multivariateGaussian, I think.

That would still be a measure on a EuclideanSpace, and gaussianProjectiveFamily is a family of measures on product types: Measure (I → ℝ)

[Rémy Degenne]

Etienne Marion said:

I personally think it should be defined for an arbitrary fintype.

I agree. We will need the squared root of a bilinear form to write a good def. I only found the squared root of a matrix.

[Rémy Degenne]

Oh sorry I misread what Etienne wrote. I was reacting to what I imagined to be "it should be defined for an arbitrary finite dimensional inner product space".

[Rémy Degenne]

I made the change from Fin d to ι in https://github.com/RemyDegenne/brownian-motion/pull/87

[Peter Pfaffelhuber]

Rémy Degenne schrieb:

Oh sorry I misread what Etienne wrote. I was reacting to what I imagined to be "it should be defined for an arbitrary finite dimensional inner product space".

Not sure this is feasible. You have to worry about existence of such an object. I think you have to use show existence on some Euclidean Space, and map the measure from there.

[Etienne Marion]

Rémy Degenne said:

Oh sorry I misread what Etienne wrote. I was reacting to what I imagined to be "it should be defined for an arbitrary finite dimensional inner product space".

This should not be too complicated either, we already have the links between matrices and continuous bilinear forms related to PosSemidef so defining the square root is straight forward.

[Rémy Degenne]

@Markus Himmel perhaps you want to claim integral_sup_rpow_edist_le_of_minimal_cover_two_of_le_one as well? It has a lot in common with integral_sup_rpow_edist_le_of_minimal_cover_two that you just proved.

[Markus Himmel]

Thanks, but I won't have much time in the next two weeks, so I won't claim any additional tasks right now.

[Rémy Degenne]

Ok, no problem. You proved a lot of lemmas from chapter 5 already! Thanks!

Your work on the other lemma will simplify the task for the person who claims this one.

[Rémy Degenne]

I added more details to the end of the blueprint, and wrote enough Lean statements to have an actual definition for the Brownian motion, instead of the sorry that was there previously. So more tasks are available over there.
The blueprint on the website will reflect the changes in around 1 hour.

[Rémy Degenne]

I claim integral_sup_rpow_edist_le_of_minimal_cover_two_of_le_one

[Rémy Degenne]

I claim lintegral_sup_cover_eq_of_lt_iInf_dist

[Etienne Marion]

If nobody has claimed it I'll try lemma 3.32 IsGaussianProcess.modification.

[David Ledvinka]

I will claim finite_kolmogorov_chentsov

[David Ledvinka]

This theorem assumes that the entire set has bounded internal covering number whereas the theorem it relies on assumes the finite subset has bounded internal covering number. I took a look at the reference paper and as far as I can tell they seem to omit this technicality. At the top of page 1479 they "assume" the covering number bound assumption (1) also applies to the subset. Of course I think you can easily prove that with that assumption you can choose a C uniform over subsets (2 times the previous C passing through the external covering number). However I think the current formal statements need to be reworked a bit. (Unless I am missing something)

[David Ledvinka]

To be specific I think HasBoundedInternalCoveringNumber (.univ : Set T) c d implies HasBoundedInternalCoveringNumber J (2 * c) d for J : Set T

[Rémy Degenne]

Yes good catch. Internal covering numbers are not monotone with respect to the set, but if we accept to pay a factor two it's fine (exercise 4.2.10 in the first edition of https://www.math.uci.edu/~rvershyn/papers/HDP-book/HDP-book.html; can't find it in the second edition). That might give a $2^d$ rather than a 2 though? It's still fine.

[David Ledvinka]

Oh yes $2 ^ d$ sorry (forgot to distribute the power in the proof in my head). This is not a problem overall but I think it is possibly a little more of a pain for refactoring.

[Rémy Degenne]

I'm making a blueprint PR to add the missing covering number lemmas.

[Rémy Degenne]

https://github.com/RemyDegenne/brownian-motion/pull/97
It has the new covering number lemmas, but it's still a draft because I want to also fix the constants everywhere. That means also changing the definition of L. @Jérémy Scanvic that will impact the lemma L_lt_top for which you have a draft (it will change some constants, but not the structure of L, so that should not be too bad).

[Rémy Degenne]

Changing the definition of L was not a big refactor, since we use its value in two lemmas only, and use it as a black box after that. I'm merging the PR in a few minutes, when CI is done.

[Etienne Marion]

I claim 6.3 (map_sub_preBrownian) and 6.4 (isKolmogorovProcess_preBrownian).

[Rémy Degenne]

Current claims:

• Jérémy Scanvic: L_lt_top
• Peter Pfaffelhuber: isProjectiveMeasureFamily_gaussianProjectiveFamily
• David Ledvinka: finite_kolmogorov_chentsov
• Etienne Marion: map_sub_preBrownian and isKolmogorovProcess_preBrownian

[Rémy Degenne]

Etienne Marion said:

I claim 6.3 (map_sub_preBrownian) and 6.4 (isKolmogorovProcess_preBrownian).

For map_sub_preBrownian, you'll probably need describe the sum of two jointly gaussian random variables, using docs#ProbabilityTheory.covariance

[Rémy Degenne]

I claim 5.70, finite_set_bound_of_dist_le_of_diam_le

[Rémy Degenne]

and finite_set_bound_of_dist_le_of_le_diam

[Rémy Degenne]

I claim internalCoveringNumber_subset_le and hasBoundedInternalCoveringNumber_subset

[Rémy Degenne]

On the Kolmogorov-Chentsov side, several of our dark green nodes in the graph still depend on sorry, because of two lemmas that are not reflected by the blueprint: exists_finset_card_eq_internalCoveringNumber and exists_finset_card_eq_packingNumber, in the Continuity/CoveringNumber file.

The quantity internalCoveringNumber is defined as an infimum of values in ENat, and exists_finset_card_eq_internalCoveringNumber states that the infimum is attained. exists_finset_card_eq_packingNumber is similar, for paking numbers and a supremum.

So that's one more task someone could claim.

[Etienne Marion]

Etienne Marion said:

I claim 6.3 (map_sub_preBrownian) and 6.4 (isKolmogorovProcess_preBrownian).

I claim 6.7 to 6.9 as well (isHolderWith_brownian -> law of B_t).

[Rémy Degenne]

Rémy Degenne said:

On the Kolmogorov-Chentsov side, several of our dark green nodes in the graph still depend on sorry, because of two lemmas that are not reflected by the blueprint: exists_finset_card_eq_internalCoveringNumber and exists_finset_card_eq_packingNumber, in the Continuity/CoveringNumber file.

The quantity internalCoveringNumber is defined as an infimum of values in ENat, and exists_finset_card_eq_internalCoveringNumber states that the infimum is attained. exists_finset_card_eq_packingNumber is similar, for paking numbers and a supremum.

So that's one more task someone could claim.

I did those. I really wanted the other results to be sorry-free :)

[Rémy Degenne]

With PR https://github.com/RemyDegenne/brownian-motion/pull/103, finite_kolmogorov_chentsov is sorry-free. We are getting close to the end of the project!

[Rémy Degenne]

On the Gaussian side, many lemmas that are green in the blueprint still depend on sorry but that's due to placeholder sorry that refer to things that are fully proved in Mathlib PRs.

[Etienne Marion]

Regarding aemeasurable_brownian_apply, I know that a continuous process can be written as a pointwise limit of measurable processes and is therefore measurable. But in the lean file it comes before continuous_brownian. Is there another (maybe easier to formalize) proof?

[Rémy Degenne]

The order in the file does not mean anything. I listed some properties there without thinking about the proofs (and as you can see the blueprint for that part is lacking).

[Rémy Degenne]

Actually the (a.e.-)measurability should be added to the conclusion of the four exists_modification... theorems: they are supposed to state that there exists a process (with a measurability condition) that is a modification and has additional properties.

[Etienne Marion]

Do you know if it’s possible to ensure true measurability? If not, my feeling is that it’s better to have BM to be measurable rather than a-e measurable, even if we only get almost sure continuity.

[Rémy Degenne]

Yes, since we start from a measurable process (preBrownian) we will be able to get a measurable and continuous process (not just a.e).

[Rémy Degenne]

I claim 5.80, the first theorem in the chain of results about existence of Hölder modifications.

[Etienne Marion]

Nice! Indeed I see how you can get it from the construction. So instead of proving aemeasurable_brownian I can prove that brownian.uncurry is measurable with respect to the product sigma-algebra.

[David Ledvinka]

I claim countable_kolmogorov_chentsov

[Rémy Degenne]

We will need a lemma like Dense.uniformContinuous_extend, but with uniformContinuous replaced with HolderWith

[Etienne Marion]

I'll have a look

[Rémy Degenne]

I think that the fact that MemHolder for exponent $b$ implies MemHolder for exponent $a$ with $0 < a < b$ is also missing from Mathlib (and will be needed).

[Etienne Marion]

Isn’t this rather that if you are a and b Hölder and a <= c <= b then you are also c Hölder?

[Rémy Degenne]

I forgot to mention an important assumption without which I think the result I want is false: the domain of the function is bounded.

[Etienne Marion]

I claim 6.12 (ContinuousMap.borel_eq_iSup_comap_eval)

[David Ledvinka]

Probably won't be able to work on this again until Monday but I am wondering what the status of whats left is. isCoverWithBoundedCoveringNumber_Ico_nnreal is partially done, are the sorrys unclaimed? Is there any sorrys in the lean not reflected in the blueprint or gaps in the blueprint that haven't fully been worked out? (and if you guys have it all worked out I can work on the "bonus" lemmas instead)

[Etienne Marion]

I claim 5.13 (volume_le_of_isCover) and 5.14 (exists_finset_card_eq_internalCoveringNumber).

[Etienne Marion]

I also did 5.15 (le_volume_of_isSeparated). I claim 5.16 to 5.20.

[Rémy Degenne]

@David Ledvinka isCoverWithBoundedCoveringNumber_Ico_nnreal is unclaimed, and together with internalCoveringNumber_smul and internalCoveringNumber_Ico_zero_one_le_one_div that I introduced when doing a partial proof is as far as I can tell the only unclaimed lemma remaining on the path to the definition of the Brownian motion.
The proof of internalCoveringNumber_Ico_zero_one_le_one_div should be very similar to the lemma internalCoveringNumber_Icc_zero_one_le_one_div proved by Etienne: the differences are Ico vs Icc and NNReal vs Real. Or it could be proved with the volume tools that Etienne is adding.

The claims are:

• @Rémy Degenne: the two remaining Hölder modification lemmas. One of them is partially done in https://github.com/RemyDegenne/brownian-motion/pull/114.
• @Peter Pfaffelhuber: isProjectiveMeasureFamily_gaussianProjectiveFamily
• @Jérémy Scanvic: L_lt_top. In progress at https://github.com/RemyDegenne/brownian-motion/pull/66
• @Etienne Marion: the lemmas relating volume and covering numbers. In progress at https://github.com/RemyDegenne/brownian-motion/pull/116

[Rémy Degenne]

Update: the only two remaining lemmas on the path to the Brownian motion definition are isCoverWithBoundedCoveringNumber_Ico_nnreal (unclaimed) and L_lt_top (claimed by Jérémy).

[David Ledvinka]

I will claim isCoverWithBoundedCoveringNumber_Ico_nnreal

[Jérémy Scanvic]

I'm not sure I'm going to be able to finish proving L_lt_top. I couldn't quite find my way through the existing mathlib lemma and I won't have much time to dig into it deeper in the next few weeks. If anyone wants to have a go at it feel free to do so!

[David Ledvinka]

I will unclaim isCoverWithBoundedCoveringNumber_Ico_nnreal then and claim L_lt_top

[Rémy Degenne]

I claim isCoverWithBoundedCoveringNumber_Ico_nnreal

[Rémy Degenne]

Done and merged.

[Rémy Degenne]

David Ledvinka said:

I will unclaim isCoverWithBoundedCoveringNumber_Ico_nnreal then and claim L_lt_top

As in Jérémy's draft PR, you'll need to add a hypothesis EMetric.diam (Set.univ : Set T) ≠ ∞ that is currently missing from the statement. That hypothesis can be proved with HasBoundedInternalCoveringNumber.diam_lt_top at the point where we use the lemma.

[Etienne Marion]

I claim 6.12, independence of Brownian increments.

[Rémy Degenne]

The main goal of the project is attained, but there are still a couple of things that could be done about the current code. Of course we could also think about extensions (prove more properties of the Brownian, define other related objects...) but for now I'll list a few things about the code we already have:

• the whole point of the measurability condition on pairs in the Kolmogorov process definition is to avoid a separability assumption on $E$. We managed to do that for most of the proof, but for the 4 final results about the existence of Hölder continuous modifications I gave up and added a SecondCountableTopology E assumption. It would be nice to remove it and deal with the measurability proofs that will break in exists_modification_holder_aux' (in the KolmogorovChentsov file). The blueprint does not contain any details about that, and the paper we are following states that the measurability "can be shown by standard arguments". Done.
• In the proof of that same lemma, I use convergence in measure, but I can't use the Mathlib definition because in Mathlib it uses dist, while we work in a EMetricSpace with edist. Perhaps we should refactor the Mathlib def? Done.
• In Mathlib there is HolderWith and HolderOnWith, but there is only MemHolder and no MemHolderOn. The conclusion of our exists_modification_holder_iSup would be naturally written with the missing MemHolderOn
• We have a lemma that gives the moment of order $2n$ of a Gaussian on $\mathbb{R}$. For completeness it would be nice to have the moment of order $2n+1$ (which is zero).
• Etienne used MeasurePreserving to state that some random variable has a specified law, because it was easier to use than a condition about Measure.map (because of measurability?). The downside is that it is very obscure: when I read "measure preserving" I don't see easily that it's just giving a law. What do we do about that? How do we best talk about the laws of random variables? Done.
• Our multivariate Gaussian is defined with a covariance matrix, which requires a basis. Do we want a definition that uses a continuous bilinear form?
• Can we prove that our Wiener measure is Gaussian? (when restricted to an interval, perhaps?)
• We are missing docstrings on several definitions, and many lemmas have weird names.

If you think of something else, please mention it below!

And there is also the most important task: PR to Mathlib.

[Etienne Marion]

About measurePreserving, I introduced a predicate HasLaw in my PR about increments (not yet pushed though) which is the same but only requires aemeasurable instead of measurable, which I think is more suited to probability. The idea is to have a framework that is closer to what we do in paper maths, in particular avoid proving measurability all the time. I won’t have much time to work on it this week-end but it should be up next week.

[David Ledvinka]

I like the idea of moving towards something like HasLaw and using type classes for properties of the law. I suggested something like this in #25602 (but didn't end up implementing it). Notice that with the current approach I had to add the more general IndepFun.map_mul_eq_map_mconv_map₀' as well as IndepFun.map_mul_eq_map_mconv_map₀ because it would be annoying to pass a proof of the pushforward of the law being finite each time you use it. The reason you have to use finite measure here is because Sigma Finite is not preserved by push-forward (but sigma finiteness of the push-forward is all you need). Thus for example we could have a typeclass SigmaFiniteLaw (X P) and then prove in particular if P is a finite measure then its always an instance (hopefully all the type class inference works here). Then IndepFun.hasLaw_mul and IndepFun.hasLaw_fun_mul could be generalized to SigmaFiniteLaw

[David Ledvinka]

If we adopt an approach like this more widely its probably also worth thinking about how to integrate it with Kernels and conditional probability. Should we also have HasConditionaLaw (similar to HasLaw but with a kernel instead of a measure) or is there a way to have one definition for both that isnt too messy when you just want to use measures?

[Etienne Marion]

We will probably need two definitions, but we can link the definition for measures to the one for kernels so that results proved for kernels can be used to easily get the analog for measures.

[David Ledvinka]

I realized that with your HasLaw predicate you don't actually need separate type classes for properties of the law like I suggested above since you can just use the typeclasses for the law μ (which I think is evidence that this predicate is a good idea). I submitted a suggestion to your HasLaw PR that implements the above suggested generalization but without the need for a separate type class.

[Peter Pfaffelhuber]

I have a question on preBrownian in the BrownianMotion.lean. Isn't this usually called the _canonical process_? (See e.g. Definition 14.6 in the Klenke book). In particular, I do not see anything particular _Brownian_ about this definition.

[Rémy Degenne]

It's indeed the canonical process. It's called pre-Brownian here because on the particular probability space that we consider it has all the properties of the Brownian except for the continuity.

[Peter Pfaffelhuber]

Ok, true. As you say this is only true on the probability space gaussianLimit. Shouldn't we call is canonicalProcess (with more general index set and state space)? For example, this is an obvious generalization:

lemma hasLaw_canonicalProcess {P : Measure (ℝ≥0 → ℝ)} : HasLaw (fun ω ↦ (preBrownian· ω)) P P where
  aemeasurable := (measurable_pi_lambda _ measurable_preBrownian).aemeasurable
  map_eq := Measure.map_id

[Etienne Marion]

Maybe related: in #134 (which is still draft, I didn't have time to clean it yet) I define an IsPreBrownian predicate as follows:

class IsPreBrownian (P : Measure Ω := by volume_tac) : Prop where
  hasLaw : ∀ I : Finset ℝ≥0, HasLaw (fun ω ↦ I.restrict (X · ω)) (gaussianProjectiveFamily I) P

[Peter Pfaffelhuber]

Note also

example : (fun ω ↦ (preBrownian · ω)) = id := rfl

[Peter Pfaffelhuber]

Etienne Marion schrieb:

Maybe related: in #134 (which is still draft, I didn't have time to clean it yet) I define an IsPreBrownian predicate as follows:

class IsPreBrownian (P : Measure Ω := by volume_tac) : Prop where
  hasLaw : ∀ I : Finset ℝ≥0, HasLaw (fun ω ↦ I.restrict (X · ω)) (gaussianProjectiveFamily I) P

It can be proved that this is the same as IsGaussianProcess with a special expectation and covariance, right?

[Etienne Marion]

Well IsGaussianProcess does not mention expectation and covariance, but yes:

instance IsPreBrownian.isGaussianProcess [IsPreBrownian X P] : IsGaussianProcess X P where
  hasGaussianLaw I := (IsPreBrownian.hasLaw I).hasGaussianLaw

[Peter Pfaffelhuber]

My claim would be that some statements in BrownianMotion.lean are still true when replacing gaussianLimit with any projectiveLimit (except those which rely on continuity, or on Gaussian distributions, of course).

[Rémy Degenne]

I created a few issues on the github repository: https://github.com/RemyDegenne/brownian-motion/issues
They are also visible on the project view: https://github.com/users/RemyDegenne/projects/1/views/1
Each issue contains a link to a lemma in the blueprint, and each of those blueprint lemmas have links to Lean statements with sorry proofs. The task for each issue is to prove that statement.

Read the contributing guide to learn how to interact with those issues, in particular how to claim them: https://github.com/RemyDegenne/brownian-motion/blob/master/CONTRIBUTING.md

Please report anything unexpected with the issue claiming workflows. It's the first time we try them on this project.
I'll add more issues in the next days.

[Etienne Marion]

Can we solve several issues in one PR or is it better to open a PR for each issue?

[Rémy Degenne]

I'm fine with one PR for both. Let's try it and see if the automated workflow allows it

[Pietro Monticone]

Sure, you can claim multiple task issues and then propose the same #PR_NUMBER that should add the keywords “close #ISSUE1 … close #ISSUEn” linking all of them.

[Pietro Monticone]

In case it doesn’t currently work as expected you can write it manually or use the UI by just selecting all of them by clicking. Pretty quick either way.

[Etienne Marion]

So I commented propose #202 on #198 and it moved in progress, but when I commented awaiting-review in #202 it did not put #198 in review.

[Rémy Degenne]

New task: https://github.com/RemyDegenne/brownian-motion/issues/203

[Etienne Marion]

Just wanted to indicate that I am working on defining the right continuation of a filtration and adding API lemmas to the blueprint and statements to prove in the code.

[Rémy Degenne]

I thought a bit about the definition of the right continuation, and I'd like to have a definition that makes discrete filtrations right continuous, so that our theorems apply to both discrete and continuous settings. A way to do that would be to do something similar to Function.rightLim: if the point i is not isolated on the right, take the infimum ⨅ j > i, 𝓕 j as you are doing in https://github.com/RemyDegenne/brownian-motion/pull/207, but if it is isolated, then take 𝓕 i. The right continuation of a filtration indexed by Nat is then the filtration itself. Also it we have a filtration indexed by [0, T], then the right continuation at T is 𝓕 T.

[Rémy Degenne]

With your current definition of right continuation (which is also implied by our previous definition of right continuous filtration), a Nat indexed filtration is right continuous only if it is constant.

[Etienne Marion]

You are right I didn’t think of that.

[Etienne Marion]

I’ll work on the part about class D/DL processes.

[Rémy Degenne]

I'm finishing the Doob Lp inequality blueprint and creating tasks.

[Rémy Degenne]

I added tasks about (auxiliary lemmas for) the Komlos lemma.

[Rémy Degenne]

Etienne Marion just added a new batch of tasks: https://github.com/RemyDegenne/brownian-motion/issues.

We are having a hard time creating tasks fast enough to keep up with the speed of formalization! Thanks to everyone contributing proofs, it's going great.

This reinforces the impression I had for the first part of the project that the bottleneck for this project is translating the maths into Lean statements (so mainly blueprint writing, and then a bit of translation work, or a lot of work when it comes to finding the right definition and generality). I also know that sometimes restraining oneself to write only statements and let others do the proofs is a bit frustrating, so I want to thank @Etienne Marion and @Kexing Ying who have been working recently on the blueprint to produce tasks for others to work on, as well as @Lorenzo Luccioli and @Alessio Rondelli who wrote parts of the blueprint on Doob-Meyer and Doob's Lp inequality.

[Etienne Marion]

Rémy Degenne said:

I also know that sometimes restraining oneself to write only statements and let others do the proofs is a bit frustrating

I agree with this :sweat_smile: But it is also quite interesting to write the blueprint and somewhat satisfying to watch the structure of the project being constructed out of it.

[Etienne Marion]

Some more tasks appeared!

[Thomas Zhu]

I am working on formalizing the entire section on simple processes: https://remydegenne.github.io/brownian-motion/blueprint/sect0005.html. I decided to go with a bundled definition of SimpleProcess and ElementaryPredictableSet, and to change a general bilinear map $B$ back to scalar multiplication in the definition of elementary stochastic integral.

[Etienne Marion]

Thomas Zhu said:

I am working on formalizing the entire section on simple processes: https://remydegenne.github.io/brownian-motion/blueprint/sect0005.html. I decided to go with a bundled definition of SimpleProcess and ElementaryPredictableSet, and to change a general bilinear map $B$ back to scalar multiplication in the definition of elementary stochastic integral.

Why did you remove the general bilinear map?

[Thomas Zhu]

Etienne Marion said:

Thomas Zhu said:

I am working on formalizing the entire section on simple processes: https://remydegenne.github.io/brownian-motion/blueprint/sect0005.html. I decided to go with a bundled definition of SimpleProcess and ElementaryPredictableSet, and to change a general bilinear map $B$ back to scalar multiplication in the definition of elementary stochastic integral.

Why did you remove the general bilinear map?

See #Brownian motion > Definition of elementary stochastic integral