OAI/Analysis/SymmetricDomains/ScaledRadialOperatorApply.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.Wiener.radialPoint line 23
2. lemma OAI.Release061.Wiener.radialPoint_coe line 27
3. def OAI.Release061.Wiener.schwarzDifference line 31
4. lemma OAI.Release061.Wiener.schwarzDifference_apply line 36
5. lemma OAI.Release061.Wiener.schwarzDifference_norm line 39
6. def OAI.Release061.Wiener.scaledRadialOperator line 54
7. lemma OAI.Release061.Wiener.scaledRadialOperator_norm_tendsto line 57
8. lemma OAI.Release061.Wiener.scaledRadialOperator_apply line 67