OAI/Analysis/Steinitz/Scales.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Uniform dyadic scale-energy estimates.

  1. lemma OAI.EuclideanSteinitz.Scale.size_nonneg line 11
  2. lemma OAI.EuclideanSteinitz.Scale.size_le_sqrt line 14
  3. lemma OAI.EuclideanSteinitz.Scale.size_le_inv line 19
  4. lemma OAI.EuclideanSteinitz.Scale.size_dyadic_nat line 21
  5. lemma OAI.EuclideanSteinitz.Scale.size_dyadic_neg_nat line 34
  6. lemma OAI.EuclideanSteinitz.Scale.size_normalized line 48
  7. lemma OAI.EuclideanSteinitz.Scale.dyadic_normalize line 54
  8. lemma OAI.EuclideanSteinitz.Scale.size_shifted line 63
  9. lemma OAI.EuclideanSteinitz.Scale.hasSum_decay_nat line 72
  10. lemma OAI.EuclideanSteinitz.Scale.hasSum_decay_neg line 78
  11. lemma OAI.EuclideanSteinitz.Scale.hasSum_decay line 87
  12. lemma OAI.EuclideanSteinitz.Scale.sum_decay_shift line 95
  13. lemma OAI.EuclideanSteinitz.Scale.sum_size_dyadic line 107
  14. lemma OAI.EuclideanSteinitz.Scale.potential_rate_le_size line 117
  15. lemma OAI.EuclideanSteinitz.Scale.gain_rate_le_size line 127
  16. lemma OAI.EuclideanSteinitz.Scale.sum_rates_dyadic line 151
  17. def OAI.EuclideanSteinitz.ScaleMatrix.primitiveTrace line 176
  18. def OAI.EuclideanSteinitz.ScaleMatrix.rateMatrix line 179
  19. def OAI.EuclideanSteinitz.ScaleMatrix.scaleTrace line 182
  20. def OAI.EuclideanSteinitz.ScaleMatrix.scaleRate line 185
  21. lemma OAI.EuclideanSteinitz.ScaleMatrix.primitiveTrace_eq line 188
  22. lemma OAI.EuclideanSteinitz.ScaleMatrix.primitiveTrace_derivative line 198
  23. lemma OAI.EuclideanSteinitz.ScaleMatrix.rateMatrix_cfc line 210
  24. lemma OAI.EuclideanSteinitz.ScaleMatrix.scaleRate_cfc line 228
  25. lemma OAI.EuclideanSteinitz.ScaleMatrix.scaleRate_le line 244
  26. lemma OAI.EuclideanSteinitz.ScaleMatrix.scaleTrace_derivative line 258
  27. lemma OAI.EuclideanSteinitz.ScaleMatrix.scaleTrace_mono_bound line 280
  28. lemma OAI.EuclideanSteinitz.ScaleMatrix.cfc_scaled line 296
  29. lemma OAI.EuclideanSteinitz.ScaleMatrix.scaleTrace_charpoly line 305
  30. lemma OAI.EuclideanSteinitz.ScaleMatrix.trace_charpoly line 316
  31. lemma OAI.EuclideanSteinitz.ScaleMatrix.scaleTrace_contraction_bound line 321
  32. lemma OAI.EuclideanSteinitz.ScaleMatrix.scaleTrace_eq line 346
  33. def OAI.EuclideanSteinitz.ScaleEnergy.rescale line 359
  34. lemma OAI.EuclideanSteinitz.ScaleEnergy.rescale_old line 362
  35. lemma OAI.EuclideanSteinitz.ScaleEnergy.rescale_next line 367
  36. def OAI.EuclideanSteinitz.ScaleEnergy.aggregateCost line 372
  37. def OAI.EuclideanSteinitz.ScaleEnergy.variation line 377
  38. def OAI.EuclideanSteinitz.ScaleEnergy.gainSum line 382
  39. lemma OAI.EuclideanSteinitz.ScaleEnergy.aggregateCost_le_variation line 384
  40. lemma OAI.EuclideanSteinitz.ScaleEnergy.variation_eq line 400
  41. lemma OAI.EuclideanSteinitz.ScaleEnergy.finish_psd line 410
  42. lemma OAI.EuclideanSteinitz.ScaleEnergy.variation_le line 418
  43. lemma OAI.EuclideanSteinitz.ScaleEnergy.sum_stepCost_eq line 424
  44. lemma OAI.EuclideanSteinitz.ScaleEnergy.aggregateCost_eq line 433
  45. lemma OAI.EuclideanSteinitz.ScaleEnergy.scale_energy_bound line 446