OAI/Analysis/WeakInfiniteness/UniformModels.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.FiniteContractionModels line 26
  2. lemma OAI.WeakPureInfiniteness.universalFaithfulRepresentation_one line 32
  3. def OAI.WeakPureInfiniteness.universalUnitalRepresentation line 36
  4. lemma OAI.WeakPureInfiniteness.unitalRep_universalWord line 44
  5. lemma OAI.WeakPureInfiniteness.operatorLetters_norm line 50
  6. lemma OAI.WeakPureInfiniteness.tensor_norm_le_faithful_finset line 56
  7. def OAI.WeakPureInfiniteness.wordTensor line 75
  8. lemma OAI.WeakPureInfiniteness.wordTensor_val line 78
  9. lemma OAI.WeakPureInfiniteness.minimalMapLeft_wordTensor line 85
  10. def OAI.WeakPureInfiniteness.wordTensorCost line 94
  11. lemma OAI.WeakPureInfiniteness.wordTensorCost_nonneg line 97
  12. lemma OAI.WeakPureInfiniteness.norm_model_amplifiedPolynomial_le line 102
  13. lemma OAI.WeakPureInfiniteness.norm_faithfulAmplifiedPolynomial_le_of_models line 129
  14. lemma OAI.WeakPureInfiniteness.norm_wordTensor_le_of_models line 169