OAI/Computability/MinUncut/Estimates/SecondFailureIndicator.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Inner.secondFailure_indicator line 27
  2. lemma OAI.MinUncut.Inner.secondRejection_measurable line 34
  3. lemma OAI.MinUncut.Inner.secondRejection_range line 48
  4. lemma OAI.MinUncut.Inner.secondRejection_integrable line 68
  5. lemma OAI.MinUncut.Inner.rowProjectedGradient_memLp line 75
  6. lemma OAI.MinUncut.Inner.rowResidualEnergy_integrable line 86
  7. theorem OAI.MinUncut.Inner.gradient_row_tail_average line 94
  8. lemma OAI.MinUncut.RowNoise.project_eq_mask_sum line 130
  9. lemma OAI.MinUncut.RowNoise.project_sum line 147
  10. lemma OAI.MinUncut.RowNoise.project_sub line 154
  11. lemma OAI.MinUncut.RowNoise.project_energy_le line 159
  12. lemma OAI.MinUncut.RowNoise.project_memLp line 168
  13. def OAI.MinUncut.RowNoise.rectangle line 174
  14. lemma OAI.MinUncut.RowNoise.rectangle_eq_composition line 177
  15. lemma OAI.MinUncut.RowNoise.jointEnergy_project_le line 199
  16. lemma OAI.MinUncut.RowNoise.jointEnergy_add_le line 213
  17. theorem OAI.MinUncut.RowNoise.rectangle_residual_le line 229
  18. lemma OAI.MinUncut.RowNoise.rectangle_energy_identity line 248