OAI/Probability/StrongRayleigh/LocalDyadicContinuity.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336AdditiveD139.LocalDyadicContinuity.Interval line 14
  2. def OAI.Problem336AdditiveD139.LocalDyadicContinuity.gridIndex line 18
  3. lemma OAI.Problem336AdditiveD139.LocalDyadicContinuity.gridIndex_le line 21
  4. lemma OAI.Problem336AdditiveD139.LocalDyadicContinuity.gridIndex_succ_div_two line 26
  5. lemma OAI.Problem336AdditiveD139.LocalDyadicContinuity.gridIndex_succ_cases line 34
  6. def OAI.Problem336AdditiveD139.LocalDyadicContinuity.approximation line 40
  7. lemma OAI.Problem336AdditiveD139.LocalDyadicContinuity.approximation_increment_le line 43
  8. lemma OAI.Problem336AdditiveD139.LocalDyadicContinuity.gridIndex_close line 59
  9. lemma OAI.Problem336AdditiveD139.LocalDyadicContinuity.approximation_close line 77
  10. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.exists_uniformContinuous_limit line 99
  11. lemma OAI.Problem336AdditiveD139.LocalDyadicContinuity.coherent_refinement line 151
  12. lemma OAI.Problem336AdditiveD139.LocalDyadicContinuity.gridIndex_at_node line 160
  13. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.limit_agrees_grid line 172
  14. def OAI.Problem336AdditiveD139.LocalDyadicContinuity.limit line 184
  15. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.uniformContinuous_limit line 187
  16. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.uniformContinuous_limit_of_eventually line 200
  17. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.measurable_limit_eval line 230
  18. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.measurable_limit line 236
  19. def OAI.Problem336AdditiveD139.LocalDyadicContinuity.globalLimit line 241
  20. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.continuous_globalLimit line 244
  21. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.globalLimit_agrees_grid line 267
  22. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.measurable_globalLimit_eval line 279
  23. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.measurable_globalLimit line 285
  24. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.ae_globalLimit_properties line 290
  25. theorem OAI.Problem336AdditiveD139.LocalDyadicContinuity.ae_globalLimit_properties_of_eventually line 303