ColorMean.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The mean of the numerical color variable

The variable at color c is 512^4 / 512^(c.val+1). This quotient represents a possibly negative integral exponent without natural subtraction. The computation includes the residual last color and also applies when the selected number of scales is zero.

theorem OAI.TalagrandThreshold.color_mean_row line 21

theorem OAI.TalagrandThreshold.color_mean_eq line 32

Source documentation

The exact finite-color mean, including the residual last color.

theorem color_mean_eq (p : ℝ) (s : ℕ) :
    (∑ c : Color s,
      colorProb p s c * ((512 : ℝ) ^ 4 / (512 : ℝ) ^ (c.val + 1))) =
      (512 : ℝ) ^ 4 *
        (p * (∑ i : Fin s, (1 / 2 : ℝ) ^ (i.val + 1)) +
          (1 - p * scaleSum s) * (1 / (512 : ℝ) ^ (s + 1))) := by
…

Mentions: OAI.TalagrandThreshold.Color, OAI.TalagrandThreshold.colorProb, OAI.TalagrandThreshold.scaleSum

theorem OAI.TalagrandThreshold.color_mean_le line 47

Source documentation

Maximality of the scale makes the common mean at most 5 * 512^4 * p.

theorem color_mean_le {p : ℝ} (hp : 0 < p) {s : ℕ}
    (_hs : p * scaleSum s ≤ 1 / 2)
    (hnext : 1 / 2 < p * scaleSum (s + 1)) :
    (∑ c : Color s,
      colorProb p s c * ((512 : ℝ) ^ 4 / (512 : ℝ) ^ (c.val + 1))) ≤
      5 * (512 : ℝ) ^ 4 * p := by
…

Mentions: OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Color, OAI.TalagrandThreshold.colorProb

theorem OAI.TalagrandThreshold.rounding_constant_pos line 69

theorem OAI.TalagrandThreshold.five_Bfour_mul_scaled_density line 72

Source documentation

The leading constant is 25.

theorem five_Bfour_mul_scaled_density (r : ℝ) :
    5 * (512 : ℝ) ^ 4 * (r / ((25 : ℝ) * (512 : ℝ) ^ 4)) = r / 5 := by
…

theorem OAI.TalagrandThreshold.color_mean_le_r_div_five line 78

Source documentation

The mean bound at the exact density used for rounding.

theorem color_mean_le_r_div_five {r : ℝ} (hr : 0 < r) {s : ℕ}
    (hs : (r / ((25 : ℝ) * (512 : ℝ) ^ 4)) * scaleSum s ≤ 1 / 2)
    (hnext : 1 / 2 < (r / ((25 : ℝ) * (512 : ℝ) ^ 4)) * scaleSum (s + 1)) :
    (∑ c : Color s,
      colorProb (r / ((25 : ℝ) * (512 : ℝ) ^ 4)) s c *
        ((512 : ℝ) ^ 4 / (512 : ℝ) ^ (c.val + 1))) ≤ r / 5 := by
…

Mentions: OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Color, OAI.TalagrandThreshold.colorProb