OAI/Probability/SKGap/Localization/DerivNonnegRightMin.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.deriv_nonneg_of_right_min line 150
2. lemma OAI.SKGapCutoff.hasDerivAt_norm_inverse_direction line 157
3. theorem OAI.SKGapCutoff.ball_subset_image_of_uniform_right_inverse line 180
4. lemma OAI.SKGapCutoff.injective_of_norm_lower line 241
5. lemma OAI.SKGapCutoff.exists_right_inverse_of_adjoint_lower line 253
6. theorem OAI.SKGapCutoff.ball_subset_image_of_adjoint_lower line 287