OAI/Analysis/FreeWords/WeakCompact.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniversalStrongKK.ScalarMean line 16
  2. def OAI.UniversalStrongKK.operatorCoefficient line 25
  3. theorem OAI.UniversalStrongKK.operatorCoefficient_apply line 36
  4. theorem OAI.UniversalStrongKK.norm_operatorCoefficient_le line 39
  5. def OAI.UniversalStrongKK.meanBilinear line 49
  6. def OAI.UniversalStrongKK.operatorMean line 83
  7. theorem OAI.UniversalStrongKK.inner_operatorMean line 86
  8. theorem OAI.UniversalStrongKK.norm_operatorMean_le line 90
  9. theorem OAI.UniversalStrongKK.exists_ultrafilter_mean line 118
  10. def OAI.UniversalStrongKK.ultrafilterMean line 147
  11. theorem OAI.UniversalStrongKK.tendsto_ultrafilterMean line 150
  12. theorem OAI.UniversalStrongKK.tendsto_operatorMean line 156
  13. theorem OAI.UniversalStrongKK.norm_le_of_wot_tendsto line 164
  14. theorem OAI.UniversalStrongKK.mem_of_wot_tendsto line 185
  15. theorem OAI.UniversalStrongKK.positive_of_wot_tendsto line 220