OAI/Probability/FreeIsing/Estimates/ContinuousModification.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.ContinuousModification.sampledLimit line 15
  2. theorem OAI.Problem367.ContinuousModification.sampledLimit_congr line 18
  3. theorem OAI.Problem367.ContinuousModification.measurable_sampledLimit line 25
  4. theorem OAI.Problem367.ContinuousModification.measurable_sampledLimit_at line 31
  5. theorem OAI.Problem367.ContinuousModification.ae_all_eq_of_continuous_modification line 36
  6. theorem OAI.Problem367.ContinuousModification.ae_continuous_sampledLimit line 55
  7. theorem OAI.Problem367.ContinuousModification.sampledLimit_equivariant line 67
  8. theorem OAI.Problem367.ContinuousModification.ae_all_eq_family line 74
  9. theorem OAI.Problem367.ContinuousModification.isStronglyProgressive_sampledLimit line 86
  10. def OAI.Problem367.ContinuousModification.dyadicLeft line 95
  11. theorem OAI.Problem367.ContinuousModification.dyadicLeft_le line 97
  12. theorem OAI.Problem367.ContinuousModification.sub_inv_pow_le_dyadicLeft line 102
  13. theorem OAI.Problem367.ContinuousModification.dyadicLeft_nonneg line 111
  14. theorem OAI.Problem367.ContinuousModification.tendsto_dyadicLeft line 116
  15. theorem OAI.Problem367.ContinuousModification.dyadicLeft_mem_rationals line 124
  16. theorem OAI.Problem367.ContinuousModification.measurable_dyadic_sample line 129
  17. theorem OAI.Problem367.ContinuousModification.isProgressive_dyadic_sample line 136
  18. theorem OAI.Problem367.ContinuousModification.isStronglyProgressive_dyadicLimit line 158
  19. theorem OAI.Problem367.ContinuousModification.measurable_dyadicLimit line 164
  20. theorem OAI.Problem367.ContinuousModification.ae_all_dyadicLimit_eq line 169