FiniteFibers.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite partitions by a key

The fibers indexed by the image of a finite source partition that source. Filtering the source commutes with taking fibers, so the same partition identities apply to restrictions of a weighted sum.

def OAI.TalagrandDiscreteConvexity.FiniteFibers.fiber line 20
Source documentation
The elements of A with the specified key.
```
def fiber (A : Finset α) (key : α → β) (b : β) : Finset α :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b
def OAI.TalagrandDiscreteConvexity.FiniteFibers.keys line 24
Source documentation
Exactly the keys attained by the finite source.
```
def keys (A : Finset α) (key : α → β) : Finset β :=
…
```
theorem OAI.TalagrandDiscreteConvexity.FiniteFibers.mem_fiber line 28
theorem OAI.TalagrandDiscreteConvexity.FiniteFibers.mem_keys line 33
theorem OAI.TalagrandDiscreteConvexity.FiniteFibers.fiber_subset line 37
theorem OAI.TalagrandDiscreteConvexity.FiniteFibers.key_eq_of_mem_fiber line 41
theorem OAI.TalagrandDiscreteConvexity.FiniteFibers.fiber_nonempty_iff line 46
theorem OAI.TalagrandDiscreteConvexity.FiniteFibers.filter_fiber line 51
Source documentation
Restricting the source commutes with taking a fiber.
```
theorem filter_fiber (A : Finset α) (key : α → β) (b : β)
    (P : α → Prop) [DecidablePred P] :
    fiber (A.filter P) key b = (fiber A key b).filter P :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.FiniteFibers.fiber
theorem OAI.TalagrandDiscreteConvexity.FiniteFibers.sum_fibers line 59
Source documentation
Summing the fibers over the attained keys counts each source element once.
```
theorem sum_fibers (A : Finset α) (key : α → β) (f : α → M) :
    (∑ b ∈ keys A key, ∑ a ∈ fiber A key b, f a) = ∑ a ∈ A, f a := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.FiniteFibers.keys, OAI.TalagrandDiscreteConvexity.FiniteFibers.fiber
theorem OAI.TalagrandDiscreteConvexity.FiniteFibers.sum_filter_fibers line 65
Source documentation
The same partition identity after restricting every fiber by a predicate.
```
theorem sum_filter_fibers (A : Finset α) (key : α → β)
    (P : α → Prop) [DecidablePred P] (f : α → M) :
    (∑ b ∈ keys A key, ∑ a ∈ (fiber A key b).filter P, f a) =
      ∑ a ∈ A.filter P, f a := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.FiniteFibers.keys, OAI.TalagrandDiscreteConvexity.FiniteFibers.fiber
theorem OAI.TalagrandDiscreteConvexity.FiniteFibers.sum_filter_eq_sum_fibers line 78
Source documentation
A restricted sum decomposed into the bins of the original source.
```
theorem sum_filter_eq_sum_fibers (A : Finset α) (key : α → β)
    (P : α → Prop) [DecidablePred P] (f : α → M) :
    (∑ a ∈ A.filter P, f a) =
      ∑ b ∈ keys A key, ∑ a ∈ (fiber A key b).filter P, f a :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.FiniteFibers.keys, OAI.TalagrandDiscreteConvexity.FiniteFibers.fiber