OAI/Analysis/Triangular/Construction/SpectralProduct.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AtomicTriangular.Construction.tailColumnSpectral line 11
2. lemma OAI.AtomicTriangular.Construction.tailColumnSpectral_norm line 13
3. lemma OAI.AtomicTriangular.Construction.summable_l1_complex_smul line 18
4. lemma OAI.AtomicTriangular.Construction.summable_tail_columns line 25
5. lemma OAI.AtomicTriangular.Construction.tsum_prod_fin_two line 28
6. lemma OAI.AtomicTriangular.Construction.tailSpectral_product line 33
7. lemma OAI.AtomicTriangular.Construction.summable_tail_columns_apply line 39
8. lemma OAI.AtomicTriangular.Construction.tailSpectral_product_apply line 43
9. lemma OAI.AtomicTriangular.Construction.tailColumnSpectral_jet line 50
10. lemma OAI.AtomicTriangular.Construction.tailSpectral_jet line 58
11. lemma OAI.AtomicTriangular.Construction.negativeJet_add line 65
12. lemma OAI.AtomicTriangular.Construction.inputJJet_negative line 69
13. lemma OAI.AtomicTriangular.Construction.inputJJet_negative_coefficient line 74