OAI/NumberTheory/Ostmann/Construction/InitialEtaStatePrior.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Construction.InitialEta.RawSample line 12
2. def OAI.Ostmann.Construction.InitialEta.rawEquiv line 18
3. abbrev OAI.Ostmann.Construction.InitialEta.SourceSample line 57
4. def OAI.Ostmann.Construction.InitialEta.sourceEquiv line 63
5. theorem OAI.Ostmann.Construction.InitialEta.sourceEquiv_spectator line 71
6. theorem OAI.Ostmann.Construction.InitialEta.sourceEquiv_small line 79
7. theorem OAI.Ostmann.Construction.InitialEta.sourceEquiv_mass line 88
8. theorem OAI.Ostmann.Construction.InitialEta.sourceEquiv_cmean line 113