OAI/Probability/FreeIsing/Estimates/ProjectiveExtension.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.CountableProjective.pullFinite line 11
2. lemma OAI.Problem367.CountableProjective.measurable_pullFinite line 14
3. lemma OAI.Problem367.CountableProjective.injective_pullFinite line 19
4. def OAI.Problem367.CountableProjective.pullFamily line 28
5. lemma OAI.Problem367.CountableProjective.projective_pullFamily line 32
6. theorem OAI.Problem367.CountableProjective.exists_projective_limit_of_equiv_nat line 42
7. theorem OAI.Problem367.CountableProjective.exists_countable_projective_limit line 81
8. lemma OAI.Problem367.CountableProjective.marginal_map_extension line 99
9. theorem OAI.Problem367.CountableProjective.exists_measure_for_countable_marginals line 115
10. lemma OAI.Problem367.CountableProjective.projectiveContent_tendsto_zero line 148
11. theorem OAI.Problem367.CountableProjective.exists_projective_limit line 169