OAI/Probability/SKBarriers/Scalar/EmbeddedSites.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.siteValueTerminal line 16
2. def OAI.SK.Analytic.embeddedSiteExponent line 19
3. def OAI.SK.Analytic.embeddedVector line 22
4. theorem OAI.SK.Analytic.embeddedVector_at line 26
5. theorem OAI.SK.Analytic.embeddedVector_off line 32
6. theorem OAI.SK.Analytic.embeddedSite_terminal line 37
7. theorem OAI.SK.Analytic.embeddedSite_pressure line 59
8. theorem OAI.SK.Analytic.embeddedSite_invariant line 72
9. theorem OAI.SK.Analytic.embeddedSites_tensorizes line 80