ProductProbability.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Marginals and pushforwards of finite product laws

All identities below follow from the weights of the actual finite laws.

theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation_pi_product line 25
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.TalagrandDiscreteConvexity.FiniteLaw, OAI.TalagrandDiscreteConvexity.FiniteLaw.pi, OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation
theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation_pi_coordinate line 35
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.TalagrandDiscreteConvexity.FiniteLaw, OAI.TalagrandDiscreteConvexity.FiniteLaw.pi, OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation
theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_pi_coordinate line 58
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.TalagrandDiscreteConvexity.FiniteLaw, OAI.TalagrandDiscreteConvexity.FiniteLaw.pi, OAI.TalagrandDiscreteConvexity.FiniteLaw.prob
theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_pi line 66
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.TalagrandDiscreteConvexity.FiniteLaw, OAI.TalagrandDiscreteConvexity.FiniteLaw.pi, OAI.TalagrandDiscreteConvexity.FiniteLaw.prob
theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_prod line 89
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.TalagrandDiscreteConvexity.FiniteLaw, OAI.TalagrandDiscreteConvexity.FiniteLaw.prob
def OAI.TalagrandDiscreteConvexity.FiniteLaw.map line 107
Source documentation
Pushforward by summing the source weights in each fiber.
```
def map (μ : FiniteLaw Ω) (f : Ω → Γ) : FiniteLaw Γ where
…
```
Mentions: OAI.TalagrandDiscreteConvexity.FiniteLaw
theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.map_weight line 117
theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.map_weight_eq_prob line 120
theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation_map line 124
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.TalagrandDiscreteConvexity.FiniteLaw, OAI.TalagrandDiscreteConvexity.FiniteLaw.map, OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation
theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_map line 134
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.TalagrandDiscreteConvexity.FiniteLaw, OAI.TalagrandDiscreteConvexity.FiniteLaw.map, OAI.TalagrandDiscreteConvexity.FiniteLaw.prob