OAI/Geometry/CylinderCovering/Angular/SquaredDirect.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.AngularEstimates.selected_square_remainder_identity line 8
  2. theorem OAI.AngularEstimates.selected_square_remainder_bound line 23
  3. theorem OAI.AngularEstimates.squared_profile_replacement line 47
  4. theorem OAI.AngularEstimates.squared_failure_balance line 89
  5. theorem OAI.AngularEstimates.squared_sum_remainder line 111
  6. theorem OAI.AngularEstimates.selected_slope_replacement line 149
  7. theorem OAI.AngularEstimates.squared_sector_data line 175
  8. theorem OAI.AngularEstimates.squared_sum_quotient_remainder line 195
  9. theorem OAI.AngularEstimates.squared_profiles_sum_replacement line 212
  10. theorem OAI.AngularEstimates.selected_sectors_squared_cap line 227
  11. theorem OAI.AngularEstimates.squared_radius_source_formula line 317
  12. theorem OAI.AngularEstimates.selected_sectors_cap_alternative line 324
  13. theorem OAI.AngularEstimates.uniform_squared_direct line 350