OAI/Analysis/CharacterCriterion/FunctionalCalculus.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KirchbergRordam.GenericRW.Domination.invReg line 28
2. def OAI.KirchbergRordam.GenericRW.Domination.remReg line 29
3. lemma OAI.KirchbergRordam.GenericRW.Domination.invReg_cont line 32
4. lemma OAI.KirchbergRordam.GenericRW.Domination.remReg_cont line 39
5. lemma OAI.KirchbergRordam.GenericRW.Domination.remReg_nonneg line 43
6. lemma OAI.KirchbergRordam.GenericRW.Domination.remReg_bound line 54
7. lemma OAI.KirchbergRordam.GenericRW.Domination.norm_sandwich_sqrt_sq line 70
8. lemma OAI.KirchbergRordam.GenericRW.Domination.norm_sandwich_le line 83
9. lemma OAI.KirchbergRordam.GenericRW.Domination.regularizer_estimate line 94
10. lemma OAI.KirchbergRordam.GenericRW.Domination.sqrt_mem_right_range line 127
11. lemma OAI.KirchbergRordam.GenericRW.Domination.sqrt_mem_self line 148
12. lemma OAI.KirchbergRordam.GenericRW.Domination.sqrt_right_range_eq line 151
13. lemma OAI.KirchbergRordam.GenericRW.Domination.exists_factor line 159
14. def OAI.KirchbergRordam.GenericRW.CuntzBelow line 183
15. lemma OAI.KirchbergRordam.GenericRW.CuntzBelow.approx line 188
16. lemma OAI.KirchbergRordam.GenericRW.CuntzBelow.of_approx line 198
17. lemma OAI.KirchbergRordam.GenericRW.CuntzBelow.of_eq line 210
18. lemma OAI.KirchbergRordam.GenericRW.CuntzBelow.refl line 217
19. lemma OAI.KirchbergRordam.GenericRW.CuntzBelow.trans line 219
20. lemma OAI.KirchbergRordam.GenericRW.CuntzBelow.map line 240
21. def OAI.KirchbergRordam.GenericRW.ExactCut.cut line 257
22. lemma OAI.KirchbergRordam.GenericRW.ExactCut.cut_nonneg line 260
23. lemma OAI.KirchbergRordam.GenericRW.ExactCut.cut_lower line 268
24. lemma OAI.KirchbergRordam.GenericRW.ExactCut.close_lower line 292
25. lemma OAI.KirchbergRordam.GenericRW.ExactCut.cut_dominated line 306
26. theorem OAI.KirchbergRordam.GenericRW.ExactCut.exists_exact_cut line 341
27. def OAI.KirchbergRordam.GenericRW.RWCut.j line 361
28. def OAI.KirchbergRordam.GenericRW.RWCut.f line 362
29. lemma OAI.KirchbergRordam.GenericRW.RWCut.j_cont line 364
30. lemma OAI.KirchbergRordam.GenericRW.RWCut.f_cont line 368
31. lemma OAI.KirchbergRordam.GenericRW.RWCut.f_nonneg line 370
32. lemma OAI.KirchbergRordam.GenericRW.RWCut.f_le_one line 375
33. lemma OAI.KirchbergRordam.GenericRW.RWCut.f_high line 383
34. lemma OAI.KirchbergRordam.GenericRW.RWCut.f_low line 390
35. lemma OAI.KirchbergRordam.GenericRW.RWCut.defect line 394
36. lemma OAI.KirchbergRordam.GenericRW.RWCut.cut_cfc line 401
37. lemma OAI.KirchbergRordam.GenericRW.RWCut.function_mul line 416
38. lemma OAI.KirchbergRordam.GenericRW.RWCut.rescaled_nonneg line 422
39. lemma OAI.KirchbergRordam.GenericRW.RWCut.rescaled_norm line 425
40. lemma OAI.KirchbergRordam.GenericRW.RWCut.rescaled_defect line 432
41. lemma OAI.KirchbergRordam.GenericRW.RWCut.fixes_cut line 447
42. lemma OAI.KirchbergRordam.GenericRW.RWCut.fixes_hereditary line 459
43. lemma OAI.KirchbergRordam.GenericRW.RWCut.fixes_of_mul_star line 472
44. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.cutoffRescale line 491
45. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.cutoffRescale_corner line 496
46. theorem OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.exists_cutoff_relations line 506
47. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.cutoffHom line 526