OAI/Computability/MaxCut/Games/Clone100Counting.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

The concrete clone sample space. Global distinctness is a stronger conditioning rule than distinctness only at repeated original «variables». It retains the same 3/100 bound and makes the number of copies uniform.

  1. abbrev OAI.MaxCutGames.Outer.Clone100Counting.Index line 12
  2. abbrev OAI.MaxCutGames.Outer.Clone100Counting.Triple line 13
  3. def OAI.MaxCutGames.Outer.Clone100Counting.sign line 15
  4. def OAI.MaxCutGames.Outer.Clone100Counting.bias line 17
  5. def OAI.MaxCutGames.Outer.Clone100Counting.majorityBit line 20

    Source documentation

    A deterministic majority, resolving a zero bias to false.

    def majorityBit (f : Index → Bool) : Bool := decide (bias f < 0)

    Mentions: OAI.MaxCutGames.Outer.Clone100Counting.Index, OAI.MaxCutGames.Outer.Clone100Counting.bias

  6. theorem OAI.MaxCutGames.Outer.Clone100Counting.majority_aligned_nonneg line 22
  7. def OAI.MaxCutGames.Outer.Clone100Counting.parityIndicator line 29
  8. theorem OAI.MaxCutGames.Outer.Clone100Counting.parityIndicator_nonneg line 32
  9. theorem OAI.MaxCutGames.Outer.Clone100Counting.parityIndicator_le_one line 37
  10. theorem OAI.MaxCutGames.Outer.Clone100Counting.parityIndicator_eq line 42
  11. def OAI.MaxCutGames.Outer.Clone100Counting.unconditionedScore line 48
  12. theorem OAI.MaxCutGames.Outer.Clone100Counting.independent_product_sum line 51
  13. theorem OAI.MaxCutGames.Outer.Clone100Counting.unconditionedScore_eq line 60
  14. theorem OAI.MaxCutGames.Outer.Clone100Counting.unconditionedScore_le_one line 80
  15. theorem OAI.MaxCutGames.Outer.Clone100Counting.signed_product_of_failure line 88
  16. theorem OAI.MaxCutGames.Outer.Clone100Counting.unconditionedScore_le_half_of_failure line 97

    Source documentation

    An equation violated by the majority assignment is satisfied by independent clone labels with probability at most one half. This also allows repeated original variable names: independence belongs to the sampled clone indices.

    theorem unconditionedScore_le_half_of_failure (p q r : Index → Bool) (rhs : Bool)
    (h : (xor (xor (majorityBit p) (majorityBit q)) (majorityBit r) == rhs) = false) :
    unconditionedScore p q r rhs ≤ 1 / 2 := by
…

    Mentions: OAI.MaxCutGames.Outer.Clone100Counting.Index, OAI.MaxCutGames.Outer.Clone100Counting.majorityBit, OAI.MaxCutGames.Outer.Clone100Counting.unconditionedScore

  17. theorem OAI.MaxCutGames.Outer.Clone100Counting.unconditionedScore_le line 108
  18. theorem OAI.MaxCutGames.Outer.Clone100Counting.condition_970200_le line 131

    Source documentation

    Conditioning a bounded function onto 970200 of one million outcomes changes its upper expectation by at most 3/100. The exact loss is 298/10000. Only finite sums and the actual accepted sample cardinality are needed.

    theorem condition_970200_le {T : Type*} [Fintype T]
    (good : T → Prop) [DecidablePred good]
    (_hT : Fintype.card T = 1000000)
    (hgood : Fintype.card {t : T // good t} = 970200)
    (f : T → ℚ) (hf0 : ∀ t, 0 ≤ f t) (hf1 : ∀ t, f t ≤ 1) :
    (∑ t : {t : T // good t}, f t.val) / 970200 ≤
      (∑ t : T, f t) / 1000000 + 3 / 100 := by
…
  19. def OAI.MaxCutGames.Outer.Clone100Counting.conditionedScore line 150
  20. theorem OAI.MaxCutGames.Outer.Clone100Counting.conditionedScore_le line 155
  21. abbrev OAI.MaxCutGames.Outer.Clone100Triples.Index line 177
  22. abbrev OAI.MaxCutGames.Outer.Clone100Triples.Triple line 178
  23. def OAI.MaxCutGames.Outer.Clone100Triples.good line 180
  24. instance OAI.MaxCutGames.Outer.Clone100Triples.(instance at line 183) line 183
  25. abbrev OAI.MaxCutGames.Outer.Clone100Triples.GoodTriple line 185
  26. def OAI.MaxCutGames.Outer.Clone100Triples.toEmbedding line 187
  27. def OAI.MaxCutGames.Outer.Clone100Triples.fromEmbedding line 196
  28. def OAI.MaxCutGames.Outer.Clone100Triples.embeddingEquiv line 204
  29. theorem OAI.MaxCutGames.Outer.Clone100Triples.card_goodTriple line 214
  30. theorem OAI.MaxCutGames.Outer.Clone100Triples.card_triple line 218
  31. instance OAI.MaxCutGames.Outer.Clone100Triples.(instance at line 221) line 221
  32. def OAI.MaxCutGames.Outer.Clone100.triples line 234
  33. theorem OAI.MaxCutGames.Outer.Clone100.triples_length line 236
  34. def OAI.MaxCutGames.Outer.Clone100.clone line 239
  35. theorem OAI.MaxCutGames.Outer.Clone100.clone_distinct line 242
  36. theorem OAI.MaxCutGames.Outer.Clone100.clone_lift line 250
  37. def OAI.MaxCutGames.Outer.Clone100.nameEquiv line 253
  38. def OAI.MaxCutGames.Outer.Clone100.equation line 255
  39. theorem OAI.MaxCutGames.Outer.Clone100.equation_distinct line 260
  40. def OAI.MaxCutGames.Outer.Clone100.equations line 269
  41. theorem OAI.MaxCutGames.Outer.Clone100.equations_length line 273
  42. theorem OAI.MaxCutGames.Outer.Clone100.equations_nonempty line 282
  43. def OAI.MaxCutGames.Outer.Clone100.clonedInput line 288
  44. def OAI.MaxCutGames.Outer.Clone100.clonedSource line 293
  45. theorem OAI.MaxCutGames.Outer.Clone100.clonedSource_distinct line 296
  46. def OAI.MaxCutGames.Outer.Clone100.lift line 312
  47. theorem OAI.MaxCutGames.Outer.Clone100.equation_lift line 315
  48. theorem OAI.MaxCutGames.Outer.Clone100.completeness_count line 319
  49. def OAI.MaxCutGames.Outer.Clone100.success line 332
  50. theorem OAI.MaxCutGames.Outer.Clone100.completeness line 335
  51. theorem OAI.MaxCutGames.Outer.Clone100.count_as_sum_inline_Clone100 line 343
  52. def OAI.MaxCutGames.Outer.Clone100.majority line 349
  53. theorem OAI.MaxCutGames.Outer.Clone100.equation_count_le line 352
  54. theorem OAI.MaxCutGames.Outer.Clone100.soundness_count line 375
  55. theorem OAI.MaxCutGames.Outer.Clone100.soundness line 389
  56. theorem OAI.MaxCutGames.Outer.Clone100.soundness_four_fifths line 407
  57. theorem OAI.MaxCutGames.Outer.Clone100.clonedInput_bits_length_le line 416
  58. def OAI.MaxCutGames.Outer.SourceIncidence.incidence line 437
  59. theorem OAI.MaxCutGames.Outer.SourceIncidence.names_distinct line 441
  60. theorem OAI.MaxCutGames.Outer.SourceIncidence.uniform_probability_eq_expect_inline_SourceIncidence line 448
  61. theorem OAI.MaxCutGames.Outer.SourceIncidence.paritySuccess_eq line 460
  62. theorem OAI.MaxCutGames.Outer.SourceIncidence.paritySuccess_input line 480
  63. def OAI.MaxCutGames.Outer.SourceIncidence.input line 490
  64. def OAI.MaxCutGames.Outer.SourceIncidence.source line 494
  65. theorem OAI.MaxCutGames.Outer.SourceIncidence.source_distinct line 497
  66. theorem OAI.MaxCutGames.Outer.SourceIncidence.source_complete line 501
  67. theorem OAI.MaxCutGames.Outer.SourceIncidence.source_sound line 518
  68. def OAI.MaxCutGames.Outer.SourceIncidence.ordinaryGame line 534
  69. theorem OAI.MaxCutGames.Outer.SourceIncidence.ordinaryGame_projection line 538
  70. theorem OAI.MaxCutGames.Outer.SourceIncidence.ordinaryGame_sound line 542