OAI/Analysis/RieszRectifiability/Kernel/TruncationLinear.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RieszRectifiability.truncated_congr_ae line 13
2. theorem OAI.RieszRectifiability.truncated_add line 22
3. theorem OAI.RieszRectifiability.truncated_smul line 33
4. def OAI.RieszRectifiability.truncationLp line 41
5. theorem OAI.RieszRectifiability.truncationLp_coe line 46
6. theorem OAI.RieszRectifiability.truncationLp_add line 52
7. theorem OAI.RieszRectifiability.truncationLp_smul line 67
8. def OAI.RieszRectifiability.truncationLinearMap line 78