OAI/Analysis/FreeWords/SpectralClip.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKUltraTrace.clipFunction line 38
  2. def OAI.KKUltraTrace.spectralClip line 40
  3. theorem OAI.KKUltraTrace.clipFunction_zero line 53
  4. theorem OAI.KKUltraTrace.clipFunction_pos line 56
  5. theorem OAI.KKUltraTrace.continuous_clipFunction line 65
  6. def OAI.KKUltraTrace.clipWeight line 70
  7. theorem OAI.KKUltraTrace.continuous_clipWeight line 72
  8. theorem OAI.KKUltraTrace.clipWeight_bounds line 75
  9. theorem OAI.KKUltraTrace.spectralClip_eq line 99
  10. theorem OAI.KKUltraTrace.weighted_square line 108
  11. theorem OAI.KKUltraTrace.spectralClip_square line 137
  12. theorem OAI.KKUltraTrace.spectralClip_error_square line 142
  13. theorem OAI.KKUltraTrace.norm_spectralClip_le line 152
  14. theorem OAI.KKUltraTrace.spectralClip_square_le line 163
  15. theorem OAI.KKUltraTrace.spectralClip_error_square_le line 172
  16. theorem OAI.KKUltraTrace.spectralClip_right_support line 181
  17. theorem OAI.KKUltraTrace.spectralClip_eq_self line 193
  18. theorem OAI.KKUltraTrace.map_spectralClip line 210
  19. def OAI.KKUltraTrace._seqOrder line 231
  20. theorem OAI.KKUltraTrace._seqSOR line 236
  21. def OAI.KKUltraTrace.sequenceEval line 240
  22. theorem OAI.KKUltraTrace.sequenceEval_apply line 250
  23. theorem OAI.KKUltraTrace.spectralClip_apply line 252
  24. theorem OAI.KKUltraTrace.spectral_clipping_transfer line 256