OAI/Analysis/BackwardIntertwiners/ProductSymbols.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BackwardIntertwiners.linfty_ae_norm_le line 22
2. lemma OAI.BackwardIntertwiners.ae_prod_count_iff line 30
3. abbrev OAI.BackwardIntertwiners.productMeasure line 38
4. def OAI.BackwardIntertwiners.IsProductMultiplier line 40
5. lemma OAI.BackwardIntertwiners.DiagonalSymbol.product_measurable line 44
6. lemma OAI.BackwardIntertwiners.DiagonalSymbol.product_memLp line 47
7. lemma OAI.BackwardIntertwiners.diagonalOperator_isProductMultiplier line 51
8. def OAI.BackwardIntertwiners.productBoundedSymbol line 61
9. lemma OAI.BackwardIntertwiners.productBoundedSymbol_ae line 74
10. lemma OAI.BackwardIntertwiners.isProductMultiplier_mem_full line 80
11. lemma OAI.BackwardIntertwiners.fullMultiplier_mem_iff_productMultiplier line 91
12. theorem OAI.BackwardIntertwiners.polarAlgebra_mem_iff_productMultiplier line 100