OAI/Computability/MinUncut/Estimates/FourthTest.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Inner.comparisonFailure line 16
  2. def OAI.MinUncut.Inner.comparisonRejection line 22
  3. lemma OAI.MinUncut.Inner.comparisonFailure_eq line 28
  4. theorem OAI.MinUncut.Inner.gradient_comparison line 37
  5. def OAI.MinUncut.Inner.pullbackFaces line 75
  6. lemma OAI.MinUncut.Inner.labelCode_pullbackFaces line 79
  7. lemma OAI.MinUncut.Inner.pullQuery_pullbackFaces line 83
  8. lemma OAI.MinUncut.Inner.pullbackFaces_joinRow line 92
  9. def OAI.MinUncut.Inner.comparisonRow line 103
  10. lemma OAI.MinUncut.Inner.comparisonRow_pullback line 108
  11. lemma OAI.MinUncut.Inner.comparisonRow_average line 117
  12. lemma OAI.MinUncut.Inner.comparisonFailure_indicator line 129
  13. lemma OAI.MinUncut.Inner.comparisonRejection_measurable line 137
  14. lemma OAI.MinUncut.Inner.comparisonRejection_range line 158
  15. lemma OAI.MinUncut.Inner.comparisonRejection_integrable line 180
  16. def OAI.MinUncut.Inner.fourthError line 188
  17. lemma OAI.MinUncut.Inner.averaged_comparison line 193
  18. lemma OAI.MinUncut.Inner.comparisonRow_spatial_average line 215
  19. def OAI.MinUncut.Composition.listMatch line 241
  20. def OAI.MinUncut.Composition.rowDistance line 244
  21. def OAI.MinUncut.Composition.restrictedFourth line 247
  22. lemma OAI.MinUncut.Composition.rowDistance_nonneg line 251
  23. lemma OAI.MinUncut.Composition.restrictedFourth_nonneg line 254
  24. lemma OAI.MinUncut.Composition.coefficient_fourth_le line 257
  25. theorem OAI.MinUncut.Composition.atom_le_matching_charge line 266