OAI/Computability/MaxCut/Games/A5Scalar.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

Finite scalar estimates in the Appendix A.5 induction

The geometric estimate retains the original positive-order condition 1 ≤ i + j + k; deleting the origin is essential when k = 0.

  1. theorem OAI.MaxCutGames.Appendix.A5Scalar.absorption line 19
  2. theorem OAI.MaxCutGames.Appendix.A5Scalar.geometric_sum_le line 43
  3. def OAI.MaxCutGames.Appendix.A5Scalar.positiveSum line 52
  4. theorem OAI.MaxCutGames.Appendix.A5Scalar.pair_sum_factor line 56
  5. theorem OAI.MaxCutGames.Appendix.A5Scalar.positiveSum_zero_eq line 64

    Source documentation

    The exact decomposition with the origin deleted.

    theorem positiveSum_zero_eq (q : ℝ) (n m : ℕ) :
    positiveSum q n m 0 =
      q * ((∑ i ∈ Finset.range n, q ^ i) * (∑ j ∈ Finset.range (m + 1), q ^ j)) +
        q * (∑ j ∈ Finset.range m, q ^ j) := by
…

    Mentions: OAI.MaxCutGames.Appendix.A5Scalar.positiveSum

  6. theorem OAI.MaxCutGames.Appendix.A5Scalar.positiveSum_zero_le line 89
  7. theorem OAI.MaxCutGames.Appendix.A5Scalar.positiveSum_pos_le line 102
  8. theorem OAI.MaxCutGames.Appendix.A5Scalar.a16_finite_geometric line 121

    Source documentation

    The original positive-order geometric bound in (A.16), with independent finite truncations. No upper bound on k is required.

    theorem a16_finite_geometric (d n m k : ℕ) (hd : 1 ≤ d) :
    (∑ i ∈ Finset.range (n + 1), ∑ j ∈ Finset.range (m + 1),
      if 1 ≤ i + j + k then ((2 : ℝ)⁻¹) ^ (63 * d * (i + j + k)) else 0) ≤
        ((2 : ℝ)⁻¹) ^ (31 * d * (k + 1)) := by
…
  9. theorem OAI.MaxCutGames.Appendix.A5Scalar.a16_original_range line 160
  10. abbrev OAI.MaxCutGames.Appendix.A5Passage.OuterIndex line 186
  11. def OAI.MaxCutGames.Appendix.A5Passage.LiftedA line 189
  12. def OAI.MaxCutGames.Appendix.A5Passage.LiftedB line 192
  13. abbrev OAI.MaxCutGames.Appendix.A5Passage.Pair line 195
  14. abbrev OAI.MaxCutGames.Appendix.A5Passage.Passage line 198
  15. theorem OAI.MaxCutGames.Appendix.A5Passage.comap_mkQ_injective line 201
  16. theorem OAI.MaxCutGames.Appendix.A5Passage.map_subtype_injective line 210
  17. theorem OAI.MaxCutGames.Appendix.A5Passage.outer_eq_of_lifted line 231
  18. theorem OAI.MaxCutGames.Appendix.A5Passage.recover_liftedA line 236
  19. theorem OAI.MaxCutGames.Appendix.A5Passage.recover_liftedB line 239
  20. def OAI.MaxCutGames.Appendix.A5Passage.forget line 242
  21. theorem OAI.MaxCutGames.Appendix.A5Passage.forget_injective line 245
  22. theorem OAI.MaxCutGames.Appendix.A5Passage.forget_val line 265
  23. instance OAI.MaxCutGames.Appendix.A5Passage.pairFintype line 270
  24. theorem OAI.MaxCutGames.Appendix.A5Passage.dim_pairA line 282
  25. theorem OAI.MaxCutGames.Appendix.A5Passage.codim_pairB line 292
  26. theorem OAI.MaxCutGames.Appendix.A5Passage.pair_order line 306
  27. theorem OAI.MaxCutGames.Appendix.A5Passage.pair_order_le line 313
  28. theorem OAI.MaxCutGames.Appendix.A5Passage.pair_rank line 320
  29. theorem OAI.MaxCutGames.Appendix.A5Passage.descendant_rank line 328
  30. theorem OAI.MaxCutGames.Appendix.A5Passage.effective_order_rank line 337
  31. theorem OAI.MaxCutGames.Appendix.A5Passage.effective_order_rank_le line 350
  32. theorem OAI.MaxCutGames.Appendix.A5Passage.effective_order_rank_pos line 366
  33. def OAI.MaxCutGames.Appendix.A5Passage.descendantSum line 377
  34. theorem OAI.MaxCutGames.Appendix.A5Passage.descendantSum_nonneg line 386
  35. theorem OAI.MaxCutGames.Appendix.F1Gram.gram_energy_le line 401

    Source documentation

    The squared entries of a Gram matrix are bounded by the squared total energy of its underlying rows. This is a pairwise Cauchy–Schwarz argument.

    theorem gram_energy_le {R C : Type*} [Fintype R] [Fintype C] (p : R → C → ℝ) :
    (∑ r, ∑ s, (∑ c, p r c * p s c)^2) ≤
      (∑ r, ∑ c, p r c^2)^2 := by
…
  36. theorem OAI.MaxCutGames.Appendix.F1Gram.sum_subtype_eq line 416
  37. theorem OAI.MaxCutGames.Appendix.F1Gram.sum_comp_le line 433
  38. def OAI.MaxCutGames.Appendix.SubspaceExtensions.horizontal line 453
  39. def OAI.MaxCutGames.Appendix.SubspaceExtensions.hKernel line 454
  40. def OAI.MaxCutGames.Appendix.SubspaceExtensions.scalarMap line 456
  41. def OAI.MaxCutGames.Appendix.SubspaceExtensions.extension line 461
  42. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.extension_mem line 465
  43. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.mkQ_eq_smul_iff line 470
  44. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.hKernel_horizontal line 477
  45. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.hKernel_extension line 482
  46. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.exists_one_extension line 489
  47. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.eq_extension_of_one_mem line 493
  48. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.eq_horizontal_of_no_one line 507
  49. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.horizontal_ne_extension line 526
  50. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.extension_injective line 533
  51. def OAI.MaxCutGames.Appendix.SubspaceExtensions.encode line 541
  52. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.encode_injective line 545
  53. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.encode_surjective line 569
  54. def OAI.MaxCutGames.Appendix.SubspaceExtensions.splitEquiv line 576
  55. def OAI.MaxCutGames.Appendix.SubspaceExtensions.horizontalEquiv line 579
  56. def OAI.MaxCutGames.Appendix.SubspaceExtensions.extensionEquiv line 592
  57. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.finrank_horizontal line 632
  58. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.finrank_extension line 635
  59. def OAI.MaxCutGames.Appendix.SubspaceExtensions.weightedTotal line 649
  60. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.card_eq_pow_finrank line 651
  61. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.quotient_card_mul_pow line 659
  62. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.weightedTotal_prod line 666
  63. def OAI.MaxCutGames.Appendix.SubspaceExtensions.mobiusWeight line 692
  64. def OAI.MaxCutGames.Appendix.SubspaceExtensions.mobiusTotal line 696
  65. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.mobiusTotal_prod line 699
  66. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.map_inverse line 722
  67. def OAI.MaxCutGames.Appendix.SubspaceExtensions.subspaceEquiv line 727
  68. def OAI.MaxCutGames.Appendix.SubspaceExtensions.subspaceMapEquiv line 733
  69. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.finrank_map_equiv line 745
  70. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.weightedTotal_equiv line 748
  71. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.mobiusTotal_equiv line 761
  72. def OAI.MaxCutGames.Appendix.SubspaceExtensions.coordinateSplit line 765
  73. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.mobiusTotal_subsingleton line 779
  74. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.coordinate_total_succ line 796
  75. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.mobiusTotal_eq_if line 805
  76. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.mobiusWeight_closed line 812
  77. theorem OAI.MaxCutGames.Appendix.SubspaceExtensions.binary_subspace_mobius line 821