OAI/Computability/MinUncut/Estimates/EraseAway.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Subbox.expect_sigma_const line 23
  2. def OAI.MinUncut.Subbox.eraseAway line 32
  3. lemma OAI.MinUncut.Subbox.mem_eraseAway line 37
  4. lemma OAI.MinUncut.Subbox.eraseAway_card line 49
  5. def OAI.MinUncut.Subbox.unpoint line 52
  6. lemma OAI.MinUncut.Subbox.pointed_unpoint line 55
  7. lemma OAI.MinUncut.Subbox.unpoint_pointed line 63
  8. abbrev OAI.MinUncut.Subbox.UnpointedBox line 70
  9. abbrev OAI.MinUncut.Subbox.BoxPoint line 71
  10. def OAI.MinUncut.Subbox.boxOfPointed line 73
  11. lemma OAI.MinUncut.Subbox.boxPoint_heq line 77
  12. def OAI.MinUncut.Subbox.boxJointEquiv line 84
  13. lemma OAI.MinUncut.Subbox.card_boxPoint line 103
  14. lemma OAI.MinUncut.Subbox.card_pointedBox line 108
  15. theorem OAI.MinUncut.Subbox.bayes_box line 112
  16. def OAI.MinUncut.Subbox.coordinateEnum line 124
  17. def OAI.MinUncut.Subbox.pointEnum line 128
  18. def OAI.MinUncut.Subbox.pointEmbed line 131
  19. lemma OAI.MinUncut.Subbox.pointEmbed_injective line 135
  20. lemma OAI.MinUncut.Subbox.pointEmbed_mem line 144
  21. lemma OAI.MinUncut.Subbox.pointwise_bayes line 147
  22. def OAI.MinUncut.Inner.codeRestriction line 165
  23. theorem OAI.MinUncut.Inner.faceCorrelation_restriction line 173
  24. def OAI.MinUncut.Slice.energy line 194
  25. lemma OAI.MinUncut.Slice.energy_nonneg line 197
  26. lemma OAI.MinUncut.Slice.energy_measurable line 201
  27. lemma OAI.MinUncut.Slice.energy_integrable line 208
  28. lemma OAI.MinUncut.Slice.sliceNorm_memLp line 215
  29. lemma OAI.MinUncut.Slice.oddMax_measurable line 222
  30. lemma OAI.MinUncut.Slice.oddMax_memLp line 240
  31. lemma OAI.MinUncut.Slice.processed_measurable line 260
  32. lemma OAI.MinUncut.Slice.processed_memLp line 269
  33. theorem OAI.MinUncut.Slice.processed_integral_loss line 276