OAI/Computability/MinUncut/Estimates/Rest.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.RowNoise.Rest line 21
  2. def OAI.MinUncut.RowNoise.joinRow line 23
  3. lemma OAI.MinUncut.RowNoise.joinRow_at line 27
  4. lemma OAI.MinUncut.RowNoise.joinRow_other line 31
  5. lemma OAI.MinUncut.RowNoise.expect_splitRow line 36
  6. def OAI.MinUncut.RowNoise.restMask line 43
  7. lemma OAI.MinUncut.RowNoise.maskKernel_split line 47
  8. def OAI.MinUncut.RowNoise.rowCoefficient line 58
  9. lemma OAI.MinUncut.RowNoise.rowCoefficient_maskProject line 62
  10. lemma OAI.MinUncut.RowNoise.rowCoefficient_maskProject_envelope line 91
  11. lemma OAI.MinUncut.RowNoise.rowEnvelope_mean line 107