OAI/NumberTheory/Ostmann/Construction/SelectedBulkPermutation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.selectedBulkPerm line 13
2. theorem OAI.Ostmann.selectedBulkPerm_bulk line 18
3. theorem OAI.Ostmann.selectedBulkPerm_nonbulk line 25
4. theorem OAI.Ostmann.selectedBulkPerm_symm line 33
5. theorem OAI.Ostmann.selectedBulkPerm_one line 39
6. theorem OAI.Ostmann.selectedBulkPerm_mul line 44
7. def OAI.Ostmann.selectedBulkSample line 51
8. theorem OAI.Ostmann.selectedBulkSample_bulk line 54
9. theorem OAI.Ostmann.selectedBulkSample_nonbulk line 59
10. theorem OAI.Ostmann.selectedBulkSample_one line 64
11. theorem OAI.Ostmann.selectedBulkSample_mul line 69
12. theorem OAI.Ostmann.selectedBulkSample_prior line 76

    Source documentation

    Only the selected coordinates need identical distributions.

    theorem selectedBulkSample_prior {B J A : Type*} [Fintype B]
        (slot : J ↪ B) (e : Equiv.Perm J) (ν : B → A → ℝ)
        (hν : ∀ j k, ν (slot j) = ν (slot k)) (y : B → A) :
        (∏ i, ν i (selectedBulkSample slot e y i)) = ∏ i, ν i (y i) := by
    …

    Mentions: OAI.Ostmann.selectedBulkSample

13. theorem OAI.Ostmann.selectedBulkSample_sum line 94
14. theorem OAI.Ostmann.selectedBulkSample_bulk_leaves line 105
15. theorem OAI.Ostmann.treeLeafMap_congr_on_slots line 115
16. theorem OAI.Ostmann.selectedBulkSample_small_leaves line 126