OAI/Analysis/SeparableQuotients/Positive/UnconditionalBasis.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SeparableQuotient.Positive.Sampling.ClosedSpan line 15
  2. abbrev OAI.SeparableQuotient.Positive.Sampling.spanVector line 16
  3. abbrev OAI.SeparableQuotient.Positive.Sampling.spanCombination line 17
  4. def OAI.SeparableQuotient.Positive.Sampling.SuppressionBoundTwo line 21
  5. lemma OAI.SeparableQuotient.Positive.Sampling.suppressionBoundTwo_of_finite line 25
  6. lemma OAI.SeparableQuotient.Positive.Sampling.coefficient_bound line 49
  7. def OAI.SeparableQuotient.Positive.Sampling.suppressedCoord line 61
  8. lemma OAI.SeparableQuotient.Positive.Sampling.suppressedCoord_combination line 64
  9. lemma OAI.SeparableQuotient.Positive.Sampling.suppressedCoord_bound line 70
  10. lemma OAI.SeparableQuotient.Positive.Sampling.suppressedCoord_ortho line 76
  11. def OAI.SeparableQuotient.Positive.Sampling.suppressedProjection line 85
  12. lemma OAI.SeparableQuotient.Positive.Sampling.suppressedProjection_apply line 89
  13. lemma OAI.SeparableQuotient.Positive.Sampling.suppressedProjection_bound line 93
  14. lemma OAI.SeparableQuotient.Positive.Sampling.suppressedProjection_combination line 108
  15. lemma OAI.SeparableQuotient.Positive.Sampling.suppressed_expansion line 116
  16. def OAI.SeparableQuotient.Positive.Sampling.unconditionalBasisOfSuppression line 137
  17. def OAI.SeparableQuotient.Positive.Sampling.IsUnconditionalBasicSequence line 163
  18. theorem OAI.SeparableQuotient.Positive.Sampling.coded_family_unconditional line 170