OAI/Probability/SpanningForest/DyadicInterpolation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.DyadicInterpolation.grid line 13
  2. theorem OAI.Problem336.DyadicInterpolation.grid_zero line 15
  3. theorem OAI.Problem336.DyadicInterpolation.grid_zero_level line 16
  4. theorem OAI.Problem336.DyadicInterpolation.grid_succ_even line 18
  5. theorem OAI.Problem336.DyadicInterpolation.grid_succ_odd line 24
  6. theorem OAI.Problem336.DyadicInterpolation.midpoint_eq_average line 30
  7. def OAI.Problem336.DyadicInterpolation.residual line 36
  8. def OAI.Problem336.DyadicInterpolation.coefficient line 39
  9. def OAI.Problem336.DyadicInterpolation.approx line 42
  10. theorem OAI.Problem336.DyadicInterpolation.continuous_approx line 45
  11. theorem OAI.Problem336.DyadicInterpolation.approx_succ line 51
  12. theorem OAI.Problem336.DyadicInterpolation.approx_old_midpoint line 56
  13. theorem OAI.Problem336.DyadicInterpolation.level_coefficient_midpoint line 76
  14. theorem OAI.Problem336.DyadicInterpolation.approx_grid line 82
  15. theorem OAI.Problem336.DyadicInterpolation.abs_residual_le line 105
  16. theorem OAI.Problem336.DyadicInterpolation.abs_residual_le_of_increments line 114
  17. theorem OAI.Problem336.DyadicInterpolation.abs_approx_succ_sub_le_of_residual line 126
  18. theorem OAI.Problem336.DyadicInterpolation.abs_approx_succ_sub_le line 142
  19. theorem OAI.Problem336.DyadicInterpolation.measurable_residual line 154
  20. theorem OAI.Problem336.DyadicInterpolation.measurable_coefficient line 158
  21. theorem OAI.Problem336.DyadicInterpolation.measurable_approx line 162