OAI/Analysis/MatrixSigning/Potential/IteratedDerivCompScale.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Difference.iteratedDeriv_comp_scale line 12
2. lemma OAI.CurrentKS.Difference.line_derivative_scale line 25
3. lemma OAI.CurrentKS.Difference.bounded_directional_derivative line 34
4. lemma OAI.CurrentKS.Difference.segment_in_ball line 55
5. theorem OAI.CurrentKS.Difference.ball_quadratic_remainder line 63
6. lemma OAI.CurrentKS.Difference.quadratic_entrywise_error line 80
7. lemma OAI.CurrentKS.Difference.mixed_error line 106