OAI/Combinatorics/UniformKServer/PilotConcentration.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Scalar slope proofs for exact compact pilot.

  1. theorem OAI.UniformKServer.PilotCompact.near_deficit line 9
  2. theorem OAI.UniformKServer.PilotCompact.nearWeight_large line 77
  3. theorem OAI.UniformKServer.PilotCompact.near_positive_unique line 107
  4. theorem OAI.UniformKServer.PilotCompact.nearWeight_eq_site line 118
  5. theorem OAI.UniformKServer.PilotCompact.near_site_exists line 134
  6. theorem OAI.UniformKServer.PilotCompact.clamp_abs line 175
  7. theorem OAI.UniformKServer.PilotCompact.bumpB_lipschitz line 184
  8. theorem OAI.UniformKServer.PilotCompact.gate_lipschitz line 192
  9. theorem OAI.UniformKServer.PilotCompact.capped_square_order line 200
  10. theorem OAI.UniformKServer.PilotCompact.capped_square_abs line 216
  11. theorem OAI.UniformKServer.PilotCompact.quadratic_abs line 226
  12. theorem OAI.UniformKServer.PilotCompact.tail_abs line 234
  13. theorem OAI.UniformKServer.PilotCompact.bumpA_tail line 243
  14. theorem OAI.UniformKServer.PilotCompact.bumpA_at_R line 252
  15. theorem OAI.UniformKServer.PilotCompact.bumpA_cross line 260
  16. theorem OAI.UniformKServer.PilotCompact.bumpA_lipschitz line 287
  17. def OAI.UniformKServer.PilotCompact.relocate line 308
  18. theorem OAI.UniformKServer.PilotCompact.trim_contribution line 313
  19. theorem OAI.UniformKServer.PilotCompact.trim_add_le line 329