The capped estimate in the hypercontractive range with a gap condition

TheoremHypercontractive exponent is at most the target exponent#✓fully proved

In the hypercontractive range the exponent 2/q' - 1 is at most the target exponent u/(2-u).

theorem hcq_exponent_le {p q' u : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (hu1 : u < 1) (hrel : 1 - u = (q' - 1) * 4 * p * (1 - p)) :
    2 / q' - 1 ≤ u / (2 - u)

TheoremClosed form of the exponent gap#✓fully proved

Closed form of the exponent gap u/(2-u) - (2/q' - 1).

theorem hcq_gap_closedForm {s u : ℝ} (hs0 : 0 < s) (hu1 : u < 1) (hslu : 0 < s + 1 - u) :
    u / (2 - u) - (2 / (1 + (1 - u) / s) - 1)
      = 2 * (1 - u) * (1 - s) / ((s + 1 - u) * (2 - u))

Used by 1

Used byUpper bound on the exponent gap

TheoremUpper bound on the exponent gap#✓fully proved

Upper bound on the exponent gap.

theorem hcq_gap_le {s u : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hu_lo : 1 - s < u) (hu_hi : u < 1) :
    u / (2 - u) - (2 / (1 + (1 - u) / s) - 1) ≤ 2 * (1 - u) * (1 - s) / s

Uses 1 · Used by 1

Proof usesClosed form of the exponent gap

Used byGap condition holds at some \(u < 1\) in the hypercontractive range

TheoremCapped estimate in the hypercontractive range with matching \(q'\)#✓fully proved

The capped estimate in the hypercontractive range, with the matching q'.

theorem hcq_capped_full [Nonempty ι] {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool) {u : ℝ}
    (hlo : 1 - 4 * p * (1 - p) ≤ u) (hu1 : u ≤ 1) :
    ∃ q' : ℝ, 1 ≤ q' ∧ q' ≤ 2 ∧ 1 - u = (q' - 1) * 4 * p * (1 - p) ∧
      (∑ 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 8

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 estimate in the hypercontractive range · Parametrization of the hypercontractive range by \(q' \in (1, 2)\)

TheoremUnder the gap condition the hypercontractive bound is dominated#✓fully proved

If δ^{gap} ≥ 4p(1-p), the bound with exponent 2/q' - 1 and factor 4p(1-p) is at most δ^{u/(2-u)}.

theorem hcq_dom_of_threshold {p δ q' u : ℝ} (hδ0 : 0 < δ)
    (hthr : 4 * (ptn_sigma p) ^ 2 ≤ δ ^ (u / (2 - u) - (2 / q' - 1))) :
    4 * (ptn_sigma p) ^ 2 * δ ^ (2 / q' - 1) ≤ δ ^ (u / (2 - u))

Uses 1 · Used by 1

Statement usesStandard deviation of a Bernoulli bit

Used byTarget-exponent capped estimate under the gap condition

TheoremTarget-exponent capped estimate from a domination bound#✓fully proved

The capped estimate with exponent u/(2-u) from a domination of the hypercontractive bound.

theorem hcq_star_of_dominates [Nonempty ι] {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool) {u : ℝ}
    (hlo : 1 - 4 * p * (1 - p) ≤ u) (hu1 : u ≤ 1)
    {q' : ℝ} (hq1 : 1 ≤ q') (hq2 : q' ≤ 2)
    (hrel : 1 - u = (q' - 1) * 4 * p * (1 - p))
    (hdom : 4 * (ptn_sigma p) ^ 2
        * (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (2 / q' - 1)
      ≤ (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (u / (2 - u))) :
    (∑ S : Finset ι, 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 13 · Used by 1

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 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 · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byTarget-exponent capped estimate under the gap condition

TheoremTarget-exponent capped estimate under the gap condition#✓fully proved

The capped estimate with exponent u/(2-u) in the hypercontractive range, under the gap condition δ^{gap} ≥ 4p(1-p).

theorem hcq_star_capped_threshold [Nonempty ι] {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool) {u : ℝ}
    (hlo : 1 - 4 * p * (1 - p) ≤ u) (hu1 : u < 1)
    (hδ0 : 0 < maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
    {q' : ℝ} (hq1 : 1 ≤ q') (hq2 : q' ≤ 2)
    (hrel : 1 - u = (q' - 1) * 4 * p * (1 - p))
    (hthr : 4 * (ptn_sigma p) ^ 2
      ≤ (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
          ^ (u / (2 - u) - (2 / q' - 1))) :
    (∑ S : Finset ι, 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 8 · Used by 2

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 usesUnder the gap condition the hypercontractive bound is dominated · Target-exponent capped estimate from a domination bound

Used byLow-range case implies the small-influence case · Capped estimate at \(p = 1/2\) for all \(u \in (0, 1)\)

TheoremCapped estimate at \(p = 1/2\) for all \(u \in (0, 1)\)#✓fully proved

At p = 1/2 the capped estimate ∑_S 4 |S| (1-u)^{|S|-1} f̂(S)² ≤ δ^{u/(2-u)} ∑ₑ Infₑ holds for all u ∈ (0, 1).

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

Uses 14

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 · Target-exponent capped estimate under the gap condition · Standard deviation of a Bernoulli bit · Closing a coordinate of a configuration · Opening a coordinate of a configuration

DefinitionLow-range residual case of the capped estimate#✓fully proved

The capped estimate for all p ∈ (1/2, q) with p < 1, δ < e^{-1}, and u ∈ (0, 1) either below the hypercontractive range or failing the gap condition.

def hcq_lowRangeResidue (q : ℝ) : Prop :=
  ∀ p ∈ Set.Ioo (1 / 2 : ℝ) q, p < 1 → ∀ {E : Type} [Fintype E] [DecidableEq E] [Nonempty E]
    (φ : ConfigSpace E → Bool),
      maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) < Real.exp (-1) →
      ∀ u : ℝ, 0 < u → u < 1 →
        (u < 1 - 4 * p * (1 - p) ∨
          (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
              ^ (u / (2 - u) - (2 / (1 + (1 - u) / (4 * p * (1 - p))) - 1))
            < 4 * (ptn_sigma p) ^ 2) →
        (∑ 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 6 · Used by 3

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

Used byLow-degree case implies the low-range case · Low-range case implies the full capped estimate on \((1/2, q)\) · Low-range case implies the small-influence case

TheoremLow-range case implies the small-influence case#✓fully proved

hcq_lowRangeResidue q implies cvg_smallDeltaResidue q.

theorem hcq_smallDelta_of_lowRange {q : ℝ} (H : hcq_lowRangeResidue q) :
    cvg_smallDeltaResidue q

Uses 16 · Used by 2

Statement usesSmall-influence residual case of the capped estimate · Low-range residual case of the capped estimate

Proof usesConfiguration space of a statistical-mechanics model · Product probability weight · Bernoulli product weight · Expectation under a product weight · Influence of a coordinate · Probability of a configuration under a product weight · Capped estimate in the hypercontractive range · Target-exponent capped estimate under the gap condition · Maximal influence under a product weight · \(p\)-biased Fourier coefficient · Standard deviation of a Bernoulli bit · Total influence under a product weight · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byLow-degree case implies the small-influence case · Low-range case implies the full capped estimate on \((1/2, q)\)

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

hcq_lowRangeResidue q implies mxd_martingaleHC_statement q.

theorem hcq_martingaleHC_of_lowRange {q : ℝ} (H : hcq_lowRangeResidue q) :
    mxd_martingaleHC_statement q

Uses 4

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

Proof usesSmall-influence case implies the full capped estimate on \((1/2, q)\) · Low-range case implies the small-influence case

TheoremGap condition holds at \(u = 1\)#✓fully proved

At u = 1 (q' = 1) the gap condition holds.

theorem hcq_dominated_nonempty {p δ : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (_hδ0 : 0 < δ) (_hδ1 : δ ≤ 1) :
    4 * (ptn_sigma p) ^ 2 ≤ δ ^ ((1 : ℝ) / (2 - 1) - (2 / (1 : ℝ) - 1))

Uses 1

Statement usesStandard deviation of a Bernoulli bit

TheoremPower bound \(s \le \delta^g\) from a logarithmic exponent bound#✓fully proved

s ≤ δ^g when g ≤ log (1/s) / log (1/δ).

theorem hcq_threshold_of_gap_small {s δ g : ℝ} (hs0 : 0 < s)
    (hδ0 : 0 < δ) (hδ1 : δ < 1) (hgle : g ≤ Real.log (1 / s) / Real.log (1 / δ)) :
    s ≤ δ ^ g

Used by 1

Used byGap condition holds at some \(u < 1\) in the hypercontractive range

TheoremGap condition holds at some \(u < 1\) in the hypercontractive range#✓fully proved

For p > 1/2 and 0 < δ < 1, some u ∈ (0, 1) lies in the hypercontractive range and satisfies the gap condition.

theorem hcq_residue_proper {p δ : ℝ} (hp : 1 / 2 < p) (hp1 : p < 1) (hδ0 : 0 < δ) (hδ1 : δ < 1) :
    ∃ u : ℝ, (0 < u ∧ u < 1) ∧ 1 - 4 * p * (1 - p) ≤ u ∧
      4 * (ptn_sigma p) ^ 2
        ≤ δ ^ (u / (2 - u) - (2 / (1 + (1 - u) / (4 * p * (1 - p))) - 1))

Uses 3 · Used by 1

Statement usesStandard deviation of a Bernoulli bit

Proof usesUpper bound on the exponent gap · Power bound \(s \le \delta^g\) from a logarithmic exponent bound

Used byLow-range case condition fails for some \(u\)

TheoremLow-range case condition fails for some \(u\)#✓fully proved

For p > 1/2 and 0 < δ < 1, the case condition in hcq_lowRangeResidue fails for some u ∈ (0, 1).

theorem hcq_antecedent_not_tautology {p δ : ℝ} (hp : 1 / 2 < p) (hp1 : p < 1)
    (hδ0 : 0 < δ) (hδ1 : δ < 1) :
    ∃ u : ℝ, (0 < u ∧ u < 1) ∧
      ¬ (u < 1 - 4 * p * (1 - p) ∨
          δ ^ (u / (2 - u) - (2 / (1 + (1 - u) / (4 * p * (1 - p))) - 1))
            < 4 * (ptn_sigma p) ^ 2)

Uses 2

Statement usesStandard deviation of a Bernoulli bit

Proof usesGap condition holds at some \(u < 1\) in the hypercontractive range

TheoremRight side of the capped estimate is nonnegative#✓fully proved

The right side δ^{u/(2-u)} ∑ₑ Infₑ of the capped estimate is nonnegative.

theorem hcq_lowRange_nonvacuous {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
    {E : Type} [Fintype E] [DecidableEq E] [Nonempty E] (φ : ConfigSpace E → Bool)
    {u : ℝ} (_hu0 : 0 < u) (_hu1 : u < 1) :
    (0 : ℝ)
      ≤ (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (u / (2 - u))
        * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 10

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Maximal influence under a product weight · 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 · Closing a coordinate of a configuration · Opening a coordinate of a configuration

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.