Centering lemma

Stream: Is there code for X?

[Yaël Dillies]

Has anyone proved the centering lemma (cf the High Dimensional Probability book)? cc @Rémy Degenne, @Kei TSUKAMOTO

[Yaël Dillies]

(sorry for the poor question, I don't have access to a computer nor to the book)

[Yaël Dillies]

I need this to prove the dimension reduction lemma for covering numbers (8.3.17 or some number around that in HDP)

[Rémy Degenne]

The centering lemma for what kind of object?

[Rémy Degenne]

Sub-Gaussian random variables I guess, given the book and the mentions?

[Yaël Dillies]

Yes, sorry, the centering lemma in terms of ||.||_{\psi_2} (following HDP's notation), so subgaussian

[Rémy Degenne]

In that case, no. And note that the sub-Gaussian definition I added is not the one with the Orlicz norm as in that lemma, but the comparison of the mgf to the one of a centered Gaussian. What I added requires expectation zero.

[Rémy Degenne]

I added property (v) of Proposition 2.5.2 of that book.

[Yaël Dillies]

Oh, I didn't notice that discrepancy. What's your motivation for requiring zero expectation?

[Rémy Degenne]

Property (v) is the one that you use in a Chernoff bound. You would typically center first, then use that property.

[Rémy Degenne]

I called that def HasSubgaussianMGF to insist on the fact that it's the mgf comparison. I am planning to add the other one too, probably under the name IsSubgaussian.

[Yaël Dillies]

Great! How much of this is already done and would I be duplicating work if I were to do this in Lean?

[Rémy Degenne]

It's not even started. If you do it, please define a general Orlicz norm then specialize to the sub-Gaussian one :)

[Yaël Dillies]

Great, consider that done :grinning_face_with_smiling_eyes:

[Yaël Dillies]

The situation here is that I need a finitely additive measure version of 8.3.18 (Haussler's packing lemma) for my PhD, and I believe a simple trick works. But, because I have close to zero intuition about finitely additive measures, I would like Lean to check my work

[Yaël Dillies]

In short, I am using Lean as a genuine proof assistant

[Rémy Degenne]

I am reading the proof of 8.3.19: is it the case that actually you just want to know that bounded random variables are sub-Gaussian in order to apply Hoeffding? (not exactly sure because I did not look up all definitions in the pages before).

PR #18091 has the fact that bounded with mean 0 is sub-Gaussian (without using the sub-Gaussian definition I introduced yet, just showing the mgf inequality), and PR #22433 has Hoeffding's inequality. You could perhaps center first, which keeps your random variable bounded in some interval, then use those results.