OAI/Analysis/CStarAlgebra/PureInfiniteness/Products.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MainGap.cut_le_self line 14
  2. lemma OAI.MainGap.norm_cut_le line 22
  3. lemma OAI.MainGap.cutInverse_nonneg line 25
  4. lemma OAI.MainGap.fixed_of_outer_fixed line 31
  5. lemma OAI.MainGap.cutInverse_fixed_carrier line 42
  6. theorem OAI.MainGap.bounded_two_slots line 52
  7. def OAI.MainGap.lpEval line 105
  8. lemma OAI.MainGap.lpEval_apply line 113
  9. def OAI.MainGap.lpBuild line 115
  10. lemma OAI.MainGap.lpBuild_apply line 118
  11. lemma OAI.MainGap.lp_nonneg_iff line 121
  12. theorem OAI.MainGap.propertyP_lp line 136
  13. lemma OAI.MainGap.lp_single_mem_Her line 176
  14. lemma OAI.MainGap.HerCompression.lp_eval line 195
  15. lemma OAI.MainGap.NormSignal.lp_eval line 224
  16. theorem OAI.MainGap.uniform_shrinking line 238