OAI/Analysis/OperatorAlgebra/ComplexSymmetricMean.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The complex linear version of the proved symmetric-interval mean. It is positive, normalized and translation invariant for a free ultrafilter.

  1. def OAI.WeakPureInfiniteness.meanRealPart line 15
  2. def OAI.WeakPureInfiniteness.meanImagPart line 18
  3. def OAI.WeakPureInfiniteness.complexSymmetricMean line 21
  4. lemma OAI.WeakPureInfiniteness.complexSymmetricMean_add line 24
  5. lemma OAI.WeakPureInfiniteness.complexSymmetricMean_smul line 37
  6. lemma OAI.WeakPureInfiniteness.complexSymmetricMean_norm_le line 53
  7. def OAI.WeakPureInfiniteness.complexSymmetricMeanCLM line 70
  8. lemma OAI.WeakPureInfiniteness.complexSymmetricMean_const line 77
  9. def OAI.WeakPureInfiniteness.complexTranslateBCF line 86
  10. lemma OAI.WeakPureInfiniteness.complexSymmetricMean_translate line 90
  11. lemma OAI.WeakPureInfiniteness.complexSymmetricMean_nonneg line 97