OAI/Analysis/CharacterCriterion/FullComparison.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.GenericRW.FullComparison.mem_span_list line 29
2. lemma OAI.KirchbergRordam.GenericRW.FullComparison.finite_presentation line 65
3. lemma OAI.KirchbergRordam.GenericRW.FullComparison.exists_full_perturbation line 84
4. theorem OAI.KirchbergRordam.GenericRW.FullComparison.full_comparison line 140
5. lemma OAI.KirchbergRordam.GenericRW.ConeCut.unit_norm line 198
6. lemma OAI.KirchbergRordam.GenericRW.ConeCut.coeff_difference line 201
7. lemma OAI.KirchbergRordam.GenericRW.ConeCut.norm_sub_q line 212
8. lemma OAI.KirchbergRordam.GenericRW.ConeCut.exists_full_cut line 222
9. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.word_sum_coordinate line 237
10. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.word_nonneg line 258
11. def OAI.KirchbergRordam.GenericRW.MaxTensor.defectWord line 267
12. def OAI.KirchbergRordam.GenericRW.MaxTensor.cornerWord line 268
13. def OAI.KirchbergRordam.GenericRW.MaxTensor.columnWord line 270
14. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.cornerWord_nonneg line 273
15. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.cornerWord_orthogonal line 276
16. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.columnWord_comparison line 281
17. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.lift_pure line 304
18. def OAI.KirchbergRordam.GenericRW.MaxTensor.powerHom line 315
19. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.powerHom_pure line 319
20. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.powerHom_word line 323
21. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.map line 335
22. lemma OAI.KirchbergRordam.GenericRW.support_cut_cfc line 350
23. lemma OAI.KirchbergRordam.GenericRW.support_cut_comparison line 366