how to formalize this theorem in Lean4?

Stream: new members

[Zihao Zhang]

image.png

[Notification Bot]

This topic was moved here from #general > how to formalize this theorem in Lean4? by Johan Commelin.

[Johan Commelin]

What have you tried so far?

[Zihao Zhang]

@Johan Commelin I just wrote this:

import Mathlib.Probability.Notation
import Mathlib.Probability.Integration
import Mathlib.Probability.Variance
import Mathlib.MeasureTheory.Function.L2Space

open MeasureTheory Filter Finset ProbabilityTheory

noncomputable section

open scoped MeasureTheory ProbabilityTheory ENNReal NNReal

variable {Ω : Type*} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω}
variable [MeasureSpace Ω]

I don't know how to define Rademacher random variable in Lean4

[Rémy Degenne]

You can state your problem like this:

import Mathlib

open MeasureTheory Finset ProbabilityTheory Measure Real
open scoped ENNReal

variable {Ω : Type*} {m : MeasurableSpace Ω} {P : Measure Ω} -- a measurable space and a measure
  {X : ℕ → Ω → ℝ} -- ℕ-indexed real-valued random variables

lemma concentration_inequality
    (hX : ∀ n, P.map (X n) = (2 : ℝ≥0∞)⁻¹ • dirac (-1) + (2 : ℝ≥0∞)⁻¹ • dirac 1) -- Rademacher law
    (h_indep : iIndepFun X P) -- independence
    {ε : ℝ} (hε : 0 ≤ ε) (n : ℕ) :
    (P {ω | ε ≤ (∑ i ∈ range n, X i ω) / n}).toReal ≤ exp (n * ε ^ 2 / 2) := by
  sorry

[Zihao Zhang]

@Rémy Degenne Thank you so much!

[Rémy Degenne]

Do you know how the proof should proceed? If you describe a math proof, I could point you to relevant lean statements or files.

[Zihao Zhang]

@Rémy Degenne This is the proof.

$$\begin{split} \Pr\left[\frac{1}{n} \sum_{i=1}^n X_i \ge \varepsilon \right] &\le \frac{1}{e^{ n \varepsilon}} \mathbb{E}\left[e^{t \sum_{i=1}^n X_i}\right] \quad (\text{Markov's inequality}) \\ &= \frac{1}{e^{t n \varepsilon}} \prod_{i=1}^n \mathbb{E}[e^{t X_i}] \\ &= \frac{1}{e^{t n \varepsilon}} \prod_{i=1}^n \left( \frac{1}{2} e^t + \frac{1}{2} e^{-t} \right) \\ &= \frac{1}{e^{t n \varepsilon}} \prod_{i=1}^n \left( \frac{1}{2} \sum_{k=0}^{\infty} \frac{t^k}{k!} + \frac{1}{2} \sum_{k=0}^{\infty} \frac{(-t)^k}{k!} \right) \\ &= \frac{1}{e^{t n \varepsilon}} \prod_{i=1}^n \sum_{k=0}^{\infty} \frac{t^{2k}}{(2k)!} \\ &\leq \frac{1}{e^{t n \varepsilon}} \prod_{i=1}^n \sum_{k=0}^{\infty} \frac{\left( \frac{t^2}{2} \right)^k}{k!} \quad (2k! \geq 2^k \cdot k!) \\ &= \frac{1}{e^{t n \varepsilon}} \prod_{i=1}^n e^{\frac{t^2}{2}} \\ &= e^{\frac{n}{2} t^2 - n t \varepsilon} \\ &= e^{-\frac{n}{2} \varepsilon^2} \quad (\text{let } t = \varepsilon) \end{split}$$

[Rémy Degenne]

In that proof, you prove that a Rademacher random variable is sub-Gaussian in the sense of ProbabilityTheory.HasSubgaussianMGF (click the "source" link: the doc entry is surprisingly unreadable).
And then you can use the result ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun . Again, look at the source code. I don't know what is happening with the docs.

[Zihao Zhang]

Rémy Degenne said:

You can state your problem like this:

import Mathlib

open MeasureTheory Finset ProbabilityTheory Measure Real
open scoped ENNReal

variable {Ω : Type*} {m : MeasurableSpace Ω} {P : Measure Ω} -- a measurable space and a measure
  {X : ℕ → Ω → ℝ} -- ℕ-indexed real-valued random variables

lemma concentration_inequality
    (hX : ∀ n, P.map (X n) = (2 : ℝ≥0∞)⁻¹ • dirac (-1) + (2 : ℝ≥0∞)⁻¹ • dirac 1) -- Rademacher law
    (h_indep : iIndepFun X P) -- independence
    {ε : ℝ} (hε : 0 ≤ ε) (n : ℕ) :
    (P {ω | ε ≤ (∑ i ∈ range n, X i ω) / n}).toReal ≤ exp (n * ε ^ 2 / 2) := by
  sorry

It reported an error
image.png
image.png

[Kevin Buzzard]

I would recommend that you read and understand the error. Lean is saying "you gave the wrong input to a function" and it's telling you exactly which function and which input.

[Rémy Degenne]

iIndepFun changed recently (it had an explicit argument for the sigma-algebra before). If you open my code in the web editor, you will see it works there. Your Mathlib must be slightly older. Either update or adapt the code to your version.

[Zihao Zhang]

OK