OAI/Dynamics/EntropyCounterexample/SphereCutoffBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.SphereCutoffs.exists_fderiv_affinePreparationCutoff_bound line 11
2. theorem OAI.Problem340.SphereCutoffs.exists_fderiv_bound_of_constant_tails line 18
3. theorem OAI.Problem340.SphereCutoffs.exists_fderiv_bound_comp_linear line 42
4. theorem OAI.Problem340.SphereCutoffs.exists_fderiv_clockGateAmbient_bound line 55
5. theorem OAI.Problem340.SphereCutoffs.exists_fderiv_preparationCutoffAmbient_bound line 71