OAI/Combinatorics/SumProduct/Alignment/PhysicalDecay01.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SourcePhysicalDecay.AllBoxes line 23
2. theorem OAI.SourcePhysicalDecay.allBoxes_subsequence line 34
3. lemma OAI.SourcePhysicalDecay.physical_box_eq_rectangle line 82
4. lemma OAI.SourcePhysicalDecay.mean_eq_expect line 90
5. lemma OAI.SourcePhysicalDecay.mean_ofReal line 93
6. theorem OAI.SourcePhysicalDecay.haar_invariant_of_allBoxes line 118
7. def OAI.SourcePhysicalDecay.AllCompatibleHaar line 169
8. theorem OAI.SourcePhysicalDecay.compatible_haar_of_allBoxes line 198
9. theorem OAI.SourceIntegerArrays.source_global_literal_haar line 250