The capped estimate in the hypercontractive range

DefinitionPer-coordinate damped weight#✓fully proved

The per-coordinate damped weight Dₑ(u) = ∑_{S ∋ e} (1-u)^{|S|-1} (f̂(S)/√(p(1-p)))² under μ_p.

noncomputable def frh_perCoordWeight (p u : ℝ) (φ : ConfigSpace ι → Bool) (e : ι) : ℝ :=
  ∑ S ∈ univ.filter (fun S : Finset ι => e ∈ S),
    (Real.sqrt (1 - u) ^ (S.erase e).card) ^ 2
      * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S / ptn_sigma p) ^ 2

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · \(p\)-biased Fourier coefficient · Standard deviation of a Bernoulli bit

Used byDamped total weight as a sum of per-coordinate weights

TheoremDamped total weight as a sum of per-coordinate weights#✓fully proved

The damped total weight is 4p(1-p) ∑ₑ Dₑ(u).

theorem frh_lhs_eq {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (φ : ConfigSpace ι → Bool)
    {u : ℝ} (_hu0 : 0 ≤ u) (hu1 : u ≤ 1) :
    (∑ S : Finset ι, 4 * (S.card : ℝ) * (1 - u) ^ (S.card - 1)
        * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
      = 4 * (ptn_sigma p) ^ 2 * ∑ e : ι, frh_perCoordWeight p u φ e

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Per-coordinate damped weight · \(p\)-biased Fourier coefficient · Standard deviation of a Bernoulli bit

TheoremDamped total weight at \(u = 0\) is at most the total influence#✓fully proved

At u = 0 the damped total weight is at most the total influence.

theorem frh_at_zero {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (φ : ConfigSpace ι → Bool) :
    (∑ S : Finset ι, 4 * (S.card : ℝ) * (1 - (0 : ℝ)) ^ (S.card - 1)
        * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
      ≤ totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 6 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · \(p\)-biased Fourier coefficient · Total influence under a product weight

Proof usesStandard deviation of a Bernoulli bit · \(p\)-biased total influence as Fourier weight

Used byCapped estimate on \((0, 1)\) from concavity of the right side · Open-interval case implies the full capped estimate on \((1/2, q)\)

TheoremCapped estimate in the hypercontractive range#✓fully proved

The capped estimate in the hypercontractive range: if 1 - u = 4p(1-p)(q'-1) with 1 ≤ q' ≤ 2, then ∑_S 4 |S| (1-u)^{|S|-1} f̂(S)² ≤ 4p(1-p) * δ^{2/q'-1} ∑ₑ Infₑ.

theorem frh_capped_martingale [Nonempty ι] {p q' : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (hq1 : 1 ≤ q') (hq2 : q' ≤ 2) {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1)
    (hrel : 1 - u = (q' - 1) * 4 * p * (1 - p)) (φ : ConfigSpace ι → Bool) :
    (∑ S : Finset ι, 4 * (S.card : ℝ) * (1 - u) ^ (S.card - 1)
        * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
      ≤ 4 * (ptn_sigma p) ^ 2
        * ((maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (2 / q' - 1)
          * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))

Uses 7 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Maximal influence under a product weight · \(p\)-biased Fourier coefficient · Standard deviation of a Bernoulli bit · Total influence under a product weight

Proof usesCapped per-coordinate estimate under the \(p\)-biased measure

Used byCapped estimate in the hypercontractive range with matching \(q'\) · Low-range case implies the small-influence case · Capped estimate at \(p = 1/2\) for all \(u \in (0, 1)\) · Target-exponent capped estimate from a domination bound · Capped estimate at the endpoint \(u = 1\)

TheoremParametrization of the hypercontractive range by \(q' \in (1, 2)\)#✓fully proved

Every u ∈ [1 - 4p(1-p), 1] has the form 1 - u = 4p(1-p)(q'-1) with q' ∈ [1, 2].

theorem frh_capped_param {p u : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (hlo : 1 - 4 * p * (1 - p) ≤ u) (hu1 : u ≤ 1) :
    ∃ q' : ℝ, 1 ≤ q' ∧ q' ≤ 2 ∧ 1 - u = (q' - 1) * 4 * p * (1 - p)

Used by 1

Used byCapped estimate in the hypercontractive range with matching \(q'\)

DefinitionOpen-interval residual case of the capped estimate#✓fully proved

The capped estimate ∑_S 4 |S| (1-u)^{|S|-1} f̂(S)² ≤ δ^{u/(2-u)} ∑ₑ Infₑ for all p ∈ (1/2, q) with p < 1 and all u ∈ (0, 1).

def frh_openResidue (q : ℝ) : Prop :=
  ∀ p ∈ Set.Ioo (1 / 2 : ℝ) q, p < 1 → ∀ {E : Type} [Fintype E] [DecidableEq E] [Nonempty E]
    (φ : ConfigSpace E → Bool), ∀ u : ℝ, 0 < u → u < 1 →
      (∑ S : Finset E, 4 * (S.card : ℝ) * (1 - u) ^ (S.card - 1)
          * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
        ≤ (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (u / (2 - u))
          * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Maximal influence under a product weight · \(p\)-biased Fourier coefficient · Total influence under a product weight

Used bySmall-influence case implies the open-interval case · Open-interval case implies the full capped estimate on \((1/2, q)\)

TheoremCapped estimate at the endpoint \(u = 1\)#✓fully proved

At u = 1 the capped estimate holds.

theorem frh_endpoint_one [Nonempty ι] {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool) :
    (∑ S : Finset ι, 4 * (S.card : ℝ) * (1 - (1 : ℝ)) ^ (S.card - 1)
        * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
      ≤ (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
          ^ ((1 : ℝ) / (2 - 1))
        * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 13 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Maximal influence under a product weight · \(p\)-biased Fourier coefficient · Total influence under a product weight

Proof usesProduct probability weight · Expectation under a product weight · Influence of a coordinate · Probability of a configuration under a product weight · Capped estimate in the hypercontractive range · Standard deviation of a Bernoulli bit · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byCapped estimate on \((0, 1)\) from concavity of the right side · Open-interval case implies the full capped estimate on \((1/2, q)\)

TheoremOpen-interval case implies the full capped estimate on \((1/2, q)\)#✓fully proved

frh_openResidue q implies mxd_martingaleHC_statement q, by adding the endpoints.

theorem frh_martingaleHC_of_openResidue {q : ℝ} (H : frh_openResidue q) :
    mxd_martingaleHC_statement q

Uses 9 · Used by 1

Statement usesOpen-interval residual case of the capped estimate · Capped influence estimate for all \(p\) in \((1/2, q)\)

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Damped total weight at \(u = 0\) is at most the total influence · Capped estimate at the endpoint \(u = 1\) · Maximal influence under a product weight · \(p\)-biased Fourier coefficient · Total influence under a product weight

Used bySmall-influence case implies the full capped estimate on \((1/2, q)\)

TheoremHypercontractive range misses an interval near \(u = 0\)#✓fully proved

For p > 1/2 the hypercontractive range u ≥ 1 - 4p(1-p) excludes a nonempty interval near u = 0.

theorem frh_lowNoise_range_nonempty {p : ℝ} (hp : 1 / 2 < p) (_hp1 : p < 1) :
    0 < 1 - 4 * p * (1 - p)

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.