OAI/Analysis/StrictMeans/PositiveFunctionals.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.continuousMap_order_bound line 43
  2. lemma OAI.StrictInverseFirstPower.positiveOperator_unit_nonneg line 52
  3. lemma OAI.StrictInverseFirstPower.positiveOperator_apply_abs_le line 56
  4. lemma OAI.StrictInverseFirstPower.positiveOperator_norm line 65
  5. lemma OAI.StrictInverseFirstPower.positiveOperator_pow_monotone line 80
  6. lemma OAI.StrictInverseFirstPower.positiveOperator_pow_norm line 89
  7. lemma OAI.StrictInverseFirstPower.positiveOperator_iterate_bound line 93
  8. def OAI.StrictInverseFirstPower.compactTestFunctional line 131
  9. lemma OAI.StrictInverseFirstPower.exists_probabilityMeasure_of_positiveFunctional line 140