OAI/Probability/SpanningForest/SchauderTents.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.SchauderTents.unitTent line 11
  2. theorem OAI.Problem336.SchauderTents.continuous_unitTent line 13
  3. theorem OAI.Problem336.SchauderTents.unitTent_nonneg line 17
  4. theorem OAI.Problem336.SchauderTents.unitTent_le_half line 19
  5. theorem OAI.Problem336.SchauderTents.unitTent_pos_iff line 26
  6. theorem OAI.Problem336.SchauderTents.unitTent_ne_zero_iff line 30
  7. theorem OAI.Problem336.SchauderTents.unitTent_eq_zero_of_le_zero line 37
  8. theorem OAI.Problem336.SchauderTents.unitTent_eq_zero_of_one_le line 41
  9. theorem OAI.Problem336.SchauderTents.unitTent_half line 45
  10. theorem OAI.Problem336.SchauderTents.unitTent_of_left line 48
  11. theorem OAI.Problem336.SchauderTents.unitTent_of_right line 53
  12. theorem OAI.Problem336.SchauderTents.unitTent_midpoint_of_no_corner line 58
  13. theorem OAI.Problem336.SchauderTents.unitTent_even_grid_midpoint line 76
  14. def OAI.Problem336.SchauderTents.amplitude line 124
  15. theorem OAI.Problem336.SchauderTents.amplitude_pos line 126
  16. def OAI.Problem336.SchauderTents.tent line 130
  17. theorem OAI.Problem336.SchauderTents.continuous_tent line 133
  18. theorem OAI.Problem336.SchauderTents.tent_nonneg line 136
  19. theorem OAI.Problem336.SchauderTents.tent_le_half_amplitude line 139
  20. theorem OAI.Problem336.SchauderTents.tent_ne_zero_iff line 146
  21. theorem OAI.Problem336.SchauderTents.tent_disjoint line 152
  22. def OAI.Problem336.SchauderTents.level line 163
  23. theorem OAI.Problem336.SchauderTents.continuous_level line 166
  24. theorem OAI.Problem336.SchauderTents.abs_level_le line 170
  25. theorem OAI.Problem336.SchauderTents.unitTent_nat_sub line 200
  26. theorem OAI.Problem336.SchauderTents.tent_grid_zero line 209
  27. theorem OAI.Problem336.SchauderTents.tent_prior_grid_zero line 215
  28. theorem OAI.Problem336.SchauderTents.level_prior_grid_zero line 225
  29. def OAI.Problem336.SchauderTents.midpoint line 229
  30. theorem OAI.Problem336.SchauderTents.tent_at_midpoint line 231
  31. theorem OAI.Problem336.SchauderTents.tent_at_other_midpoint line 241
  32. theorem OAI.Problem336.SchauderTents.level_at_midpoint line 247
  33. theorem OAI.Problem336.SchauderTents.tent_old_midpoint line 259
  34. theorem OAI.Problem336.SchauderTents.tent_old_midpoint_of_lt line 272
  35. theorem OAI.Problem336.SchauderTents.level_old_midpoint line 280