OAI/Analysis/TracialSplitting/WeightedFamilies.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CurrentMain.WeightedBlockFamily line 17
  2. def OAI.CurrentMain.WeightedBlockFamily.range line 37
  3. def OAI.CurrentMain.WeightedBlockFamily.weightedSum line 39
  4. lemma OAI.CurrentMain.WeightedBlockFamily.range_projection line 42
  5. lemma OAI.CurrentMain.WeightedBlockFamily.weightedSum_nonneg line 45
  6. lemma OAI.CurrentMain.weightedAverage_sum line 52
  7. lemma OAI.CurrentMain.weightedAverage_mass_upper line 58
  8. theorem OAI.CurrentMain.weighted_family_of_average line 66
  9. def OAI.CurrentMain.ProjectionRow.overlapTest line 174
  10. lemma OAI.CurrentMain.ProjectionRow.trace_overlap_sample line 177
  11. theorem OAI.CurrentMain.ProjectionRow.sample_mass_overlap line 187
  12. lemma OAI.CurrentMain.traceTwoNorm_sub_le line 227
  13. lemma OAI.CurrentMain.traceTwoNorm_sum_le line 231
  14. lemma OAI.CurrentMain.traceTwoNorm_commutator_le line 235
  15. lemma OAI.CurrentMain.commutator_perturb_sq line 244
  16. lemma OAI.CurrentMain.projection_overlap_identity line 258
  17. lemma OAI.CurrentMain.weightedAverage_overlap line 281
  18. lemma OAI.CurrentMain.weightedAverage_overlap_le line 290
  19. lemma OAI.CurrentMain.unitary_coefficient_tests line 308