OAI/Combinatorics/Sidorenko/Coercivity.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SidorenkoCounterexample.quadratic_ge_right line 7
2. theorem OAI.SidorenkoCounterexample.quadratic_ge_endpoints line 15
3. theorem OAI.SidorenkoCounterexample.coercivity_scalar_pos line 34

   Source documentation

   The scalar minimization for nonnegative δ, without analytic derivatives.

   theorem coercivity_scalar_pos (P T δ : ℝ) (hP : 0 ≤ P) (hδ : 0 ≤ δ)
       (_hT : 0 ≤ T) (hTP : T ≤ P + 3 * δ) :
       (P ^ 2 + δ ^ 2) / 18 ≤
         3 * δ ^ 2 / 4 + (2 * P - T) ^ 2 / 18 + (5 * P - T) * δ / 6 -
           (min (P / 3 + δ) ((P - T + 3 * δ) / 2)) ^ 2 / 2 := by
   …

4. theorem OAI.SidorenkoCounterexample.coercivity_scalar_neg line 56

   Source documentation

   The scalar minimization used after δ = -y and P = x + 3y.

   theorem coercivity_scalar_neg (x T y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y)
       (_hT : 0 ≤ T) (hTx : T ≤ x) :
       (x ^ 2 + y ^ 2) / 18 ≤
         y ^ 2 / 4 + (2*x-T)*y/3 + (2*x-T)^2/18 -
           (min (x/3) ((x-T)/2))^2/2 := by
   …

5. def OAI.SidorenkoCounterexample.scalarForm line 76

   Source documentation

   Scalar lower bound after controlling the v-term and applying Cauchy–Schwarz.

   noncomputable def scalarForm (c d P T δ : ℝ) : ℝ :=
   …

6. theorem OAI.SidorenkoCounterexample.coercivity_scalar line 80
7. def OAI.SidorenkoCounterexample.quadraticPart line 113

   Source documentation

   Exactly the homogeneous quadratic part of equation (tail-linear-loss).

   noncomputable def quadraticPart (c d δ v : ℝ) (p t : Fin 3 → ℝ) : ℝ :=
   …

8. theorem OAI.SidorenkoCounterexample.three_sq line 118
9. theorem OAI.SidorenkoCounterexample.coercivity line 124

   Source documentation

   Manuscript Lemma lem:coercivity, with every feasibility condition explicit. No dimension-dependent error term or asymptotic assumption occurs here.

   theorem coercivity (c d δ v : ℝ) (p t : Fin 3 → ℝ)
       (hc : |δ| ≤ c) (hd : (∑ i, p i)+(∑ i, t i) ≤ d)
       (hp : ∀ i, 0 ≤ p i) (ht : ∀ i, 0 ≤ t i) (hv : 0 ≤ v)
       (htp : ∀ i, t i ≤ p i+δ) (hvp : ∀ i, v ≤ p i+δ)
       (hw : 0 ≤ (d-3*δ)/2-(∑ i, p i)+v) :
       ((∑ i, p i)^2+(∑ i, t i)^2+δ^2)/342 + (c-|δ|)*(d+3*δ)/12 ≤
         quadraticPart c d δ v p t := by
   …

   Mentions: OAI.SidorenkoCounterexample.quadraticPart

10. def OAI.SidorenkoCounterexample.triangular line 177
11. def OAI.SidorenkoCounterexample.baseline line 180

    Source documentation

    The face baseline β=C/2-∑b(h)/6, after D=d+c and s=p+t.

    noncomputable def baseline (c d : ℝ) (p t : Fin 3 → ℝ) : ℝ :=
    …

12. def OAI.SidorenkoCounterexample.plantedGain line 186
13. theorem OAI.SidorenkoCounterexample.slack_identity line 192

    Source documentation

    Equation (slack), with the actual baseline and gain, not a new bound.

    theorem slack_identity (c d δ v : ℝ) (p t : Fin 3 → ℝ) :
        baseline c d p t - plantedGain c d δ v p t =
        (c*(d+δ-1)-δ*(d+2)+2*δ^2)/4 +
        (∑ i, ((2*p i-t i)*(2*p i-t i-1)/6 + δ*p i-c*(p i+t i)/6)) +
        v*((d-3*δ)/2-(∑ i, p i)+v) - triangular v := by
    …

    Mentions: OAI.SidorenkoCounterexample.baseline, OAI.SidorenkoCounterexample.plantedGain, OAI.SidorenkoCounterexample.triangular

14. theorem OAI.SidorenkoCounterexample.slack_quadratic line 201

    Source documentation

    Equation (tail-linear-loss).

    theorem slack_quadratic (c d δ v : ℝ) (p t : Fin 3 → ℝ) :
        baseline c d p t - plantedGain c d δ v p t =
        quadraticPart c d δ v p t - c/4 - δ/2 -
          (2*(∑ i, p i)-(∑ i, t i))/6-v/2 := by
    …

    Mentions: OAI.SidorenkoCounterexample.baseline, OAI.SidorenkoCounterexample.plantedGain, OAI.SidorenkoCounterexample.quadraticPart

15. theorem OAI.SidorenkoCounterexample.slack_uniform_linear line 210

    Source documentation

    Uniform linear loss on a face, as used in (tail-budget).

    theorem slack_uniform_linear (c d δ v M : ℝ) (p t : Fin 3 → ℝ)
        (hc : 0 ≤ c) (hδ : δ ≤ c) (hv : v ≤ M)
        (hP : (∑ i, p i) ≤ 3*(M-c)) (hT : 0 ≤ ∑ i, t i) :
        quadraticPart c d δ v p t - 3*M/2 ≤
          baseline c d p t - plantedGain c d δ v p t := by
    …

    Mentions: OAI.SidorenkoCounterexample.quadraticPart, OAI.SidorenkoCounterexample.baseline, OAI.SidorenkoCounterexample.plantedGain

16. theorem OAI.SidorenkoCounterexample.slack_leading_coefficient line 219

    Source documentation

    The leading coefficient in d is exactly (c-δ+2v)/4.

    theorem slack_leading_coefficient (c d δ v : ℝ) (p t : Fin 3 → ℝ) :
        baseline c d p t - plantedGain c d δ v p t =
        ((c-δ+2*v)/4)*d + baseline c 0 p t - plantedGain c 0 δ v p t := by
    …

    Mentions: OAI.SidorenkoCounterexample.baseline, OAI.SidorenkoCounterexample.plantedGain

17. theorem OAI.SidorenkoCounterexample.slack_integer_regime line 227

    Source documentation

    Equation (tail-integer-slack), after the bounded-dimension argument forces u=c, δ=c and v=0.

    theorem slack_integer_regime (c d : ℝ) (p t : Fin 3 → ℝ) :
        baseline c d p t - plantedGain c d c 0 p t =
        (3*c^2-3*c)/4 +
          (∑ i, ((2*p i-t i)^2+(c-1)*(2*p i-t i)+3*c*p i))/6 := by
    …

    Mentions: OAI.SidorenkoCounterexample.baseline, OAI.SidorenkoCounterexample.plantedGain

18. theorem OAI.SidorenkoCounterexample.slack_pos_of_two_le line 236

    Source documentation

    For common dimension at least two, the eventual integer-regime slack is strictly positive. This needs no rounding relaxation.

    theorem slack_pos_of_two_le (c d : ℝ) (p t : Fin 3 → ℝ)
        (hc : 2 ≤ c) (hp : ∀ i, 0 ≤ p i) :
        0 < baseline c d p t - plantedGain c d c 0 p t := by
    …

    Mentions: OAI.SidorenkoCounterexample.baseline, OAI.SidorenkoCounterexample.plantedGain

19. theorem OAI.SidorenkoCounterexample.integer_pair_slack line 251

    Source documentation

    The zero-common-dimension local equality calculation must use integer parameters; the corresponding assertion is false for general real tuples.

    theorem integer_pair_slack (p t : ℤ) (hp : 0 ≤ p) (ht : 0 ≤ t) (htp : t ≤ p) :
        0 ≤ (2*p-t)*(2*p-t-1) ∧
          ((2*p-t)*(2*p-t-1) = 0 ↔ (p=0 ∧ t=0) ∨ (p=1 ∧ t=1)) := by
    …

20. def OAI.SidorenkoCounterexample.faceBaseline line 271
21. theorem OAI.SidorenkoCounterexample.triangular_nonneg line 274
22. theorem OAI.SidorenkoCounterexample.triangular_pos line 276
23. theorem OAI.SidorenkoCounterexample.triangular_mono line 278
24. theorem OAI.SidorenkoCounterexample.triangular_nat line 282
25. theorem OAI.SidorenkoCounterexample.faceBaseline_lower line 288
26. theorem OAI.SidorenkoCounterexample.half_triangular_bounds line 301
27. theorem OAI.SidorenkoCounterexample.lower_active_slack line 341
28. structure OAI.SidorenkoCounterexample.TailTuple line 385
29. def OAI.SidorenkoCounterexample.TailTuple.s line 392
30. def OAI.SidorenkoCounterexample.TailTuple.h line 393
31. def OAI.SidorenkoCounterexample.TailTuple.maxH line 394
32. def OAI.SidorenkoCounterexample.TailTuple.delta line 395
33. def OAI.SidorenkoCounterexample.TailTuple.P line 396
34. def OAI.SidorenkoCounterexample.TailTuple.T line 397
35. def OAI.SidorenkoCounterexample.TailTuple.Q line 398
36. def OAI.SidorenkoCounterexample.TailTuple.energy line 400
37. def OAI.SidorenkoCounterexample.tailGain line 402
38. def OAI.SidorenkoCounterexample.tailSlack line 405
39. def OAI.SidorenkoCounterexample.tailEnergy line 407
40. def OAI.SidorenkoCounterexample.TailFeasible line 410
41. theorem OAI.SidorenkoCounterexample.TailTuple.h_le_max line 417
42. theorem OAI.SidorenkoCounterexample.TailTuple.exists_max line 419
43. theorem OAI.SidorenkoCounterexample.TailTuple.c_le_max line 422
44. theorem OAI.SidorenkoCounterexample.TailTuple.p_le_h line 424
45. theorem OAI.SidorenkoCounterexample.TailTuple.t_le_h line 426
46. theorem OAI.SidorenkoCounterexample.TailTuple.s_le_h line 428
47. theorem OAI.SidorenkoCounterexample.TailTuple.delta_abs_le line 430
48. theorem OAI.SidorenkoCounterexample.TailTuple.baseline line 435
49. theorem OAI.SidorenkoCounterexample.TailFeasible.sum_le line 440
50. theorem OAI.SidorenkoCounterexample.TailFeasible.d_delta_nonneg line 448
51. theorem OAI.SidorenkoCounterexample.TailFeasible.energy_nonneg line 457
52. theorem OAI.SidorenkoCounterexample.TailFeasible.coercivity line 466
53. theorem OAI.SidorenkoCounterexample.TailFeasible.v_le_max line 478
54. theorem OAI.SidorenkoCounterexample.tailEnergy_nonneg line 488
55. theorem OAI.SidorenkoCounterexample.tailSlack_energy_lower line 494
56. def OAI.SidorenkoCounterexample.pairVertices line 532
57. def OAI.SidorenkoCounterexample.facePair line 533
58. def OAI.SidorenkoCounterexample.pairFace line 534
59. def OAI.SidorenkoCounterexample.pairParent line 535
60. def OAI.SidorenkoCounterexample.pairBridge line 536
61. def OAI.SidorenkoCounterexample.faceBit line 537
62. def OAI.SidorenkoCounterexample.separationCount line 538
63. theorem OAI.SidorenkoCounterexample.faces_card line 540
64. theorem OAI.SidorenkoCounterexample.pairVertices_card line 541
65. theorem OAI.SidorenkoCounterexample.pairVertices_injective line 542
66. theorem OAI.SidorenkoCounterexample.facePair_injective line 543
67. theorem OAI.SidorenkoCounterexample.facePair_correct line 544
68. theorem OAI.SidorenkoCounterexample.pairFace_correct line 545
69. theorem OAI.SidorenkoCounterexample.pairFace_injective line 546
70. theorem OAI.SidorenkoCounterexample.pairParent_lt line 547
71. theorem OAI.SidorenkoCounterexample.pairBridge_self line 548
72. theorem OAI.SidorenkoCounterexample.pairBridge_parent line 549
73. theorem OAI.SidorenkoCounterexample.separationCount_pos line 550
74. theorem OAI.SidorenkoCounterexample.separationCount_root line 551
75. theorem OAI.SidorenkoCounterexample.separationCount_le line 552
76. theorem OAI.SidorenkoCounterexample.root_pair line 553
77. theorem OAI.SidorenkoCounterexample.nonnegative_interval_sq line 559
78. theorem OAI.SidorenkoCounterexample.tail_pair_energy line 566
79. theorem OAI.SidorenkoCounterexample.parent_energy_bound line 584
80. def OAI.SidorenkoCounterexample.separationExcess line 607
81. def OAI.SidorenkoCounterexample.GlobalTailFeasible line 610
82. theorem OAI.SidorenkoCounterexample.separationExcess_nonneg line 614
83. theorem OAI.SidorenkoCounterexample.separationExcess_root line 620
84. theorem OAI.SidorenkoCounterexample.global_tail_budget line 632
85. def OAI.SidorenkoCounterexample.tailPairBound line 655

    Source documentation

    A deliberately coarse but absolute bound on unseparated pair dimensions. It replaces the manuscript's unbounded-subsequence argument by a finite energy propagation along a certified spanning tree of the exact complex.

    def tailPairBound : ℕ := 2*4^32*22572+396

86. theorem OAI.SidorenkoCounterexample.global_tail_pair_bound line 657
87. structure OAI.SidorenkoCounterexample.TailBox line 702
88. def OAI.SidorenkoCounterexample.TailBox.tuple line 710
89. def OAI.SidorenkoCounterexample.tailRemainder line 712
90. def OAI.SidorenkoCounterexample.tailLinear line 715
91. def OAI.SidorenkoCounterexample.tailRemainderBound line 716
92. theorem OAI.SidorenkoCounterexample.tailRemainderBound_nonneg line 718
93. theorem OAI.SidorenkoCounterexample.tailSlack_linear line 720
94. theorem OAI.SidorenkoCounterexample.tailLinear_nonneg line 726
95. theorem OAI.SidorenkoCounterexample.tailLinear_half line 730
96. theorem OAI.SidorenkoCounterexample.tailRemainder_bounded line 735
97. theorem OAI.SidorenkoCounterexample.tailSlack_lower_nonneg line 749
98. theorem OAI.SidorenkoCounterexample.global_maxH_bound line 758
99. theorem OAI.SidorenkoCounterexample.eventually_integer_regime line 771
100. theorem OAI.SidorenkoCounterexample.delta_integer_regime line 820
101. theorem OAI.SidorenkoCounterexample.tailSlack_integer line 822
102. theorem OAI.SidorenkoCounterexample.integer_slack_classification line 827
103. def OAI.SidorenkoCounterexample.FaceResidue line 890
104. theorem OAI.SidorenkoCounterexample.full_zero_face_residue line 893
105. theorem OAI.SidorenkoCounterexample.lower_zero_face_residue line 903
106. theorem OAI.SidorenkoCounterexample.FaceResidue.one_iff line 917
107. theorem OAI.SidorenkoCounterexample.pair_incidence_card line 927
108. theorem OAI.SidorenkoCounterexample.sum_face_pairs line 929
109. theorem OAI.SidorenkoCounterexample.residue_root_zero line 943
110. theorem OAI.SidorenkoCounterexample.residue_propagation line 949
111. theorem OAI.SidorenkoCounterexample.uniform_tail_dichotomy line 972

     Source documentation

     The exact nonsaving residue of the singular-tail exponent calculation, uniform over all corner activity patterns when D is large enough.

      theorem uniform_tail_dichotomy : ∃ D₀ : ℕ, ∀ D ≥ D₀,
         ∀ (full : Fin 22 → Bool) (a : Fin 22 → TailTuple) (h : Fin 33 → ℕ),
         GlobalTailFeasible D full a h →
         (∑ j, tailSlack D (full j) (a j))+separationExcess h ≤ 0 →
         (∀ j, (a j).c=0) ∧ (∀ e, h e=0 ∨ h e=2) ∧
         (∀ j, tailSlack D (full j) (a j)=0) ∧ separationExcess h=0 ∧
         (∑ j, tailGain D (full j) (a j))=(2/3:ℝ)*∑ e, triangular (h e) := by
     …

     Mentions: OAI.SidorenkoCounterexample.TailTuple, OAI.SidorenkoCounterexample.GlobalTailFeasible, OAI.SidorenkoCounterexample.tailSlack, OAI.SidorenkoCounterexample.separationExcess, OAI.SidorenkoCounterexample.tailGain, OAI.SidorenkoCounterexample.triangular

112. def OAI.SidorenkoCounterexample.plantedTailTuple line 1027
113. theorem OAI.SidorenkoCounterexample.plantedTailTuple_s line 1036
114. theorem OAI.SidorenkoCounterexample.plantedTailTuple_feasible line 1044
115. def OAI.SidorenkoCounterexample.fullPlantedExponent line 1091
116. theorem OAI.SidorenkoCounterexample.fullPlantedExponent_eq line 1099