The capped estimate from convexity

TheoremNonpositivity of a convex function from its endpoint values#✓fully proved

A convex function on [0, 1] that is nonpositive at both endpoints is nonpositive on [0, 1]. See also ConvexOn.le_max_of_mem_Icc.

theorem cvg_convexGap_le {G : ℝ → ℝ} (hG : ConvexOn ℝ (Icc (0 : ℝ) 1) G)
    (h0 : G 0 ≤ 0) (h1 : G 1 ≤ 0) {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1) :
    G u ≤ 0

Used by 1

Used byCapped estimate on \((0, 1)\) from concavity of the right side

TheoremFinite sum of convex functions is convex#✓fully proved

A finite sum of convex functions is convex.

theorem cvg_convexOn_sum {α : Type*} (s : Finset α) (g : α → ℝ → ℝ) {D : Set ℝ}
    (hD : Convex ℝ D) (hg : ∀ a ∈ s, ConvexOn ℝ D (g a)) :
    ConvexOn ℝ D (fun u => ∑ a ∈ s, g a u)

Used by 1

Used byConvexity of the damped total weight

TheoremConvexity of \((1 - u)^k\) on \((0, 1)\)#✓fully proved

u ↦ (1 - u)^k is convex on [0, 1].

theorem cvg_oneSubPow_convexOn (k : ℕ) :
    ConvexOn ℝ (Icc (0 : ℝ) 1) (fun u : ℝ => (1 - u) ^ k)

Used by 1

Used byConvexity of the damped total weight

TheoremConvexity of the damped total weight#✓fully proved

The damped total weight u ↦ ∑_S 4 |S| (1-u)^{|S|-1} f̂(S)² is convex on [0, 1].

theorem cvg_L_convexOn (p : ℝ) (φ : ConfigSpace ι → Bool) :
    ConvexOn ℝ (Icc (0 : ℝ) 1)
      (fun u => ∑ S : Finset ι, 4 * (S.card : ℝ) * (1 - u) ^ (S.card - 1)
        * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)

Uses 4 · Used by 1

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

Proof usesFinite sum of convex functions is convex · Convexity of \((1 - u)^k\) on \((0, 1)\)

Used byCapped estimate on \((0, 1)\) from concavity of the right side

TheoremConcavity of \(\exp(m u/(2-u))\) for \(-1 \le m \le 0\)#✓fully proved

u ↦ exp (m · u/(2-u)) is concave on [0, 1] for -1 ≤ m ≤ 0.

theorem cvg_Q_concaveOn {m : ℝ} (hm0 : m ≤ 0) (hm1 : -1 ≤ m) :
    ConcaveOn ℝ (Icc (0 : ℝ) 1) (fun u : ℝ => Real.exp (m * (u / (2 - u))))

Used by 1

Used byConcavity of \(\delta^{u/(2-u)} T\) for \(e^{-1} \le \delta \le 1\)

TheoremConcavity of \(\delta^{u/(2-u)} T\) for \(e^{-1} \le \delta \le 1\)#✓fully proved

u ↦ δ^{u/(2-u)} T is concave on [0, 1] for e^{-1} ≤ δ ≤ 1 and T ≥ 0.

theorem cvg_R_concaveOn {δ T : ℝ} (hδlo : Real.exp (-1) ≤ δ) (hδhi : δ ≤ 1) (hT : 0 ≤ T) :
    ConcaveOn ℝ (Icc (0 : ℝ) 1) (fun u : ℝ => δ ^ (u / (2 - u)) * T)

Uses 1 · Used by 1

Proof usesConcavity of \(\exp(m u/(2-u))\) for \(-1 \le m \le 0\)

Used byCapped estimate when the maximal influence is at least \(e^{-1}\)

TheoremCapped estimate on \((0, 1)\) from concavity of the right side#✓fully proved

If the right side of the capped estimate is concave in u, the estimate holds on (0, 1).

theorem cvg_openResidue_of_concaveR [Nonempty ι] {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool)
    (hconc : ConcaveOn ℝ (Icc (0 : ℝ) 1)
      (fun u => (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
        ^ (u / (2 - u)) * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)))
    {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)
      ≤ (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (u / (2 - u))
        * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 9 · Used by 1

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 usesConvexity of the damped total weight · Nonpositivity of a convex function from its endpoint values · Damped total weight at \(u = 0\) is at most the total influence · Capped estimate at the endpoint \(u = 1\)

Used byCapped estimate when the maximal influence is at least \(e^{-1}\)

TheoremMaximal influence of a Boolean function is at most one#✓fully proved

The maximal influence of a Boolean function is at most 1.

theorem cvg_maxInfl_le_one [Nonempty ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
    (φ : ConfigSpace ι → Bool) :
    maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0) ≤ 1

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Maximal 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

Used byCapped estimate when the maximal influence is at least \(e^{-1}\)

TheoremCapped estimate when the maximal influence is at least \(e^{-1}\)#✓fully proved

The capped estimate holds for all u ∈ (0, 1) when the maximal influence is at least e^{-1}.

theorem cvg_openResidue_largeDelta [Nonempty ι] {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (φ : ConfigSpace ι → Bool)
    (hδlo : Real.exp (-1) ≤ maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
    {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)
      ≤ (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (u / (2 - u))
        * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 14 · Used by 1

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 · Concavity of \(\delta^{u/(2-u)} T\) for \(e^{-1} \le \delta \le 1\) · Maximal influence of a Boolean function is at most one · Capped estimate on \((0, 1)\) from concavity of the right side · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used bySmall-influence case implies the open-interval case

DefinitionSmall-influence residual case of the capped estimate#✓fully proved

The capped estimate for all p ∈ (1/2, q) with p < 1, all Boolean functions with maximal influence δ < e^{-1}, and all u ∈ (0, 1).

def cvg_smallDeltaResidue (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 →
      (∑ 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 4

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 byLow-degree case implies the small-influence case · Small-influence case implies the full capped estimate on \((1/2, q)\) · Small-influence case implies the open-interval case · Low-range case implies the small-influence case

TheoremSmall-influence case implies the open-interval case#✓fully proved

cvg_smallDeltaResidue q implies frh_openResidue q.

theorem cvg_openResidue_of_smallDelta {q : ℝ}
    (H : cvg_smallDeltaResidue q) : frh_openResidue q

Uses 8 · Used by 1

Statement usesSmall-influence residual case of the capped estimate · Open-interval residual case of the capped estimate

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Capped estimate when the maximal influence is at least \(e^{-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)\)

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

cvg_smallDeltaResidue q implies mxd_martingaleHC_statement q.

theorem cvg_martingaleHC_of_smallDelta {q : ℝ}
    (H : cvg_smallDeltaResidue q) : mxd_martingaleHC_statement q

Uses 4 · Used by 2

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

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

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

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.