ProbabilitySubsetProduct.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Moments of products on a subset of coordinates

Under the actual product law, observables supported on a finite subset factor into their coordinate expectations. Extending the factors by one outside the subset reduces this to the full product moment identity.

theorem OAI.TalagrandThreshold.FiniteLaw.expectation_pi_subset_product line 22
Source documentation
A product on a subset has the product of its actual coordinate means.
```
theorem expectation_pi_subset_product (μ : ∀ i, FiniteLaw (A i))
    (S : Finset I) (f : ∀ i, A i → ℝ) :
    (pi μ).expectation (fun ω => ∏ i ∈ S, f i (ω i)) =
      ∏ i ∈ S, (μ i).expectation (f i) := by
…
```
Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.pi, OAI.TalagrandThreshold.FiniteLaw.expectation
theorem OAI.TalagrandThreshold.FiniteLaw.expectation_pi_subset_product_of_mean line 45
Source documentation
Equal coordinate means give the corresponding power of the subset size.
```
theorem expectation_pi_subset_product_of_mean (μ : ∀ i, FiniteLaw (A i))
    (S : Finset I) (f : ∀ i, A i → ℝ) (a : ℝ)
    (hmean : ∀ i ∈ S, (μ i).expectation (f i) = a) :
    (pi μ).expectation (fun ω => ∏ i ∈ S, f i (ω i)) = a ^ S.card := by
…
```
Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.expectation, OAI.TalagrandThreshold.FiniteLaw.pi
theorem OAI.TalagrandThreshold.FiniteLaw.expectation_pi_subset_product_const line 56
Source documentation
Identically distributed coordinates give a power of their common mean.
```
theorem expectation_pi_subset_product_const {Ω : Type*} [Fintype Ω]
    (μ : FiniteLaw Ω) (S : Finset I) (f : Ω → ℝ) :
    (pi (fun _ : I => μ)).expectation (fun ω => ∏ i ∈ S, f (ω i)) =
      (μ.expectation f) ^ S.card := by
…
```
Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.pi, OAI.TalagrandThreshold.FiniteLaw.expectation