OAI/Probability/FreeIsing/Estimates/DyadicContinuity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.DyadicContinuity.geometric_limit line 11
  2. theorem OAI.Problem367.DyadicContinuity.continuousOn_geometric_limit line 34
  3. theorem OAI.Problem367.DyadicContinuity.floor_double_cases line 58
  4. theorem OAI.Problem367.DyadicContinuity.floor_near_cases line 70
  5. theorem OAI.Problem367.DyadicContinuity.dyadicLeft_refinement line 85
  6. theorem OAI.Problem367.DyadicContinuity.dyadic_refinement_bound line 105
  7. theorem OAI.Problem367.DyadicContinuity.dyadic_oscillation_bound line 130
  8. theorem OAI.Problem367.DyadicContinuity.continuousOn_dyadicLimit line 153
  9. theorem OAI.Problem367.DyadicContinuity.tendsto_dyadic_sample line 189
  10. theorem OAI.Problem367.DyadicContinuity.dyadicLeft_grid line 210
  11. theorem OAI.Problem367.DyadicContinuity.dyadicLimit_grid line 224
  12. theorem OAI.Problem367.DyadicContinuity.continuousOn_Ici_dyadicLimit line 233
  13. theorem OAI.Problem367.DyadicContinuity.continuous_nnreal_dyadicLimit line 250
  14. theorem OAI.Problem367.DyadicContinuity.continuous_nnreal_dyadicLimit_of_nat_grid line 259