OAI/Geometry/ProjectionBodies/ScalarBounds.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PettyProjection.Scalar.exponent line 8
2. def OAI.PettyProjection.Scalar.coefficient line 10
3. def OAI.PettyProjection.Scalar.beta line 14
4. def OAI.PettyProjection.Scalar.weight line 16
5. def OAI.PettyProjection.Scalar.e line 19
6. def OAI.PettyProjection.Scalar.M line 21
7. def OAI.PettyProjection.Scalar.W line 23
8. def OAI.PettyProjection.Scalar.G line 25
9. def OAI.PettyProjection.Scalar.D line 27
10. def OAI.PettyProjection.Scalar.I line 30

    Source documentation

    Closed form of the integral of M'(a)^2 over [1,z], or zero below 1.

    def I (n : ℕ) (z : ℝ) : ℝ :=
    …

11. def OAI.PettyProjection.Scalar.L line 38
12. lemma OAI.PettyProjection.Scalar.inverse_pow_lower line 45

    Source documentation

    A second-order lower bound for inverse powers, valid in every dimension. This is the low-z convexity estimate.

    lemma inverse_pow_lower (n : ℕ) {z : ℝ} (hz : 0 < z) (hz1 : z ≤ 1) :
        1 + n * (1 - z) + (n : ℝ) * (n + 1) / 2 * (1 - z)^2 ≤ (z⁻¹)^n := by
    …

13. lemma OAI.PettyProjection.Scalar.coefficient_pos line 71
14. lemma OAI.PettyProjection.Scalar.beta_pos line 75
15. lemma OAI.PettyProjection.Scalar.beta_lt_one line 79
16. lemma OAI.PettyProjection.Scalar.weight_pos line 83
17. lemma OAI.PettyProjection.Scalar.weight_lt_one line 87
18. lemma OAI.PettyProjection.Scalar.large_local_margin line 92

    Source documentation

    Exact positivity margin on the low-z interval in dimensions at least seven.

    lemma large_local_margin {r : ℝ} (hr : 7 ≤ r) :
        0 < r + 3 - 8 * (r^2 + 5*r + 7) / ((r+1)*(r+3)) := by
    …

19. lemma OAI.PettyProjection.Scalar.mean_bound line 109

    Source documentation

    Scalar mean bound, including every dimension.

    lemma mean_bound (n : ℕ) (hn : 4 ≤ n) :
        coefficient n * (2*n*beta n^2 / (weight n * (2*n+8)) -
          (1-beta n)^2 / (1-weight n)) ≤
          (2*(exponent n : ℝ)-1) / (exponent n : ℝ)^2 := by
    …

    Mentions: OAI.PettyProjection.Scalar.coefficient, OAI.PettyProjection.Scalar.beta, OAI.PettyProjection.Scalar.weight, OAI.PettyProjection.Scalar.exponent

20. lemma OAI.PettyProjection.Scalar.local_margin line 141
21. lemma OAI.PettyProjection.Scalar.low_W_bound line 160
22. lemma OAI.PettyProjection.Scalar.low_D_square line 176
23. lemma OAI.PettyProjection.Scalar.low_pointwise line 185
24. def OAI.PettyProjection.Scalar.P4 line 207
25. lemma OAI.PettyProjection.Scalar.certificate_4 line 209
26. def OAI.PettyProjection.Scalar.U4 line 217
27. lemma OAI.PettyProjection.Scalar.U4_pos line 219
28. lemma OAI.PettyProjection.Scalar.P4_pos line 227
29. lemma OAI.PettyProjection.Scalar.high_pointwise_4 line 237
30. def OAI.PettyProjection.Scalar.P5 line 243
31. lemma OAI.PettyProjection.Scalar.certificate_5 line 245
32. def OAI.PettyProjection.Scalar.U5 line 253
33. lemma OAI.PettyProjection.Scalar.U5_pos line 255
34. lemma OAI.PettyProjection.Scalar.P5_pos line 263
35. lemma OAI.PettyProjection.Scalar.high_pointwise_5 line 273
36. def OAI.PettyProjection.Scalar.P6 line 279
37. lemma OAI.PettyProjection.Scalar.certificate_6 line 281
38. def OAI.PettyProjection.Scalar.U6 line 289
39. lemma OAI.PettyProjection.Scalar.U6_pos line 291
40. lemma OAI.PettyProjection.Scalar.P6_pos line 295
41. lemma OAI.PettyProjection.Scalar.high_pointwise_6 line 305
42. def OAI.PettyProjection.Scalar.P7 line 311
43. lemma OAI.PettyProjection.Scalar.certificate_7 line 313
44. lemma OAI.PettyProjection.Scalar.P7_pos line 321
45. lemma OAI.PettyProjection.Scalar.high_pointwise_7 line 330
46. def OAI.PettyProjection.Scalar.P8 line 336
47. lemma OAI.PettyProjection.Scalar.certificate_8 line 338
48. lemma OAI.PettyProjection.Scalar.P8_pos line 346
49. lemma OAI.PettyProjection.Scalar.high_pointwise_8 line 355
50. def OAI.PettyProjection.Scalar.P9 line 361
51. lemma OAI.PettyProjection.Scalar.certificate_9 line 363
52. lemma OAI.PettyProjection.Scalar.P9_pos line 371
53. lemma OAI.PettyProjection.Scalar.high_pointwise_9 line 380
54. lemma OAI.PettyProjection.Scalar.choose_double line 389

    Source documentation

    The exact coefficient comparison used in the all-dimensional scalar estimate.

    lemma choose_double (n j : ℕ) : 2^j * n.choose j ≤ (2*n).choose j := by
    …

55. lemma OAI.PettyProjection.Scalar.choose_double_cubic line 409
56. def OAI.PettyProjection.Scalar.tail line 418

    Source documentation

    Taylor remainder of the n-th power after its quadratic term.

    def tail (n : ℕ) (x : ℝ) : ℝ :=
    …

57. lemma OAI.PettyProjection.Scalar.tail_nonneg line 421
58. lemma OAI.PettyProjection.Scalar.tail_expansion line 426
59. lemma OAI.PettyProjection.Scalar.tail_double line 444
60. lemma OAI.PettyProjection.Scalar.shifted_polynomial_pos line 476

    Source documentation

    Positivity mechanism for the all-dimensional polynomial. Cancellation of its first two coefficients leaves a positive quadratic term; all later coefficients are controlled by the doubled binomial comparison.

    lemma shifted_polynomial_pos (n : ℕ) (hn : 2 ≤ n) {x : ℝ} (hx : 0 < x)
        (a b c d e u v w t : ℝ)
        (hzero : a+u+t=0) (hone : 2*n*a+b+n*u+v=0)
        (htwo : 0 < ((2*n).choose 2 : ℝ)*a+2*n*b+c+(n.choose 2 : ℝ)*u+n*v+w)
        (ha : 0 ≤ a) (hau : 0 ≤ 8*a+u)
        (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d) (he : 0 ≤ e)
        (hv : 0 ≤ v) (hw : 0 ≤ w) :
        0 < (1+x)^(2*n)*(a+b*x+c*x^2+d*x^3+e*x^4)+
          (1+x)^n*(u+v*x+w*x^2)+t := by
    …

    Mentions: OAI.PettyProjection.Scalar.e

61. def OAI.PettyProjection.Scalar.largeC line 515
62. def OAI.PettyProjection.Scalar.H line 516
63. def OAI.PettyProjection.Scalar.A4 line 518
64. def OAI.PettyProjection.Scalar.A2 line 519
65. def OAI.PettyProjection.Scalar.A1 line 520
66. def OAI.PettyProjection.Scalar.A0 line 521
67. def OAI.PettyProjection.Scalar.B2 line 522
68. def OAI.PettyProjection.Scalar.B0 line 523
69. def OAI.PettyProjection.Scalar.T0 line 524
70. def OAI.PettyProjection.Scalar.q0 line 526
71. def OAI.PettyProjection.Scalar.q1 line 527
72. def OAI.PettyProjection.Scalar.q2 line 528
73. def OAI.PettyProjection.Scalar.q3 line 529
74. def OAI.PettyProjection.Scalar.q4 line 530
75. def OAI.PettyProjection.Scalar.r0 line 531
76. def OAI.PettyProjection.Scalar.r1 line 532
77. def OAI.PettyProjection.Scalar.r2 line 533
78. def OAI.PettyProjection.Scalar.V0 line 535
79. def OAI.PettyProjection.Scalar.V1 line 536
80. def OAI.PettyProjection.Scalar.V2 line 537
81. def OAI.PettyProjection.Scalar.R0 line 538
82. lemma OAI.PettyProjection.Scalar.V0_pos line 540
83. lemma OAI.PettyProjection.Scalar.V1_pos line 547
84. lemma OAI.PettyProjection.Scalar.V2_pos line 554
85. lemma OAI.PettyProjection.Scalar.R0_pos line 560
86. lemma OAI.PettyProjection.Scalar.q0_identity line 568
87. lemma OAI.PettyProjection.Scalar.q1_identity line 574
88. lemma OAI.PettyProjection.Scalar.q2_identity line 580
89. lemma OAI.PettyProjection.Scalar.r0_identity line 586
90. lemma OAI.PettyProjection.Scalar.large_signs line 592
91. lemma OAI.PettyProjection.Scalar.constant_vanish line 618
92. lemma OAI.PettyProjection.Scalar.linear_vanish line 623
93. lemma OAI.PettyProjection.Scalar.quadratic_identity line 629
94. lemma OAI.PettyProjection.Scalar.large_polynomial_pos line 636
95. lemma OAI.PettyProjection.Scalar.z_mul_inverse_pow_succ line 671
96. lemma OAI.PettyProjection.Scalar.large_I_formula line 675
97. lemma OAI.PettyProjection.Scalar.large_gap_formula line 702
98. lemma OAI.PettyProjection.Scalar.large_cleared_gap line 727
99. lemma OAI.PettyProjection.Scalar.high_pointwise_large line 739
100. theorem OAI.PettyProjection.Scalar.pointwise line 750

     Source documentation

     The pointwise scalar estimate, including its exact equality condition, in every dimension covered by the main theorem.

     theorem pointwise (n : ℕ) (hn : 4 ≤ n) {z : ℝ} (hz : 0 < z) :
         L n z ≤ 2*W n z ∧ (L n z = 2*W n z ↔ z=1) := by
     …

     Mentions: OAI.PettyProjection.Scalar.L, OAI.PettyProjection.Scalar.W