OAI/Dynamics/EntropyCounterexample/RealAngularDerivative.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.norm_fderiv_real_cutoff_angular_power line 13
2. theorem OAI.Problem340.norm_fderiv_real_cutoff_angular_power_le line 27
3. theorem OAI.Problem340.contDiff_real_cutoff_angular_power line 41
4. theorem OAI.Problem340.norm_fderiv_real_cutoff_phase_power_le line 53
5. theorem OAI.Problem340.norm_real_cutoff_phase_power_le_one line 75
6. theorem OAI.Problem340.norm_add_fderiv_real_cutoff_phase_power_le line 86
7. theorem OAI.Problem340.exists_real_cutoff_phase_power_bound line 101