OAI/Combinatorics/ExpectationThreshold/ColorArithmetic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization of the profile coefficient

At level i+1, the color probability is 256^(i+1)*p. Its likelihood factor cancels the density and turns the counting factor 3*4^(i+1) into the geometric coefficient 3/64^(i+1).

  1. theorem OAI.TalagrandThreshold.profile_coefficient_eq line 18
  2. theorem OAI.TalagrandThreshold.profile_coefficient_pow_eq line 34