ProbabilityColors.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

The actual independent color law

Colors are indexed from zero; their numerical levels are one larger. The first s colors have masses 256^(i+1) * p, and the final color carries the remaining mass. All laws below use these literal weights.

abbrev OAI.TalagrandThreshold.Color line 21
abbrev OAI.TalagrandThreshold.Coloring line 23
def OAI.TalagrandThreshold.scaleSum line 26
Source documentation
The geometric sum appearing in the admissibility condition.
```
def scaleSum (s : ℕ) : ℝ := ∑ i : Fin s, (256 : ℝ) ^ (i.val + 1)
```
def OAI.TalagrandThreshold.colorProb line 29
Source documentation
The literal single-coordinate probabilities from the selector experiment.
```
def colorProb (p : ℝ) (s : ℕ) (c : Color s) : ℝ :=
…
```
Mentions: OAI.TalagrandThreshold.Color
theorem OAI.TalagrandThreshold.scaleSum_zero line 32
theorem OAI.TalagrandThreshold.scaleSum_nonneg line 35
theorem OAI.TalagrandThreshold.colorProb_castSucc line 38
theorem OAI.TalagrandThreshold.colorProb_last line 42
theorem OAI.TalagrandThreshold.sum_colorProb line 47
Source documentation
Normalization is an algebraic identity, even before assuming positivity.
```
theorem sum_colorProb (p : ℝ) (s : ℕ) : ∑ c : Color s, colorProb p s c = 1 := by
…
```
Mentions: OAI.TalagrandThreshold.Color, OAI.TalagrandThreshold.colorProb
theorem OAI.TalagrandThreshold.colorProb_pos line 54
theorem OAI.TalagrandThreshold.colorProb_nonneg line 61
theorem OAI.TalagrandThreshold.colorProb_le_one line 65
def OAI.TalagrandThreshold.colorLaw line 71
theorem OAI.TalagrandThreshold.colorLaw_weight line 77
theorem OAI.TalagrandThreshold.colorLaw_isPositive line 81
def OAI.TalagrandThreshold.colorMass line 88
Source documentation
Probability mass of a complete coloring, with one factor per vertex.
```
def colorMass (p : ℝ) (s : ℕ) (a : Coloring α s) : ℝ :=
…
```
Mentions: OAI.TalagrandThreshold.Coloring
theorem OAI.TalagrandThreshold.colorMass_pos line 91
theorem OAI.TalagrandThreshold.colorMass_nonneg line 95
theorem OAI.TalagrandThreshold.sum_colorMass line 102
Source documentation
Summing over actual colorings gives total mass one.
```
theorem sum_colorMass (p : ℝ) (s : ℕ) :
    ∑ a : Coloring α s, colorMass p s a = 1 := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.colorMass
def OAI.TalagrandThreshold.coloringLaw line 110
Source documentation
The independent product law on exactly the original vertex set.
```
def coloringLaw (p : ℝ) (s : ℕ) (hp : 0 < p)
    (hs : p * scaleSum s ≤ 1 / 2) : FiniteLaw (Coloring α s) :=
…
```
Mentions: OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.Coloring
theorem OAI.TalagrandThreshold.coloringLaw_weight line 114
theorem OAI.TalagrandThreshold.coloringLaw_isPositive line 118
theorem OAI.TalagrandThreshold.coloringLaw_expectation_coordinate line 124
Source documentation
Coordinate observables have the explicitly specified color marginal.
```
theorem coloringLaw_expectation_coordinate (p : ℝ) (s : ℕ) (hp : 0 < p)
    (hs : p * scaleSum s ≤ 1 / 2) (x : α) (f : Color s → ℝ) :
    (coloringLaw p s hp hs).expectation (fun a => f (a x)) =
      ∑ c : Color s, colorProb p s c * f c :=
…
```
Mentions: OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Color, OAI.TalagrandThreshold.coloringLaw, OAI.TalagrandThreshold.colorProb
theorem OAI.TalagrandThreshold.coloringLaw_expectation_product line 131
Source documentation
Independent coordinate observables factor under the actual coloring law.
```
theorem coloringLaw_expectation_product (p : ℝ) (s : ℕ) (hp : 0 < p)
    (hs : p * scaleSum s ≤ 1 / 2) (f : α → Color s → ℝ) :
    (coloringLaw p s hp hs).expectation (fun a => ∏ x, f x (a x)) =
      ∏ x, ∑ c : Color s, colorProb p s c * f x c :=
…
```
Mentions: OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Color, OAI.TalagrandThreshold.coloringLaw, OAI.TalagrandThreshold.colorProb