OAI/Computability/UniqueGames/Soundness/PartnerLinearLemmas.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Soundness.PartnerLinear.SourceCoordinates line 19
2. abbrev OAI.UniqueGamesTheorem.Soundness.PartnerLinear.Active line 20
3. abbrev OAI.UniqueGamesTheorem.Soundness.PartnerLinear.Inactive line 21
4. abbrev OAI.UniqueGamesTheorem.Soundness.PartnerLinear.PartnerCoordinates line 22
5. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.sourceCoordinates line 24
6. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.sourceFromCoordinates line 27
7. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.sourceEquiv line 33
8. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partnerCoordinates line 51
9. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partnerFromCoordinates line 56
10. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partnerEquiv line 67
11. instance OAI.UniqueGamesTheorem.Soundness.PartnerLinear.sourceAddCommGroup line 96
12. instance OAI.UniqueGamesTheorem.Soundness.PartnerLinear.sourceModule line 99
13. instance OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partnerAddCommGroup line 102
14. instance OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partnerModule line 105
15. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.sourceLinearEquiv line 108
16. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partnerLinearEquiv line 111
17. instance OAI.UniqueGamesTheorem.Soundness.PartnerLinear.sourceFintype line 114
18. instance OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partnerFintype line 118
19. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.source_add line 122
20. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.source_zero line 131
21. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partner_add line 137
22. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partner_zero line 150
23. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection line 156
24. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection_apply line 165
25. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection_surjective line 168
26. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.mem_projection_ker line 171
27. instance OAI.UniqueGamesTheorem.Soundness.PartnerLinear.sourceFiniteDimensional line 177
28. instance OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partnerFiniteDimensional line 181
29. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.kernelEquiv line 186

    Source documentation

    Identifies the actual linear kernel with the previously counted concrete kernel.

    noncomputable def kernelEquiv :
        (projection rhs active slot).ker ≃ KernelCardinality.Kernel rhs active slot where
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection, OAI.UniqueGamesTheorem.Soundness.KernelCardinality.Kernel

30. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection_ker_card line 193
31. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection_ker_finrank line 198
32. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection_ker_finrank_of_card line 205
33. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.source_finrank line 210
34. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.disjoint_projection_kernels line 216

    Source documentation

    Distinct coordinate blocks make disjoint active-set kernels have trivial intersection.

    theorem disjoint_projection_kernels
        (active' : P → Bool) (slot' : P → Slot)
        (hdisjoint : ∀ j, active j = true → active' j = false) :
        (projection rhs active slot).ker ⊓ (projection rhs active' slot').ker = ⊥ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection

35. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.sourceTau line 229
36. def OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partnerTau line 232
37. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.sourceTau_apply line 236
38. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.partnerTau_apply line 237
39. theorem OAI.UniqueGamesTheorem.Soundness.PartnerLinear.tau_comp_projection line 240
40. def OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.bernoulliAverage line 255

    Source documentation

    Expectation of f evaluated at the number of successes in n independent Bernoulli trials. The recursion itself specifies the product distribution.

    def bernoulliAverage (p : Rat) : Nat → (Nat → Rat) → Rat
      | 0, f => f 0
      | n + 1, f =>
          (1 - p) * bernoulliAverage p n f +
            p * bernoulliAverage p n (fun k => f (k + 1))

41. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.bernoulliAverage_scale line 261
42. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.bernoulliAverage_geometric line 270

    Source documentation

    The exact binomial generating-function identity used in (6.25).

    theorem bernoulliAverage_geometric (p a : Rat) (n : Nat) :
        bernoulliAverage p n (fun k => a ^ k) = (1 - p * (1 - a)) ^ n := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.bernoulliAverage

43. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.bernoulliAverage_mono line 282
44. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.success_le_geometric line 299

    Source documentation

    The repeated-game bound is the explicitly supplied premise conditional. The premise averaged is the separate law-of-total-probability obligation.

    theorem success_le_geometric
        (p a success : Rat) (n : Nat) (conditionalSuccess : Nat → Rat)
        (hp : 0 ≤ p) (hp' : p ≤ 1)
        (conditional : ∀ k, conditionalSuccess k ≤ a ^ k)
        (averaged : success ≤ bernoulliAverage p n conditionalSuccess) :
        success ≤ (1 - p * (1 - a)) ^ n := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.bernoulliAverage

45. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.pow_mono_nonneg line 310
46. def OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.zeroProbability line 324

    Source documentation

    A uniformly sampled vector in a d-dimensional binary space is zero with probability 2^(-d). The counting justification is a separate obligation.

    def zeroProbability (d : Nat) : Rat := (1 / 2 : Rat) ^ d

47. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.zeroProbability_nonneg line 326
48. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.zeroProbability_le_one line 329
49. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.zeroProbability_antitone line 337
50. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.geometric_le_dimension_bound line 357

    Source documentation

    The last inequality in (6.25), including the sign obligations.

    theorem geometric_le_dimension_bound (d L n : Nat) (hd : d ≤ L)
        (a : Rat) (ha : 0 ≤ a) (ha' : a ≤ 1) :
        (1 - zeroProbability d * (1 - a)) ^ n ≤
          (1 - zeroProbability L * (1 - a)) ^ n := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.zeroProbability

51. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.projection_upper_bound line 374

    Source documentation

    Lemma 6.8's numerical conclusion, conditional on the repeated-game and averaging premises. In particular these hypotheses must be proved for the same augmented strategy, including its fixed advice.

    theorem projection_upper_bound
        (d L n : Nat) (hd : d ≤ L) (a success : Rat)
        (ha : 0 ≤ a) (ha' : a ≤ 1) (conditionalSuccess : Nat → Rat)
        (conditional : ∀ k, conditionalSuccess k ≤ a ^ k)
        (averaged : success ≤ bernoulliAverage (zeroProbability d) n conditionalSuccess) :
        success ≤ (1 - zeroProbability L * (1 - a)) ^ n := by
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.bernoulliAverage, OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.zeroProbability

52. def OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.decoderThreshold line 385
53. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.decoderThreshold_pos line 387
54. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.exists_pos_nat_gt line 397

    Source documentation

    An elementary Archimedean bound for rational parameters.

    theorem exists_pos_nat_gt (x : Rat) : ∃ n : Nat, 0 < n ∧ x < (n : Rat) := by
    …

55. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.power_mul_growth_le_one line 407

    Source documentation

    The estimate b^n ≤ 1 / (1+n(1-b)) without division.

    theorem power_mul_growth_le_one (b : Rat) (hb : 0 ≤ b) (hb' : b ≤ 1)
        (n : Nat) : b ^ n * (1 + (n : Rat) * (1 - b)) ≤ 1 := by
    …

56. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.exists_power_lt line 425

    Source documentation

    Positive powers of a rational base below one eventually fall below every positive rational threshold; this supplies the search target in (4.4).

    theorem exists_power_lt (b threshold : Rat) (hb : 0 ≤ b) (hb' : b < 1)
        (ht : 0 < threshold) : ∃ n : Nat, 0 < n ∧ b ^ n < threshold := by
    …

57. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.zeroProbability_pos line 442
58. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.exists_repetition_length line 445
59. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.soundness_of_bounds line 462

    Source documentation

    Proposition 6.9's contradiction, with its dependency boundary visible. extraction is the entire lower-bound implication; upper must bound every strategy of the same type, with all allowed advice; gap is (4.4).

    theorem soundness_of_bounds
        {Labeling Strategy : Type} (acceptance : Labeling → Rat)
        (success : Strategy → Rat) (delta lower upperBound : Rat)
        (extraction : ∀ labeling, delta < acceptance labeling →
          ∃ strategy, lower ≤ success strategy)
        (upper : ∀ strategy, success strategy ≤ upperBound)
        (gap : upperBound < lower) :
        ∀ labeling, acceptance labeling ≤ delta := by
    …

60. theorem OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.soundness_from_repetition line 480

    Source documentation

    Proposition 6.9 specialized to (6.25) and (4.4). Every occurrence of strategy is the same object, so fixed advice cannot silently change between the lower and upper bounds.

    theorem soundness_from_repetition
        {Labeling Strategy : Type} (acceptance : Labeling → Rat)
        (success : Strategy → Rat) (dimension : Strategy → Nat)
        (conditionalSuccess : Strategy → Nat → Rat)
        (delta a theta : Rat) (q L t : Nat) (ha : 0 ≤ a) (ha' : a ≤ 1)
        (dimension_le : ∀ strategy, dimension strategy ≤ L)
        (conditional : ∀ strategy k, conditionalSuccess strategy k ≤ a ^ k)
        (averaged : ∀ strategy, success strategy ≤
          bernoulliAverage (zeroProbability (dimension strategy)) t
            (conditionalSuccess strategy))
        (extraction : ∀ labeling, delta < acceptance labeling →
          ∃ strategy, decoderThreshold theta q ≤ success strategy)
    …

    Mentions: OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.bernoulliAverage, OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.zeroProbability, OAI.UniqueGamesTheorem.Soundness.RepetitionUpper.decoderThreshold