OAI/Analysis/SeparableQuotients/StoppedCharges.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeparableQuotient.ActualSpace.TypeI.stoppedCharge line 11
  2. lemma OAI.SeparableQuotient.ActualSpace.TypeI.stoppedCharge_nonneg line 16
  3. lemma OAI.SeparableQuotient.ActualSpace.TypeI.total_incidence line 20
  4. lemma OAI.SeparableQuotient.ActualSpace.TypeI.stoppedCharge_norm line 33
  5. lemma OAI.SeparableQuotient.ActualSpace.TypeI.stopped_eval_bound line 59
  6. lemma OAI.SeparableQuotient.ActualSpace.Family.sum_theta_tail_le line 72
  7. lemma OAI.SeparableQuotient.ActualSpace.Parameters.B_sum line 93
  8. lemma OAI.SeparableQuotient.ActualSpace.Family.sum_low_lengths line 98
  9. def OAI.SeparableQuotient.ActualSpace.TypeII.earlyGroups line 126
  10. abbrev OAI.SeparableQuotient.ActualSpace.TypeII.ChildVectors line 129
  11. def OAI.SeparableQuotient.ActualSpace.TypeII.recombineEarly line 132
  12. lemma OAI.SeparableQuotient.ActualSpace.TypeII.early_lengths_bound line 137
  13. lemma OAI.SeparableQuotient.ActualSpace.TypeII.early_theta_bound line 143
  14. lemma OAI.SeparableQuotient.ActualSpace.TypeII.recombineEarly_nonneg line 148
  15. lemma OAI.SeparableQuotient.ActualSpace.TypeII.recombineEarly_support line 154
  16. lemma OAI.SeparableQuotient.ActualSpace.TypeII.recombineEarly_norm line 163
  17. lemma OAI.SeparableQuotient.ActualSpace.TypeII.recombineEarly_l1 line 186
  18. def OAI.SeparableQuotient.ActualSpace.TypeII.lateGroups line 222
  19. def OAI.SeparableQuotient.ActualSpace.TypeII.lateVector line 225
  20. def OAI.SeparableQuotient.ActualSpace.TypeII.earlyBoundary line 229
  21. lemma OAI.SeparableQuotient.ActualSpace.TypeII.lateVector_nonneg line 233
  22. lemma OAI.SeparableQuotient.ActualSpace.TypeII.earlyBoundary_nonneg line 238
  23. lemma OAI.SeparableQuotient.ActualSpace.TypeII.lateVector_norm line 243
  24. lemma OAI.SeparableQuotient.ActualSpace.TypeII.earlyBoundary_l1 line 266
  25. def OAI.SeparableQuotient.ActualSpace.ThinnedWindows.localSmall line 285
  26. def OAI.SeparableQuotient.ActualSpace.ThinnedWindows.localLarge line 289
  27. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.localSmall_nonneg line 295
  28. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.localLarge_nonneg line 301
  29. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.localSmall_support line 310
  30. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.localLarge_support line 316
  31. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.localSmall_norm line 323
  32. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.localLarge_l1 line 331