FiniteProductCounting.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Counting events on disjoint sets of coordinates

The sample space is the actual finite function space U → E, with uniform probability given by cardinality divided by the cardinality of that space. A coordinate-swap bijection proves independence of two events from their literal disjoint supports. Finite intersections then follow by induction. No independence hypothesis or distinctness within an individual tuple is used.

def OAI.MetricEntropyDuality.FiniteProductCounting.DependsOn line 28
Source documentation
Agreement on the named coordinates determines event membership.
```
def DependsOn (S : Finset U) (A : Finset (U → E)) : Prop :=
…
```
def OAI.MetricEntropyDuality.FiniteProductCounting.prob line 32
Source documentation
Uniform probability on the complete finite product sample space.
```
noncomputable def prob (A : Finset (U → E)) : ℝ :=
…
```
def OAI.MetricEntropyDuality.FiniteProductCounting.coordinateSwap line 36
Source documentation
Swap the two assignments outside S, retaining them on S.
```
def coordinateSwap (S : Finset U) (z : (U → E) × (U → E)) :
    (U → E) × (U → E) :=
…
```
theorem OAI.MetricEntropyDuality.FiniteProductCounting.coordinateSwap_involutive line 42
theorem OAI.MetricEntropyDuality.FiniteProductCounting.card_inter_mul_card_sample line 48
Source documentation
The two-event counting identity is a bijection of actual assignments.
```
theorem card_inter_mul_card_sample (S T : Finset U) (A B : Finset (U → E))
    (hA : DependsOn S A) (hB : DependsOn T B) (hST : Disjoint S T) :
    (A ∩ B).card * Fintype.card (U → E) = A.card * B.card := by
…
```
Mentions: OAI.MetricEntropyDuality.FiniteProductCounting.DependsOn
theorem OAI.MetricEntropyDuality.FiniteProductCounting.prob_nonneg line 85
theorem OAI.MetricEntropyDuality.FiniteProductCounting.sample_card_pos line 93
theorem OAI.MetricEntropyDuality.FiniteProductCounting.prob_univ line 97
theorem OAI.MetricEntropyDuality.FiniteProductCounting.prob_inter line 101
Source documentation
Uniform independence is derived from disjoint coordinate supports.
```
theorem prob_inter (S T : Finset U) (A B : Finset (U → E))
    (hA : DependsOn S A) (hB : DependsOn T B) (hST : Disjoint S T) :
    prob (A ∩ B) = prob A * prob B := by
…
```
Mentions: OAI.MetricEntropyDuality.FiniteProductCounting.DependsOn, OAI.MetricEntropyDuality.FiniteProductCounting.prob
def OAI.MetricEntropyDuality.FiniteProductCounting.allEvents line 117
Source documentation
All indexed events hold; the index set and events are kept literally.
```
def allEvents {J : Type uJ} [DecidableEq J] (s : Finset J)
    (A : J → Finset (U → E)) : Finset (U → E) :=
…
```
theorem OAI.MetricEntropyDuality.FiniteProductCounting.mem_allEvents line 121
theorem OAI.MetricEntropyDuality.FiniteProductCounting.allEvents_empty line 126
theorem OAI.MetricEntropyDuality.FiniteProductCounting.allEvents_insert line 131
theorem OAI.MetricEntropyDuality.FiniteProductCounting.dependsOn_allEvents line 137
theorem OAI.MetricEntropyDuality.FiniteProductCounting.prob_allEvents_eq_prod line 156
Source documentation
Every finite family of events on pairwise disjoint supports factors.
```
theorem prob_allEvents_eq_prod {J : Type uJ} [DecidableEq J]
    (s : Finset J) (S : J → Finset U) (A : J → Finset (U → E))
    (hdep : ∀ j ∈ s, DependsOn (S j) (A j))
    (hdisj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) :
    prob (allEvents s A) = ∏ j ∈ s, prob (A j) := by
…
```
Mentions: OAI.MetricEntropyDuality.FiniteProductCounting.DependsOn, OAI.MetricEntropyDuality.FiniteProductCounting.prob, OAI.MetricEntropyDuality.FiniteProductCounting.allEvents
theorem OAI.MetricEntropyDuality.FiniteProductCounting.prob_all_univ_eq_prod line 178
theorem OAI.MetricEntropyDuality.FiniteProductCounting.prob_all_univ_le_pow line 187
Source documentation
The repeated-event bound follows from the proved finite product identity.
```
theorem prob_all_univ_le_pow {w : ℕ} (S : Fin w → Finset U)
    (A : Fin w → Finset (U → E))
    (hdep : ∀ j, DependsOn (S j) (A j))
    (hdisj : Pairwise fun i j => Disjoint (S i) (S j))
    (b : ℝ) (hbound : ∀ j, prob (A j) ≤ b) :
    prob (allEvents Finset.univ A) ≤ b ^ w := by
…
```
Mentions: OAI.MetricEntropyDuality.FiniteProductCounting.DependsOn, OAI.MetricEntropyDuality.FiniteProductCounting.prob, OAI.MetricEntropyDuality.FiniteProductCounting.allEvents