OAI/Analysis/StrictMeans/FamilyDerivatives.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StrictInverseFirstPower.continuous_holomorphicFamily_deriv line 55
2. lemma OAI.StrictInverseFirstPower.complex_path_norm_hasDerivAt line 78
3. lemma OAI.StrictInverseFirstPower.complex_path_normFirst_hasDerivAt line 91
4. lemma OAI.StrictInverseFirstPower.complex_normSecond_at_one line 109
5. lemma OAI.StrictInverseFirstPower.compactFamily_hasDerivAt_integral line 124