OAI/Analysis/Steinitz/FilterMoments.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Filtered moments, prefix bounds, and rank-one contractions.

  1. lemma OAI.EuclideanSteinitz.Filter.cutoff_size line 15
  2. lemma OAI.EuclideanSteinitz.Filter.cutoff_square_size line 26
  3. lemma OAI.EuclideanSteinitz.Filter.cutoff_scaled_size line 34
  4. lemma OAI.EuclideanSteinitz.Filter.squareMass_weighted line 47
  5. lemma OAI.EuclideanSteinitz.Filter.squareMass_le_weighted line 51
  6. lemma OAI.EuclideanSteinitz.Filter.coisometry_norm_le line 56
  7. lemma OAI.EuclideanSteinitz.Filter.cutoff_norm_le line 67
  8. lemma OAI.EuclideanSteinitz.Filter.lift_cutoff_contract line 73
  9. lemma OAI.EuclideanSteinitz.Filter.lift_cutoff_mass line 90
  10. lemma OAI.EuclideanSteinitz.Filter.lift_cutoff_size line 98
  11. lemma OAI.EuclideanSteinitz.Filter.weightedSq_diagonal_mono line 111
  12. lemma OAI.EuclideanSteinitz.Filter.lift_cutoff_time line 121
  13. lemma OAI.EuclideanSteinitz.Energy.finish_append line 160
  14. lemma OAI.EuclideanSteinitz.Energy.cost_append line 166
  15. lemma OAI.EuclideanSteinitz.Energy.cost_prefix line 172
  16. lemma OAI.EuclideanSteinitz.Filter.run_append line 188
  17. lemma OAI.EuclideanSteinitz.Filter.run_fresh_append line 195
  18. lemma OAI.EuclideanSteinitz.Filter.good_prefix line 207
  19. lemma OAI.EuclideanSteinitz.Filter.fresh_prefix line 211
  20. lemma OAI.EuclideanSteinitz.Filter.nodup_prefix line 215
  21. lemma OAI.EuclideanSteinitz.Filter.moves_good line 219
  22. lemma OAI.EuclideanSteinitz.Filter.cost_prefix_difference line 225
  23. lemma OAI.EuclideanSteinitz.Filter.local_prefix_increment line 234
  24. lemma OAI.EuclideanSteinitz.Filter.coisometry_column line 272
  25. lemma OAI.EuclideanSteinitz.Filter.state_trace_le line 282
  26. lemma OAI.EuclideanSteinitz.Filter.Step.b_square_le line 299
  27. lemma OAI.EuclideanSteinitz.Filter.gains_le_total line 311
  28. lemma OAI.EuclideanSteinitz.Filter.move_scale line 328
  29. lemma OAI.EuclideanSteinitz.Filter.sum_epoch_cost line 337
  30. lemma OAI.EuclideanSteinitz.Filter.sum_dyadic_le line 352
  31. def OAI.EuclideanSteinitz.Filter.vectorMass line 398
  32. def OAI.EuclideanSteinitz.Filter.eta line 399
  33. def OAI.EuclideanSteinitz.Filter.symmetricContraction line 400
  34. def OAI.EuclideanSteinitz.Filter.symmetricStep line 401
  35. lemma OAI.EuclideanSteinitz.Filter.vectorMass_nonneg line 404
  36. lemma OAI.EuclideanSteinitz.Filter.eta_pos line 406
  37. lemma OAI.EuclideanSteinitz.Filter.eta_le_one line 408
  38. lemma OAI.EuclideanSteinitz.Filter.eta_identity line 411
  39. lemma OAI.EuclideanSteinitz.Filter.rank_square line 419
  40. lemma OAI.EuclideanSteinitz.Filter.symmetricContraction_transpose line 427
  41. lemma OAI.EuclideanSteinitz.Filter.symmetricContraction_square line 430
  42. lemma OAI.EuclideanSteinitz.Filter.symmetricContraction_unit line 439
  43. lemma OAI.EuclideanSteinitz.Filter.symmetricStep_good line 460
  44. lemma OAI.EuclideanSteinitz.Filter.contraction_loss line 466
  45. lemma OAI.EuclideanSteinitz.Filter.contraction_apply line 481