OAI/Computability/MinUncut/Estimates/ArraySum.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Inner.arraySum line 21
  2. lemma OAI.MinUncut.Inner.arraySum_apply line 23
  3. lemma OAI.MinUncut.Inner.labelCode_add line 28
  4. lemma OAI.MinUncut.Inner.labelCode_eq_of_arraySum line 33
  5. lemma OAI.MinUncut.Inner.gradient_eq_of_arraySum line 40
  6. def OAI.MinUncut.Inner.addConstantArray line 49
  7. def OAI.MinUncut.Inner.rowCode line 52
  8. lemma OAI.MinUncut.Inner.labelCode_addConstantArray line 54
  9. def OAI.MinUncut.Inner.diagonal line 60
  10. lemma OAI.MinUncut.Inner.diagonal_involutive line 63
  11. lemma OAI.MinUncut.Inner.diagonal_add line 69
  12. lemma OAI.MinUncut.Inner.diagonal_smul line 73
  13. lemma OAI.MinUncut.Inner.diagonal_preserves line 77
  14. lemma OAI.MinUncut.Inner.integral_diagonal line 89
  15. lemma OAI.MinUncut.Inner.integral_code_translate line 97
  16. lemma OAI.MinUncut.Inner.query_translate line 113
  17. lemma OAI.MinUncut.Inner.pullQuery_addConstantArray line 126
  18. lemma OAI.MinUncut.Inner.smooth_addConstantArray line 134
  19. theorem OAI.MinUncut.Inner.gradient_addConstantArray line 149
  20. def OAI.MinUncut.Inner.doubleMatch line 177
  21. def OAI.MinUncut.Inner.rowFill line 180
  22. lemma OAI.MinUncut.Inner.doubleMatch_rowFill line 183
  23. def OAI.MinUncut.Inner.cylinderArray line 195
  24. lemma OAI.MinUncut.Inner.cylinderArray_local line 198
  25. lemma OAI.MinUncut.Inner.cylinderArray_sum_zero line 205
  26. lemma OAI.MinUncut.Inner.arraySum_add line 218
  27. theorem OAI.MinUncut.Inner.gradient_cylinder line 221
  28. theorem OAI.MinUncut.Inner.gradient_fourier_cylinder line 230