Degree truncation of the capped estimate under p-biased measures

TheoremFourier total weight equals \(4p(1-p)\) times the total influence#✓fully proved

The Fourier total weight under μ_p: 4 ∑_S |S| f̂(S)² = 4p(1-p) ∑ₑ Infₑ.

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

Uses 6 · Used by 1

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 byBound on the high-degree part of the damped total weight

TheoremBound on the high-degree part of the damped total weight#✓fully proved

The Fourier part of degree greater than k contributes at most 4p(1-p)(1-u)^k ∑ₑ Infₑ to the damped total weight.

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

Uses 5 · Used by 1

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

Proof usesFourier total weight equals \(4p(1-p)\) times the total influence

Used byCapped estimate from its low-degree part

TheoremCapped estimate from its low-degree part#✓fully proved

The capped estimate follows from a bound on its part of degree at most k.

theorem dtr_trunc_split {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (φ : ConfigSpace ι → Bool)
    {u : ℝ} (hu0 : 0 < u) (hu1 : u < 1) (k : ℕ) :
    (∑ S : Finset ι, 4 * (S.card : ℝ) * (1 - u) ^ (S.card - 1)
        * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
      ≤ (4 * ∑ S ∈ univ.filter (fun S : Finset ι => 1 ≤ S.card ∧ S.card ≤ k),
            (S.card : ℝ) * (1 - u) ^ (S.card - 1)
              * (ptn_coeff p (fun ω => if φ ω then (1 : ℝ) else 0) S) ^ 2)
        + (1 - u) ^ k * (4 * p * (1 - p)
            * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))

Uses 5 · Used by 1

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

Proof usesBound on the high-degree part of the damped total weight

Used byLow-degree case implies the low-range case

DefinitionExponent \(q^{\ast}(p, u)\) paired with the damping#✓fully proved

The exponent q*(p, u) = 1 + (1-u)/(4p(1-p)) paired with the damping 1 - u.

noncomputable def dtr_qstar (p u : ℝ) : ℝ := 1 + (1 - u) / (4 * p * (1 - p))

Used by 2

Used byLow-degree case implies the low-range case · Low-degree residual case of the capped estimate

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

The low-degree form of the capped estimate for every p ∈ (1/2, q) with p < 1, small maximal influence δ < e^{-1}, and parameters u outside the range handled by CappedExponentGap.

StatMech.Probability.dtr_lowDegreeResidue · 17 lines

def dtr_lowDegreeResidue (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 / dtr_qstar p u - 1))
            < 4 * (ptn_sigma p) ^ 2) →
        ∃ k : ℕ,
          4 * ∑ S ∈ univ.filter (fun S : Finset E => 1 ≤ S.card ∧ S.card ≤ k),
              (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))
              - 4 * p * (1 - p) * (1 - u) ^ k)
              * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 7 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Exponent \(q^{\ast}(p, u)\) paired with the damping · 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-degree case implies the full capped estimate on \((1/2, q)\) · Low-degree case implies the small-influence case

TheoremLow-degree case implies the low-range case#✓fully proved

dtr_lowDegreeResidue q implies hcq_lowRangeResidue q.

theorem dtr_lowDegree_of_residue {q : ℝ} (H : dtr_lowDegreeResidue q) :
    hcq_lowRangeResidue q

Uses 10 · Used by 1

Statement usesLow-degree residual case of the capped estimate · Low-range residual case of the capped estimate

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Exponent \(q^{\ast}(p, u)\) paired with the damping · Capped estimate from its low-degree part · 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 small-influence case

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

dtr_lowDegreeResidue q implies cvg_smallDeltaResidue q.

theorem dtr_smallDelta_of_residue {q : ℝ} (H : dtr_lowDegreeResidue q) :
    cvg_smallDeltaResidue q

Uses 4 · Used by 1

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

Proof usesLow-degree case implies the low-range case · Low-range case implies the small-influence case

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

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

dtr_lowDegreeResidue q implies mxd_martingaleHC_statement q.

theorem dtr_martingaleHC_of_residue {q : ℝ} (H : dtr_lowDegreeResidue q) :
    mxd_martingaleHC_statement q

Uses 4

Statement usesLow-degree 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-degree case implies the small-influence case

TheoremSome truncation level gives a nonnegative budget#✓fully proved

For δ > 0 the truncation budget δ^{u/(2-u)} - 4p(1-p)(1-u)^k is nonnegative for some k.

theorem dtr_budget_pos {p δ u : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (hu0 : 0 < u) (_hu1 : u < 1)
    (hδ0 : 0 < δ ^ (u / (2 - u))) :
    ∃ k : ℕ, 0 ≤ δ ^ (u / (2 - u)) - 4 * p * (1 - p) * (1 - u) ^ k

Used by 1

Used bySome truncation level makes the low-degree right side nonnegative

TheoremSome truncation level makes the low-degree right side nonnegative#✓fully proved

For δ^{u/(2-u)} > 0 some truncation level k makes the right side of the low-degree bound in dtr_lowDegreeResidue nonnegative.

theorem dtr_residue_c0 {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    {u : ℝ} (hu0 : 0 < u) (hu1 : u < 1)
    {E : Type} [Fintype E] [DecidableEq E] [Nonempty E] (φ : ConfigSpace E → Bool)
    (hδ0 : 0 < (maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0))
        ^ (u / (2 - u))) :
    ∃ k : ℕ, (0 : ℝ)
      ≤ ((maxInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)) ^ (u / (2 - u))
          - 4 * p * (1 - p) * (1 - u) ^ k)
        * totalInfl (OSSS.bernoulliWeight p) (fun ω => if φ ω then (1 : ℝ) else 0)

Uses 11

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 · Some truncation level gives a nonnegative budget · Closing a coordinate of a configuration · Opening a coordinate of a configuration

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.