OAI/NumberTheory/EgyptianFractions/SampleWordTransfer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.RandomProducts.typed_sample_event_card line 9

   Source documentation

   The finite-set word model agrees exactly with independent samples in the alphabet subtype.

   theorem typed_sample_event_card {α : Type*} [DecidableEq α]
       (P : Finset α) (t : ℕ) (R : (Fin t → α) → Prop) [DecidablePred R] :
       Fintype.card {f : Fin t → P // R (fun i => (f i : α))} =
         ((sampleWords P t).filter R).card := by
   …

   Mentions: OAI.Problem337.RandomProducts.sampleWords

2. theorem OAI.Problem337.RandomProducts.typed_product_event_card line 34

   Source documentation

   Reindexing a finite sample index type preserves all product-dependent event counts.

   theorem typed_product_event_card {ι : Type*} [Fintype ι] [DecidableEq ι]
       (P : Finset ℕ) (R : ℕ → Prop) [DecidablePred R] :
       Fintype.card {f : ι → P // R (∏ i, (f i : ℕ))} =
         ((sampleWords P (Fintype.card ι)).filter (fun f => R (∏ i, f i))).card := by
   …

   Mentions: OAI.Problem337.RandomProducts.sampleWords

3. theorem OAI.Problem337.RandomProducts.typed_product_event_probability line 52

   Source documentation

   Normalized version, suitable for an exposed block of independent typed samples.

   theorem typed_product_event_probability {ι : Type*} [Fintype ι] [DecidableEq ι]
       (P : Finset ℕ) (R : ℕ → Prop) [DecidablePred R] :
       (Fintype.card {f : ι → P // R (∏ i, (f i : ℕ))} : ℝ) /
           (Fintype.card (ι → P) : ℝ) =
         (((sampleWords P (Fintype.card ι)).filter (fun f => R (∏ i, f i))).card : ℝ) /
           (P.card : ℝ) ^ (Fintype.card ι) := by
   …

   Mentions: OAI.Problem337.RandomProducts.sampleWords

4. theorem OAI.Problem337.RandomProducts.restriction_event_probability line 62

   Source documentation

   Independent uniform sampling has uniform marginals on every subset of coordinates.

   theorem restriction_event_probability {ι β : Type*} [Fintype ι] [DecidableEq ι]
       [Fintype β] [Nonempty β] (s : Finset ι) (R : (s → β) → Prop) [DecidablePred R] :
       (Fintype.card {f : ι → β // R (fun i : s => f i)} : ℝ) /
           (Fintype.card (ι → β) : ℝ) =
         (Fintype.card {g : s → β // R g} : ℝ) / (Fintype.card (s → β) : ℝ) := by
   …

5. theorem OAI.Problem337.RandomProducts.restricted_product_event_probability line 84

   Source documentation

   A product over a subset of labelled coordinates has the ordinary independent-product law.

   theorem restricted_product_event_probability {ι : Type*} [Fintype ι] [DecidableEq ι]
       (P : Finset ℕ) [Nonempty P] (s : Finset ι) (R : ℕ → Prop) [DecidablePred R] :
       (Fintype.card {f : ι → P // R (∏ i : s, (f i : ℕ))} : ℝ) /
           (Fintype.card (ι → P) : ℝ) =
         (((sampleWords P (Fintype.card s)).filter (fun f => R (∏ i, f i))).card : ℝ) /
           (P.card : ℝ) ^ (Fintype.card s) := by
   …

   Mentions: OAI.Problem337.RandomProducts.sampleWords