OAI/Analysis/BackwardIntertwiners/ConvolutionBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BackwardIntertwiners.EnvelopeBounds line 11
  2. lemma OAI.BackwardIntertwiners.middle_exponent line 17
  3. def OAI.BackwardIntertwiners.centeredCorrelation line 28
  4. lemma OAI.BackwardIntertwiners.EnvelopeBounds.reflected line 35
  5. lemma OAI.BackwardIntertwiners.EnvelopeBounds.central_norm line 42
  6. lemma OAI.BackwardIntertwiners.EnvelopeBounds.middle_pos line 50
  7. lemma OAI.BackwardIntertwiners.EnvelopeBounds.middle_neg line 66
  8. lemma OAI.BackwardIntertwiners.EnvelopeBounds.tail_pos line 76
  9. lemma OAI.BackwardIntertwiners.EnvelopeBounds.tail_neg line 90
  10. lemma OAI.BackwardIntertwiners.tsum_bound_middle_tail line 102
  11. lemma OAI.BackwardIntertwiners.central_norm_le_of_correlation_zero line 124
  12. def OAI.BackwardIntertwiners.geometricMiddle line 136
  13. lemma OAI.BackwardIntertwiners.geometricMiddle_hasSum line 138
  14. lemma OAI.BackwardIntertwiners.geometricMiddle_budget line 150
  15. lemma OAI.BackwardIntertwiners.EnvelopeBounds.correlation_budget line 175
  16. theorem OAI.BackwardIntertwiners.no_correlation_of_envelopes line 238