OAI/Probability/FreeIsing/Estimates/ProgressiveVersionPushforward.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.ProgressiveVersionPushforward.gridTime line 15
2. def OAI.Problem367.ProgressiveVersionPushforward.leftTime line 17
3. lemma OAI.Problem367.ProgressiveVersionPushforward.leftTime_le line 20
4. lemma OAI.Problem367.ProgressiveVersionPushforward.tendsto_leftTime line 23
5. lemma OAI.Problem367.ProgressiveVersionPushforward.leftTime_mem_range line 28
6. lemma OAI.Problem367.ProgressiveVersionPushforward.denseRange_gridTime line 31
7. lemma OAI.Problem367.ProgressiveVersionPushforward.measurable_leftTime line 36
8. def OAI.Problem367.ProgressiveVersionPushforward.version line 40
9. lemma OAI.Problem367.ProgressiveVersionPushforward.measurable_version line 43
10. lemma OAI.Problem367.ProgressiveVersionPushforward.progressive_version line 48
11. lemma OAI.Problem367.ProgressiveVersionPushforward.version_eq_of_grid line 57
12. lemma OAI.Problem367.ProgressiveVersionPushforward.ae_all_version_eq line 68
13. lemma OAI.Problem367.ProgressiveVersionPushforward.measurableEmbedding_gridEval line 75
14. theorem OAI.Problem367.ProgressiveVersionPushforward.continuous_progressive_version_of_pullback line 83