OAI/Combinatorics/BalancedRyser/Profiles/ProfileIdentifiability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.ProfileIdentifiability.laplaceSeries line 13
2. theorem OAI.Balanced.ProfileIdentifiability.tendsto_rescaled_laplaceSeries line 16
3. theorem OAI.Balanced.ProfileIdentifiability.exists_least_nonzero_exponent line 54
4. theorem OAI.Balanced.ProfileIdentifiability.laplaceSeries_eq_zero_imp line 67
5. theorem OAI.Balanced.ProfileIdentifiability.exists_laplaceSeries_ne_zero line 83
6. theorem OAI.Balanced.ProfileIdentifiability.summable_laplaceTerms line 93
7. theorem OAI.Balanced.ProfileIdentifiability.laplaceSeries_injective line 102