ProbabilityLikelihood.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Likelihood of an actual move of colors

The full guarded profile records every changed coordinate exactly once. Grouping the coordinate likelihood factors by that profile gives the precise ratio used by the selector estimate.

theorem OAI.TalagrandThreshold.prod_profile_eq_prod_changes line 28

Source documentation

Group a product over changed vertices by the actual full profile.

theorem prod_profile_eq_prod_changes (a z : Coloring α s)
    (F : Color s → Color s → ℝ) :
    (∏ i : Fin s, ∏ h : Color s, F i.castSucc h ^ profile a z i h) =
      ∏ x ∈ changes a z, F (z x) (a x) := by
…

Mentions: OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Color

theorem OAI.TalagrandThreshold.pow_profileSize_eq_prod_changes line 79
Source documentation
The profile exponent is the product of one p-factor per actual changed vertex.
```
theorem pow_profileSize_eq_prod_changes (p : ℝ) (a z : Coloring α s) :
    p ^ profileSize (profile a z) = ∏ _x ∈ changes a z, p := by
…
```
Mentions: OAI.TalagrandThreshold.Coloring
theorem OAI.TalagrandThreshold.colorMass_profile_likelihood line 90
Source documentation
Exact likelihood regrouping for the original independent color law and an actual move to earlier colors. Each source row retains all original-color counts.
```
theorem colorMass_profile_likelihood (p : ℝ) (s : ℕ) (hp : 0 < p)
    (hs : p * scaleSum s ≤ 1 / 2) (a z : Coloring α s) (haz : Selector.Earlier a z) :
    p ^ Selector.profileSize (Selector.profile a z) * colorMass p s a =
      colorMass p s z * ∏ i : Fin s,
        ((p / colorProb p s i.castSucc) ^ Selector.rowCount (Selector.profile a z) i *
          ∏ h : Color s, (colorProb p s h) ^ Selector.profile a z i h) := by
…
```
Mentions: OAI.TalagrandThreshold.scaleSum, OAI.TalagrandThreshold.Coloring, OAI.TalagrandThreshold.Selector.Earlier, OAI.TalagrandThreshold.Selector.profileSize, OAI.TalagrandThreshold.Selector.profile, OAI.TalagrandThreshold.colorMass, OAI.TalagrandThreshold.colorProb, OAI.TalagrandThreshold.Selector.rowCount, OAI.TalagrandThreshold.Color