OAI/NumberTheory/EgyptianFractions/RandomExposure.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.RandomExposure.exists_two_disjoint_subsets line 10

   Source documentation

   Two disjoint equally sized groups can be selected from a sufficiently large finite set.

   theorem exists_two_disjoint_subsets {α : Type*} [DecidableEq α]
       (D : Finset α) (s : ℕ) (hsize : 2 * s ≤ D.card) :
       ∃ A B : Finset α, A ⊆ D ∧ B ⊆ D ∧ Disjoint A B ∧ A.card = s ∧ B.card = s := by
   …

   Mentions: OAI.Problem337.D

2. theorem OAI.Problem337.RandomExposure.exists_differing_blocks line 24

   Source documentation

   Select the two fresh groups for a pair of Boolean words with enough differing positions.

   theorem exists_differing_blocks {ι : Type*} [Fintype ι] [DecidableEq ι]
       (I J : ι → Bool) (s : ℕ)
       (hsize : 2 * s ≤ (Finset.univ.filter fun i => I i ≠ J i).card) :
       ∃ A B : Finset ι, Disjoint A B ∧ A.card = s ∧ B.card = s ∧
         (∀ i ∈ A, I i ≠ J i) ∧ (∀ i ∈ B, I i ≠ J i) := by
   …

3. def OAI.Problem337.RandomExposure.splitSample line 38

   Source documentation

   Reindex all labelled samples into two free blocks and their exposed complement.

   def splitSample {α β : Type*} [DecidableEq α] (A B : Finset α) (hAB : Disjoint A B) :
       (α → β) ≃ ((A → β) × (B → β) × ({i : α // i ∉ A ∧ i ∉ B} → β)) where
   …

4. theorem OAI.Problem337.RandomExposure.splitSample_symm_left line 59
5. theorem OAI.Problem337.RandomExposure.splitSample_symm_right line 65
6. theorem OAI.Problem337.RandomExposure.splitSample_symm_exposed line 72
7. def OAI.Problem337.RandomExposure.splitSampleExposedFirst line 80

   Source documentation

   The same exposure equivalence with exposed samples first, ready for conditional averages.

   def splitSampleExposedFirst {α β : Type*} [DecidableEq α]
       (A B : Finset α) (hAB : Disjoint A B) :
       (α → β) ≃ (({i : α // i ∉ A ∧ i ∉ B} → β) × ((A → β) × (B → β))) :=
   …

8. theorem OAI.Problem337.RandomExposure.splitSampleExposedFirst_symm line 86
9. theorem OAI.Problem337.RandomExposure.sum_splitSample line 93

   Source documentation

   Fubini's identity for the finite exposure partition; no independence assumption is hidden.

   theorem sum_splitSample {α β M : Type*} [Fintype α] [DecidableEq α] [Fintype β]
       [AddCommMonoid M] (A B : Finset α) (hAB : Disjoint A B) (F : (α → β) → M) :
       (∑ p, F p) = ∑ a : A → β, ∑ b : B → β,
         ∑ c : {i : α // i ∉ A ∧ i ∉ B} → β,
           F ((splitSample A B hAB).symm (a, b, c)) := by
   …

   Mentions: OAI.Problem337.F, OAI.Problem337.RandomExposure.splitSample

10. def OAI.Problem337.RandomExposure.selectedLabels line 103

    Source documentation

    The labelled coordinates selected by a Boolean word on a given coordinate set.

    def selectedLabels {ι : Type*} [DecidableEq ι] (I : ι → Bool) (A : Finset ι) :
        Finset (ι × Bool) := A.image (fun i => (i, I i))

11. theorem OAI.Problem337.RandomExposure.mem_selectedLabels line 106
12. theorem OAI.Problem337.RandomExposure.selectedLabels_card line 111
13. theorem OAI.Problem337.RandomExposure.selectedLabels_disjoint line 117
14. theorem OAI.Problem337.RandomExposure.product_selectedLabels line 125
15. theorem OAI.Problem337.RandomExposure.selected_product_factorization line 135

    Source documentation

    Factor the first word's product into exposed and two free coordinate groups.

    theorem selected_product_factorization {ι M : Type*} [Fintype ι] [DecidableEq ι]
        [CommMonoid M] (I : ι → Bool) (A B : Finset ι) (hAB : Disjoint A B)
        (p : ι × Bool → M) :
        (∏ i, p (i, I i)) =
          (∏ i ∈ Finset.univ \ (A ∪ B), p (i, I i)) *
          (∏ i ∈ A, p (i, I i)) * (∏ i ∈ B, p (i, I i)) := by
    …

16. theorem OAI.Problem337.RandomExposure.other_word_exposed line 146

    Source documentation

    The other word uses none of the free labelled samples when the coordinates differ.

    theorem other_word_exposed {ι : Type*} [DecidableEq ι]
        (I J : ι → Bool) (A : Finset ι) (hdiff : ∀ i ∈ A, I i ≠ J i) (i : ι) :
        (i, J i) ∉ selectedLabels I A := by
    …

    Mentions: OAI.Problem337.RandomExposure.selectedLabels

17. theorem OAI.Problem337.RandomExposure.other_product_invariant line 154

    Source documentation

    Products selected by the other word are unchanged by varying only free samples.

    theorem other_product_invariant {ι M : Type*} [Fintype ι] [DecidableEq ι] [CommMonoid M]
        (I J : ι → Bool) (A B : Finset ι)
        (hA : ∀ i ∈ A, I i ≠ J i) (hB : ∀ i ∈ B, I i ≠ J i)
        (p q : ι × Bool → M)
        (hpq : ∀ z, z ∉ selectedLabels I A → z ∉ selectedLabels I B → p z = q z) :
        (∏ i, p (i, J i)) = ∏ i, q (i, J i) := by
    …

    Mentions: OAI.Problem337.RandomExposure.selectedLabels

18. abbrev OAI.Problem337.RandomExposure.ExposedLabel line 165

    Source documentation

    The exposed label set.

    abbrev ExposedLabel {ι : Type*} [DecidableEq ι]
        (I : ι → Bool) (A B : Finset ι) :=
    …

19. def OAI.Problem337.RandomExposure.outsideSelectedLabel line 170

    Source documentation

    Every remaining coordinate of the first word is an exposed labelled sample.

    def outsideSelectedLabel {ι : Type*} [Fintype ι] [DecidableEq ι]
        (I : ι → Bool) (A B : Finset ι) (i : ↥(Finset.univ \ (A ∪ B))) : ExposedLabel I A B := by
    …

    Mentions: OAI.Problem337.RandomExposure.ExposedLabel

20. theorem OAI.Problem337.RandomExposure.outsideSelectedLabel_injective line 177
21. theorem OAI.Problem337.RandomExposure.outside_card line 183
22. def OAI.Problem337.RandomExposure.exposedFirstProduct line 190

    Source documentation

    The first word's exposed factor, with an explicit product over the non-fresh coordinates.

    def exposedFirstProduct {ι β M : Type*} [Fintype ι] [DecidableEq ι] [CommMonoid M]
        (v : β → M) (I : ι → Bool) (A B : Finset ι) (c : ExposedLabel I A B → β) : M :=
    …

    Mentions: OAI.Problem337.v, OAI.Problem337.RandomExposure.ExposedLabel

23. def OAI.Problem337.RandomExposure.exposedOtherProduct line 195

    Source documentation

    All coordinates of the second word remain exposed.

    def exposedOtherProduct {ι β M : Type*} [Fintype ι] [DecidableEq ι] [CommMonoid M]
        (v : β → M) (I J : ι → Bool) (A B : Finset ι)
        (hA : ∀ i ∈ A, I i ≠ J i) (hB : ∀ i ∈ B, I i ≠ J i)
        (c : ExposedLabel I A B → β) : M :=
    …

    Mentions: OAI.Problem337.v, OAI.Problem337.RandomExposure.ExposedLabel

24. theorem OAI.Problem337.RandomExposure.exposed_first_factor_formula line 202

    Source documentation

    Explicit form of the exposed factor, useful for bounding the bad gcd event.

    theorem exposed_first_factor_formula {ι β M : Type*} [Fintype ι] [DecidableEq ι]
        [CommMonoid M] (v : β → M) (I : ι → Bool) (A B : Finset ι) (hAB : Disjoint A B)
        (a : selectedLabels I A → β) (b : selectedLabels I B → β) (c : ExposedLabel I A B → β) :
        (∏ i ∈ Finset.univ \ (A ∪ B),
          v ((splitSample _ _ (selectedLabels_disjoint I hAB)).symm (a, b, c) (i, I i))) =
          exposedFirstProduct v I A B c := by
    …

    Mentions: OAI.Problem337.v, OAI.Problem337.RandomExposure.selectedLabels, OAI.Problem337.RandomExposure.ExposedLabel, OAI.Problem337.RandomExposure.splitSample, OAI.Problem337.RandomExposure.selectedLabels_disjoint, OAI.Problem337.RandomExposure.exposedFirstProduct

25. theorem OAI.Problem337.RandomExposure.exposed_other_factor_formula line 214
26. theorem OAI.Problem337.RandomExposure.exposed_product_factorization line 227

    Source documentation

    The exact exposed-variable factorization used in the random-product correlation argument. The two free blocks affect only the first word, each through its own product.

    theorem exposed_product_factorization {ι β M : Type*} [Fintype ι] [DecidableEq ι]
        [Nonempty β] [CommMonoid M] (v : β → M)
        (I J : ι → Bool) (A B : Finset ι) (hAB : Disjoint A B)
        (hA : ∀ i ∈ A, I i ≠ J i) (hB : ∀ i ∈ B, I i ≠ J i) :
        let E := splitSample (β := β) (selectedLabels I A) (selectedLabels I B)
    …

    Mentions: OAI.Problem337.v, OAI.Problem337.RandomExposure.splitSample, OAI.Problem337.RandomExposure.selectedLabels