OAI/Analysis/Triangular/Schwartz/Realness.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AtomicTriangular.Construction.P_conj line 10
2. lemma OAI.AtomicTriangular.Construction.dslope_conj_real line 14
3. lemma OAI.AtomicTriangular.Construction.dBasis_conj line 32
4. lemma OAI.AtomicTriangular.Construction.cBasis_conj line 34
5. lemma OAI.AtomicTriangular.Construction.finiteC_conj line 36
6. lemma OAI.AtomicTriangular.Construction.finiteD_conj line 39
7. lemma OAI.AtomicTriangular.Construction.tailInput_conj line 42
8. lemma OAI.AtomicTriangular.Construction.finiteInput_conj line 44
9. lemma OAI.AtomicTriangular.Construction.inputComplex_real line 47
10. lemma OAI.AtomicTriangular.Construction.inputComplex_re line 49
11. lemma OAI.AtomicTriangular.Construction.inputComplex_eq line 52
12. def OAI.AtomicTriangular.Construction.complexInputSchwartz line 56
13. lemma OAI.AtomicTriangular.Construction.complexInputSchwartz_apply line 58
14. lemma OAI.AtomicTriangular.Construction.radial_neg line 62
15. lemma OAI.AtomicTriangular.Construction.inputComplex_even line 63
16. lemma OAI.AtomicTriangular.Construction.fourier_conj_even line 65