ProbabilityProduct.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Marginals and pushforwards of finite product laws

Product moments, one-coordinate marginals, and pushforward identities follow from the weights of the finite laws.

theorem OAI.TalagrandThreshold.FiniteLaw.expectation_pi_product line 26
Source documentation
Product observables factor under the product of the given finite laws.
```
theorem expectation_pi_product (μ : ∀ i, FiniteLaw (A i))
    (f : ∀ i, A i → ℝ) :
    (pi μ).expectation (fun ω => ∏ i, f i (ω i)) =
      ∏ i, (μ i).expectation (f i) := by
…
```
Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.pi, OAI.TalagrandThreshold.FiniteLaw.expectation
theorem OAI.TalagrandThreshold.FiniteLaw.expectation_pi_coordinate line 36
Source documentation
A coordinate of the product law has exactly its prescribed marginal.
```
theorem expectation_pi_coordinate (μ : ∀ i, FiniteLaw (A i))
    (i : I) (f : A i → ℝ) :
    (pi μ).expectation (fun ω => f (ω i)) = (μ i).expectation f := by
…
```
Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.pi, OAI.TalagrandThreshold.FiniteLaw.expectation
theorem OAI.TalagrandThreshold.FiniteLaw.prob_pi_coordinate line 59
Source documentation
Events depending on one coordinate have their original probabilities.
```
theorem prob_pi_coordinate (μ : ∀ i, FiniteLaw (A i))
    (i : I) (P : A i → Prop) :
    (pi μ).prob (fun ω => P (ω i)) = (μ i).prob P := by
…
```
Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.pi, OAI.TalagrandThreshold.FiniteLaw.prob
theorem OAI.TalagrandThreshold.FiniteLaw.prob_pi line 67
Source documentation
A cylinder event has the product of its coordinate probabilities.
```
theorem prob_pi (μ : ∀ i, FiniteLaw (A i)) (P : ∀ i, A i → Prop) :
    (pi μ).prob (fun ω => ∀ i, P i (ω i)) = ∏ i, (μ i).prob (P i) := by
…
```
Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.pi, OAI.TalagrandThreshold.FiniteLaw.prob
theorem OAI.TalagrandThreshold.FiniteLaw.prob_prod line 90
Source documentation
Rectangle events factor under the binary product law.
```
theorem prob_prod (μ : FiniteLaw Ω) (ν : FiniteLaw Γ)
    (P : Ω → Prop) (Q : Γ → Prop) :
    (μ.prod ν).prob (fun z => P z.1 ∧ Q z.2) = μ.prob P * ν.prob Q := by
…
```
Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.prob
def OAI.TalagrandThreshold.FiniteLaw.map line 108
Source documentation
Pushforward by summing the source weights in each fiber.
```
def map (μ : FiniteLaw Ω) (f : Ω → Γ) : FiniteLaw Γ where
…
```
Mentions: OAI.TalagrandThreshold.FiniteLaw
theorem OAI.TalagrandThreshold.FiniteLaw.map_weight line 118
theorem OAI.TalagrandThreshold.FiniteLaw.map_weight_eq_prob line 121
theorem OAI.TalagrandThreshold.FiniteLaw.expectation_map line 125
Source documentation
Observables of a pushed law are evaluated along the defining map.
```
theorem expectation_map (μ : FiniteLaw Ω) (f : Ω → Γ) (g : Γ → ℝ) :
    (map μ f).expectation g = μ.expectation (fun ω => g (f ω)) := by
…
```
Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.map, OAI.TalagrandThreshold.FiniteLaw.expectation
theorem OAI.TalagrandThreshold.FiniteLaw.prob_map line 135
Source documentation
The probability of an event under a pushed law is its preimage probability.
```
theorem prob_map (μ : FiniteLaw Ω) (f : Ω → Γ) (P : Γ → Prop) :
    (map μ f).prob P = μ.prob (fun ω => P (f ω)) := by
…
```
Mentions: OAI.TalagrandThreshold.FiniteLaw, OAI.TalagrandThreshold.FiniteLaw.map, OAI.TalagrandThreshold.FiniteLaw.prob