OAI/Dynamics/EntropyCounterexample/SphereAngularInput.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.SphereAngularInput.horizontal line 11
  2. def OAI.Problem340.SphereAngularInput.phase line 13
  3. def OAI.Problem340.SphereAngularInput.angularAmbient line 15
  4. def OAI.Problem340.SphereAngularInput.angular line 18
  5. theorem OAI.Problem340.SphereAngularInput.contDiff_horizontal line 21
  6. theorem OAI.Problem340.SphereAngularInput.contDiffAt_phase line 28
  7. theorem OAI.Problem340.SphereAngularInput.contDiffAt_angularAmbient_of_horizontal line 35
  8. theorem OAI.Problem340.SphereAngularInput.angularAmbient_eq_zero_of_low line 41
  9. theorem OAI.Problem340.SphereAngularInput.angularAmbient_eq_zero_of_high line 45
  10. theorem OAI.Problem340.SphereAngularInput.contDiffAt_angularAmbient_of_low line 49
  11. theorem OAI.Problem340.SphereAngularInput.contDiffAt_angularAmbient_of_high line 57
  12. def OAI.Problem340.SphereAngularInput.regularDomain line 65
  13. theorem OAI.Problem340.SphereAngularInput.isOpen_regularDomain line 68
  14. theorem OAI.Problem340.SphereAngularInput.contDiffOn_angularAmbient line 74
  15. theorem OAI.Problem340.SphereAngularInput.sphere_mem_regularDomain line 83
  16. theorem OAI.Problem340.SphereAngularInput.continuous_angular line 97
  17. theorem OAI.Problem340.SphereAngularInput.norm_phase_le_one line 104
  18. theorem OAI.Problem340.SphereAngularInput.norm_angularAmbient_le_one line 109
  19. theorem OAI.Problem340.SphereAngularInput.norm_angular_le_one line 117
  20. def OAI.Problem340.SphereAngularInput.phaseBelt line 120
  21. theorem OAI.Problem340.SphereAngularInput.isCompact_phaseBelt line 123
  22. theorem OAI.Problem340.SphereAngularInput.horizontal_ne_zero_on_phaseBelt line 128
  23. theorem OAI.Problem340.SphereAngularInput.norm_phase_eq_one line 141
  24. theorem OAI.Problem340.SphereAngularInput.exists_bounds_cutoff_and_phase line 144
  25. theorem OAI.Problem340.SphereAngularInput.fderiv_angularAmbient_eq_zero_of_low line 164
  26. theorem OAI.Problem340.SphereAngularInput.fderiv_angularAmbient_eq_zero_of_high line 173
  27. theorem OAI.Problem340.SphereAngularInput.norm_fderiv_angularAmbient_le_at line 182
  28. theorem OAI.Problem340.SphereAngularInput.exists_uniform_angular_bound line 217
  29. theorem OAI.Problem340.SphereAngularInput.exists_uniform_angular_bound_on_compact line 240
  30. theorem OAI.Problem340.SphereAngularInput.exists_uniform_angular_neighborhood line 281
  31. theorem OAI.Problem340.SphereAngularInput.phase_eq_normalize line 300
  32. theorem OAI.Problem340.SphereAngularInput.phase_eq_of_positive_scale line 304