OAI/Analysis/DiagonalForms.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DiagonalForms.System.logMean line 14
  2. theorem OAI.QuantumCalculus.integral_exp_affine_log line 18
  3. theorem OAI.DiagonalForms.System.logMean_self line 39
  4. theorem OAI.DiagonalForms.System.logMean_symm line 40
  5. theorem OAI.DiagonalForms.System.logMean_pos line 46
  6. theorem OAI.DiagonalForms.System.logMean_le_arithmetic line 53
  7. theorem OAI.DiagonalForms.System.logMean_exp_mul_f line 75
  8. theorem OAI.DiagonalForms.System.logMean_mul_f line 101
  9. theorem OAI.DiagonalForms.System.logMean_arithmetic_plus line 105
  10. theorem OAI.DiagonalForms.System.logMean_arithmetic_minus line 112
  11. theorem OAI.DiagonalForms.System.logMean_product line 119
  12. theorem OAI.DiagonalForms.System.logMean_scale line 138
  13. theorem OAI.DiagonalForms.System.logMean_mono line 147
  14. structure OAI.DiagonalForms.System line 181
  15. def OAI.DiagonalForms.System.sourceForm line 194
  16. def OAI.DiagonalForms.System.Comparison line 197
  17. def OAI.DiagonalForms.System.multiplier line 201
  18. theorem OAI.DiagonalForms.System.multiplier_apply line 204
  19. theorem OAI.DiagonalForms.System.source_summable line 207
  20. theorem OAI.DiagonalForms.System.comparison_add line 220
  21. theorem OAI.DiagonalForms.System.comparison_smul line 228
  22. def OAI.DiagonalForms.System.parallel line 235
  23. theorem OAI.DiagonalForms.System.parallel_pos line 237
  24. theorem OAI.DiagonalForms.System.parallel_norm_bound line 241
  25. theorem OAI.DiagonalForms.System.parallel_minimum line 248
  26. theorem OAI.DiagonalForms.System.comparison_parallel line 256
  27. theorem OAI.DiagonalForms.System.sourceForm_finite line 288
  28. theorem OAI.DiagonalForms.System.sourceForm_tendsto line 316
  29. theorem OAI.DiagonalForms.System.comparison_tendsto line 323
  30. theorem OAI.DiagonalForms.System.comparison_zero line 331
  31. theorem OAI.DiagonalForms.System.comparison_finsetSum line 335
  32. theorem OAI.DiagonalForms.System.comparison_tsum line 345
  33. theorem OAI.DiagonalForms.System.parallel_inv line 361
  34. theorem OAI.DiagonalForms.System.comparison_harmonic_sum_pos line 367
  35. theorem OAI.DiagonalForms.System.comparison_harmonic_sum line 395
  36. theorem OAI.DiagonalForms.System.integral_comp_simpleFunc line 419
  37. theorem OAI.DiagonalForms.System.comparison_harmonic_sum_add line 441
  38. def OAI.DiagonalForms.System.compactApprox line 474
  39. theorem OAI.DiagonalForms.System.integral_compactApprox_tendsto line 477
  40. theorem OAI.DiagonalForms.System.comparison_integral line 492
  41. theorem OAI.DiagonalForms.System.comparison_inverse_integral_add line 507
  42. theorem OAI.DiagonalForms.System.comparison_harmonic_sum_nonneg line 534
  43. theorem OAI.DiagonalForms.System.comparison_inverse_integral line 551
  44. abbrev OAI.DiagonalForms.System.UnitInterval line 584
  45. theorem OAI.DiagonalForms.System.integral_unitInterval line 586
  46. theorem OAI.DiagonalForms.System.unitInterval_volume line 591
  47. theorem OAI.DiagonalForms.System.affine_pos line 594
  48. theorem OAI.DiagonalForms.System.integral_affine_inv line 600
  49. theorem OAI.DiagonalForms.System.comparison_logMean line 615
  50. theorem OAI.DiagonalForms.System.inverse_logMean_inverse line 640
  51. theorem OAI.DiagonalForms.System.comparison_dualLogMean line 656
  52. def OAI.DiagonalForms.System.resolventWeight line 693
  53. theorem OAI.DiagonalForms.System.resolvent_kernel_pos line 696
  54. theorem OAI.DiagonalForms.System.comparison_resolvent line 703
  55. theorem OAI.DiagonalForms.System.resolventWeight_pos line 754
  56. theorem OAI.DiagonalForms.System.continuous_resolvent_affine line 760
  57. theorem OAI.DiagonalForms.System.comparison_resolvent_average line 779
  58. theorem OAI.DiagonalForms.System.continuous_resolvent_comp line 823
  59. theorem OAI.DiagonalForms.System.continuousOn_resolventWeight line 837
  60. def OAI.DiagonalForms.System.fiveQuadratic line 849
  61. theorem OAI.DiagonalForms.System.comparison_fiveQuadratic line 856