OAI/Analysis/WeakInfiniteness/WordCompression.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.wordEval line 25
  2. lemma OAI.WeakPureInfiniteness.norm_wordEval_le_one line 29
  3. lemma OAI.WeakPureInfiniteness.norm_wordEval_intertwining_le line 40
  4. def OAI.WeakPureInfiniteness.wordSpace line 78
  5. instance OAI.WeakPureInfiniteness.wordSpace_finiteDimensional line 82
  6. lemma OAI.WeakPureInfiniteness.wordSpace_mono line 93
  7. lemma OAI.WeakPureInfiniteness.wordEval_mem_wordSpace line 99
  8. lemma OAI.WeakPureInfiniteness.wordEval_mem_wordSpace_of_length_le line 110
  9. lemma OAI.WeakPureInfiniteness.testVector_mem_wordSpace line 116
  10. lemma OAI.WeakPureInfiniteness.adjoint_compress line 121
  11. lemma OAI.WeakPureInfiniteness.compressed_wordEval line 128
  12. lemma OAI.WeakPureInfiniteness.wordSpace_compression_exact line 140
  13. def OAI.WeakPureInfiniteness.amplifiedPolynomial line 159
  14. lemma OAI.WeakPureInfiniteness.amplifiedPolynomial_intertwining line 164
  15. lemma OAI.WeakPureInfiniteness.norm_amplifiedPolynomial_intertwining_le line 178
  16. lemma OAI.WeakPureInfiniteness.norm_amplifiedPolynomial_le line 203
  17. lemma OAI.WeakPureInfiniteness.amplifiedPolynomial_tmul line 245
  18. lemma OAI.WeakPureInfiniteness.amplifiedPolynomial_compression_exact line 251
  19. lemma OAI.WeakPureInfiniteness.norm_amplifiedPolynomial_le_of_finite_compressions line 269