Rademacher type and cotype

DefinitionRademacher sign of a coordinate#✓fully proved

The Rademacher sign attached to a coordinate: 1 for true, -1 for false.

def rademacherSign (𝕜 : Type*) [RCLike 𝕜] {n : ℕ} (ε : Fin n → Bool) (i : Fin n) : 𝕜 :=
  if ε i then 1 else -1

Used by 11

Used byBound on the average Rademacher norm · Average squared norm of a Rademacher sum · Average squared Rademacher sum of unit vectors · Rademacher signs have norm one · Hilbert spaces have Rademacher cotype 2 · Rademacher sign on a false coordinate is minus one · Rademacher sign on a true coordinate is one · Hilbert spaces have Rademacher type 2 · Square-root form of the Rademacher second moment · Second moment of a Rademacher sum in a Hilbert space · Second moment of a real Rademacher sum

TheoremRademacher sign on a true coordinate is one#✓fully proved

The sign is 1 on a true coordinate.

theorem rademacherSign_eq_one_of {n : ℕ} {ε : Fin n → Bool} {i : Fin n}
    (h : ε i = true) : rademacherSign 𝕜 ε i = (1 : 𝕜)

Uses 1

Statement usesRademacher sign of a coordinate

TheoremRademacher sign on a false coordinate is minus one#✓fully proved

The sign is -1 on a false coordinate.

theorem rademacherSign_eq_neg_one_of {n : ℕ} {ε : Fin n → Bool} {i : Fin n}
    (h : ε i = false) : rademacherSign 𝕜 ε i = (-1 : 𝕜)

Uses 1

Statement usesRademacher sign of a coordinate

TheoremRademacher signs have norm one#✓fully proved

Every Rademacher sign has norm 1.

theorem norm_rademacherSign {n : ℕ} (ε : Fin n → Bool) (i : Fin n) :
    ‖rademacherSign 𝕜 ε i‖ = 1

Uses 1

Statement usesRademacher sign of a coordinate

TheoremNumber of sign vectors of length n#✓fully proved

Number of sign vectors: Fin n → Bool has 2 ^ n elements.

theorem card_sign_vectors (n : ℕ) :
    Fintype.card (Fin n → Bool) = 2 ^ n

Used by 2

Used byBound on the average Rademacher norm · Second moment of a Rademacher sum in a Hilbert space

TheoremSecond moment of a Rademacher sum in a Hilbert space#✓fully proved

Exact second moment of a Rademacher sum in a Hilbert space: the sum over all sign vectors of ‖∑ᵢ εᵢ • xᵢ‖² equals 2 ^ n * ∑ᵢ ‖xᵢ‖². Cross terms cancel: the induction step pairs the two values of the last sign and applies the parallelogram law.

theorem sum_rademacher_sq_norm_eq (n : ℕ) (x : Fin n → E) :
    ∑ ε : Fin n → Bool, ‖∑ i, rademacherSign 𝕜 ε i • x i‖ ^ 2
      = (2 : ℝ) ^ n * ∑ i, ‖x i‖ ^ 2

Uses 2 · Used by 3

Statement usesRademacher sign of a coordinate

Proof usesNumber of sign vectors of length n

Used byBound on the average Rademacher norm · Average squared norm of a Rademacher sum · Second moment of a real Rademacher sum

TheoremAverage squared norm of a Rademacher sum#✓fully proved

The average (uniform over sign vectors) of ‖∑ᵢ εᵢ • xᵢ‖² is exactly ∑ᵢ ‖xᵢ‖².

theorem average_rademacher_sq_norm_eq (n : ℕ) (x : Fin n → E) :
    ((2 : ℝ) ^ n) ⁻¹ * ∑ ε : Fin n → Bool, ‖∑ i, rademacherSign 𝕜 ε i • x i‖ ^ 2
      = ∑ i, ‖x i‖ ^ 2

Uses 2 · Used by 4

Statement usesRademacher sign of a coordinate

Proof usesSecond moment of a Rademacher sum in a Hilbert space

Used byAverage squared Rademacher sum of unit vectors · Hilbert spaces have Rademacher cotype 2 · Hilbert spaces have Rademacher type 2 · Square-root form of the Rademacher second moment

TheoremHilbert spaces have Rademacher type 2#✓fully proved

Rademacher type 2 with constant 1: the average of the squared Rademacher sums is at most ∑ᵢ ‖xᵢ‖².

theorem rademacher_type_two (n : ℕ) (x : Fin n → E) :
    ((2 : ℝ) ^ n) ⁻¹ * ∑ ε : Fin n → Bool, ‖∑ i, rademacherSign 𝕜 ε i • x i‖ ^ 2
      ≤ ∑ i, ‖x i‖ ^ 2

Uses 2

Statement usesRademacher sign of a coordinate

Proof usesAverage squared norm of a Rademacher sum

TheoremHilbert spaces have Rademacher cotype 2#✓fully proved

Rademacher cotype 2 with constant 1: ∑ᵢ ‖xᵢ‖² is at most the average of the squared Rademacher sums.

theorem rademacher_cotype_two (n : ℕ) (x : Fin n → E) :
    ∑ i, ‖x i‖ ^ 2
      ≤ ((2 : ℝ) ^ n) ⁻¹ * ∑ ε : Fin n → Bool, ‖∑ i, rademacherSign 𝕜 ε i • x i‖ ^ 2

Uses 2

Statement usesRademacher sign of a coordinate

Proof usesAverage squared norm of a Rademacher sum

TheoremSquare-root form of the Rademacher second moment#✓fully proved

Square-root form of the exact second moment.

theorem sqrt_average_rademacher_sq_norm_eq (n : ℕ) (x : Fin n → E) :
    Real.sqrt (((2 : ℝ) ^ n) ⁻¹ *
        ∑ ε : Fin n → Bool, ‖∑ i, rademacherSign 𝕜 ε i • x i‖ ^ 2)
      = Real.sqrt (∑ i, ‖x i‖ ^ 2)

Uses 2

Statement usesRademacher sign of a coordinate

Proof usesAverage squared norm of a Rademacher sum

TheoremBound on the average Rademacher norm#✓fully proved

The average Rademacher norm is at most (∑ᵢ ‖xᵢ‖²)^{1/2} (Cauchy–Schwarz for the finite average, plus the exact second moment).

theorem average_rademacher_norm_le (n : ℕ) (x : Fin n → E) :
    ((2 : ℝ) ^ n) ⁻¹ * ∑ ε : Fin n → Bool, ‖∑ i, rademacherSign 𝕜 ε i • x i‖
      ≤ Real.sqrt (∑ i, ‖x i‖ ^ 2)

Uses 3

Statement usesRademacher sign of a coordinate

Proof usesNumber of sign vectors of length n · Second moment of a Rademacher sum in a Hilbert space

TheoremAverage squared Rademacher sum of unit vectors#✓fully proved

For unit vectors, the average squared Rademacher sum equals n.

theorem average_rademacher_sq_norm_eq_of_norm_eq_one {n : ℕ} {x : Fin n → E}
    (hx : ∀ i, ‖x i‖ = 1) :
    ((2 : ℝ) ^ n) ⁻¹ * ∑ ε : Fin n → Bool, ‖∑ i, rademacherSign 𝕜 ε i • x i‖ ^ 2
      = n

Uses 2

Statement usesRademacher sign of a coordinate

Proof usesAverage squared norm of a Rademacher sum

TheoremSecond moment of a real Rademacher sum#✓fully proved

Scalar real form: the second moment of ∑ᵢ ±aᵢ over all sign choices is 2 ^ n * ∑ᵢ aᵢ².

theorem sum_rademacher_sq_real (n : ℕ) (a : Fin n → ℝ) :
    ∑ ε : Fin n → Bool, (∑ i, (if ε i then a i else -a i)) ^ 2
      = (2 : ℝ) ^ n * ∑ i, (a i) ^ 2

Uses 2

Proof usesRademacher sign of a coordinate · Second moment of a Rademacher sum in a Hilbert space

DefinitionRademacher distribution#✓fully proved

The Rademacher distribution is the measure on \(\{-1, 1\}\), viewed as a subset of \(\mathbb{Z}\), that gives mass \(1/2\) to each of \(1\) and \(-1\).

noncomputable def rademacherDistribution : Measure ({-1, 1} : Set ℤ) :=
  bernoulliMeasure ⟨1, by decide⟩ ⟨-1, by decide⟩ ⟨1 / 2, by norm_num⟩

Used by 1

Used byProduct Rademacher distribution

DefinitionProduct Rademacher distribution#✓fully proved

For an index type \(\iota\), this is the product over \(\iota\) of copies of the Rademacher distribution: the joint law of a family \((\varepsilon_i)_{i \in \iota}\) of independent Rademacher random variables, as a measure on the functions \(\iota \to \{-1, 1\}\).

noncomputable def rademacherProductDistribution (ι : Type*) :
    Measure (ι → ({-1, 1} : Set ℤ)) :=
  infinitePi (fun _ : ι ↦ rademacherDistribution)

Uses 1 · Used by 2

Statement usesRademacher distribution

Used byEnflo type · Rademacher type

DefinitionDiscrete partial derivative on the Rademacher cube#✓fully proved

Let \(X\) be a real Banach space, \(n\) a natural number and \(f : \{-1, 1\}^n \to X\). For \(j \in \{1, \dots, n\}\) and \(\varepsilon = (\varepsilon_1, \dots, \varepsilon_n) \in \{-1, 1\}^n\), the discrete partial derivative of \(f\) in direction \(j\) at \(\varepsilon\) is

\[ D_j f(\varepsilon) = \frac{1}{2}\bigl(f(\varepsilon) - f(\varepsilon_1, \dots, -\varepsilon_j, \dots, \varepsilon_n)\bigr), \]

where only the \(j\)-th coordinate of \(\varepsilon\) is negated in the second term.

noncomputable def D {n : ℕ} (j : Fin n) (f : (Fin n → ({-1, 1} : Set ℤ)) → X)
      (ε : Fin n → ({-1, 1} : Set ℤ)) : X :=
  (1 / (2 : ℝ)) • (f ε - f (update ε j (- ε j)))

Used by 1

Used byEnflo type

DefinitionRademacher type#✓fully proved

Let \(X\) be a real Banach space, \(C \in [0, \infty]\) and \(p\) a real number. We say that \(X\) has Rademacher type \(p\) with constant \(C\) if for every \(n \ge 1\) and all \(x_1, \dots, x_n \in X\),

\[ \mathbb{E}\Bigl\|\sum_{j=1}^n \varepsilon_j x_j\Bigr\|^p \le C^p \sum_{j=1}^n \|x_j\|^p, \]

where \(\varepsilon_1, \dots, \varepsilon_n\) are independent Rademacher random variables. Both sides are computed in \([0, \infty]\).

def IsRademacherType (C : ℝ≥0∞) (p : ℝ) : Prop :=
  ∀ n ≥ 1, ∀ (x : Fin n → X),
    𝔼⁻[‖ ∑ j : Fin n, ((ε j) : ℝ) • (x j) ‖ₑ ^ p; ε ∼ rademacherProductDistribution (Fin n)]
    ≤ C ^ p * ∑ j : Fin n, ‖ x j ‖ₑ ^ p

Uses 1 · Used by 1

Statement usesProduct Rademacher distribution

Used byRademacher type constant

DefinitionRademacher type constant#✓fully proved

For a real Banach space \(X\) and a real number \(p\), \(T^R_p(X)\) is the infimum in \([0, \infty]\) of all \(C \in [0, \infty]\) such that \(X\) has Rademacher type \(p\) with constant \(C\).

noncomputable def TR (p : ℝ) : ℝ≥0∞ := sInf {C : ℝ≥0∞ | IsRademacherType X C p}

Uses 1 · Used by 1

Statement usesRademacher type

Used byComparison of Rademacher and Enflo type constants

DefinitionEnflo type#✓fully proved

Let \(X\) be a real Banach space, \(C \in [0, \infty]\) and \(p\) a real number. We say that \(X\) has Enflo type \(p\) with constant \(C\) if for every \(n \ge 1\) and every function \(f : \{-1, 1\}^n \to X\),

\[ \mathbb{E}\Bigl\|\frac{f(\varepsilon) - f(-\varepsilon)}{2}\Bigr\|^p \le C^p \sum_{j=1}^n \mathbb{E}\,\|D_j f(\varepsilon)\|^p, \]

where \(\varepsilon = (\varepsilon_1, \dots, \varepsilon_n)\) is a sequence of independent Rademacher random variables, \(-\varepsilon = (-\varepsilon_1, \dots, -\varepsilon_n)\), and \(D_j f\) is the discrete partial derivative of \(f\) in direction \(j\). Both sides are computed in \([0, \infty]\).

def IsEnfloType (C : ℝ≥0∞) (p : ℝ) : Prop :=
    ∀ n ≥ 1, ∀ (f : (Fin n → ({-1, 1} : Set ℤ)) → X),
  𝔼⁻[‖ (1 / (2 : ℝ)) • (f ε - f (- ε)) ‖ₑ ^ p; ε ∼ rademacherProductDistribution (Fin n)]
  ≤ C ^ p * ∑ j : Fin n, 𝔼⁻[‖ D j f ε ‖ₑ ^ p; ε ∼ rademacherProductDistribution (Fin n)]

Uses 2 · Used by 1

Statement usesDiscrete partial derivative on the Rademacher cube · Product Rademacher distribution

Used byEnflo type constant

DefinitionEnflo type constant#✓fully proved

For a real Banach space \(X\) and a real number \(p\), \(T^E_p(X)\) is the infimum in \([0, \infty]\) of all \(C \in [0, \infty]\) such that \(X\) has Enflo type \(p\) with constant \(C\).

noncomputable def TE (p : ℝ) : ℝ≥0∞ := sInf {C : ℝ≥0∞ | IsEnfloType X C p}

Uses 1 · Used by 1

Statement usesEnflo type

Used byComparison of Rademacher and Enflo type constants

TheoremComparison of Rademacher and Enflo type constants#●ready to prove

For every real Banach space \(X\) and every real number \(p\) with \(1 \le p \le 2\), the Rademacher type constant and the Enflo type constant of \(X\) satisfy \(T^R_p(X) \le T^E_p(X) \le \frac{\pi}{\sqrt{2}}\, T^R_p(X)\).

public theorem_wanted theorem_1_1 (p : ℝ) (h1p : 1 ≤ p) (hp2 : p ≤ 2) :
    TR X p ≤ TE X p ∧ TE X p ≤ (pi / sqrt 2) * TR X p

Sources

• P. Ivanisvili, R. van Handel, and A. Volberg, Rademacher type and Enflo type coincide, Annals of Math, 192 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_rademacher_enflo_type of the lean-eval benchmark.

Uses 2

Statement usesEnflo type constant · Rademacher type constant

20 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.