CoordinateObservations.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Boolean observations of finite product laws

Independent Boolean observations with common success probability have the Bernoulli law on subsets, both on individual atoms and on arbitrary families.

theorem OAI.TalagrandDiscreteConvexity.prob_pi_cubeSet_eq_mass line 22
Source documentation
A specified set of successful coordinate observations has its Bernoulli mass.
```
theorem prob_pi_cubeSet_eq_mass (μ : ∀ i, FiniteLaw (Ω i))
    (obs : ∀ i, Ω i → Bool) (p : ℝ)
    (hobs : ∀ i, (μ i).prob (fun w => obs i w = true) = p) (s : Finset α) :
    (FiniteLaw.pi μ).prob (fun ω => cubeSet (fun i => obs i (ω i)) = s) =
      bernoulliMass p s := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.FiniteLaw, OAI.TalagrandDiscreteConvexity.w, OAI.TalagrandDiscreteConvexity.FiniteLaw.pi, OAI.TalagrandDiscreteConvexity.cubeSet, OAI.TalagrandDiscreteConvexity.bernoulliMass
theorem OAI.TalagrandDiscreteConvexity.prob_pi_cubeSet_mem_family line 50
Source documentation
Membership of the observed set in a family has exactly its Bernoulli measure.
```
theorem prob_pi_cubeSet_mem_family (μ : ∀ i, FiniteLaw (Ω i))
    (obs : ∀ i, Ω i → Bool) (p : ℝ)
    (hobs : ∀ i, (μ i).prob (fun w => obs i w = true) = p) (D : Family α) :
    (FiniteLaw.pi μ).prob (fun ω => cubeSet (fun i => obs i (ω i)) ∈ D) =
      familyMeasure p D := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.FiniteLaw, OAI.TalagrandDiscreteConvexity.w, OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.FiniteLaw.pi, OAI.TalagrandDiscreteConvexity.cubeSet, OAI.TalagrandDiscreteConvexity.familyMeasure