OAI/Computability/MinUncut/Estimates/Assembly.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Inner.zeroProcessed line 17
  2. lemma OAI.MinUncut.Inner.zeroProcessed_measurable line 22
  3. lemma OAI.MinUncut.Inner.zeroProcessed_memLp line 27
  4. lemma OAI.MinUncut.Inner.zero_processing_loss_integral line 34
  5. lemma OAI.MinUncut.Inner.zero_processing_loss_average line 53
  6. lemma OAI.MinUncut.Inner.class_correlation_processing line 86
  7. lemma OAI.MinUncut.Inner.pair_class_correlation line 112
  8. lemma OAI.MinUncut.Inner.zero_class_correlation line 145
  9. lemma OAI.MinUncut.Inner.weighted_pair_class_correlation line 188
  10. lemma OAI.MinUncut.Inner.weighted_zero_class_correlation line 217
  11. lemma OAI.MinUncut.Inner.weighted_lowGradient_classes line 231
  12. def OAI.MinUncut.Inner.classTarget line 244
  13. lemma OAI.MinUncut.Inner.classTarget_pos line 246
  14. lemma OAI.MinUncut.Inner.classes_times_target line 250
  15. lemma OAI.MinUncut.Inner.rectangle_bounds line 256
  16. lemma OAI.MinUncut.Inner.rectangle_pair_room line 261
  17. theorem OAI.MinUncut.Inner.inner_atom_of_errors line 267
  18. lemma OAI.MinUncut.Inner.exists_dimension line 332
  19. lemma OAI.MinUncut.Inner.exists_positive_nat_div_lt line 346
  20. lemma OAI.MinUncut.Inner.exists_reciprocal_processing line 355
  21. lemma OAI.MinUncut.Inner.exists_box_scale line 383
  22. lemma OAI.MinUncut.Inner.exists_ambient_scale line 400
  23. lemma OAI.MinUncut.Inner.exists_small_rational_atoms line 420
  24. lemma OAI.MinUncut.Inner.nested_atom_lt line 432