OAI/Computability/UniqueGames/Analysis/A5FrequencyTransportLemmas.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Appendix.A5FrequencyTransport.quotient_relativeFrequency_apply line 26
2. theorem OAI.UniqueGamesTheorem.Appendix.A5FrequencyTransport.quotient_compress_apply line 38
3. theorem OAI.UniqueGamesTheorem.Appendix.A5FrequencyTransport.compression_eq_relativeFrequency_of_pointwise line 47

   Source documentation

   The relative compression equation follows from the concrete map to the direct quotient on each element of the retained subspace.

   theorem compression_eq_relativeFrequency_of_pointwise
       (A A' : Submodule F2 V) (B' B : Submodule F2 W)
       (hA : A ≤ A') (hB : B' ≤ B)
       (X : B →ₗ[F2] (V ⧸ A)) (Y : B' →ₗ[F2] (V ⧸ A'))
       (hY : ∀ b : B', Submodule.mapQ A A' LinearMap.id hA
         (X ⟨b.val, hB b.property⟩) = Y b) :
       compress X (A'.map A.mkQ) (B'.comap B.subtype) =
         A5ReverseIndex.relativeFrequency A A' B' B hA hB Y := by
   …

   Mentions: OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.relativeFrequency

4. theorem OAI.UniqueGamesTheorem.Appendix.A5FrequencyTransport.quotientFactor_mapQ line 64
5. theorem OAI.UniqueGamesTheorem.Appendix.A5FrequencyTransport.dualFactor_quotient line 74
6. theorem OAI.UniqueGamesTheorem.Appendix.A5FrequencyTransport.outputFactor_symm_as_inclusion line 85
7. theorem OAI.UniqueGamesTheorem.Appendix.A5FrequencyTransport.compression_eq_relativeFrequency_dualFactor line 97

   Source documentation

   The naturally transported local compression belongs to the precise relative-frequency fiber used in A5ReverseIndex.Ancestor.

   theorem compression_eq_relativeFrequency_dualFactor
       (A : Submodule F2 V) (B : Submodule F2 W)
       (C : Submodule F2 (V ⧸ A)) (D : Submodule F2 B)
       (hA : A ≤ C.comap A.mkQ) (hB : D.map B.subtype ≤ B)
       (X : B →ₗ[F2] (V ⧸ A)) :
       compress X ((C.comap A.mkQ).map A.mkQ) ((D.map B.subtype).comap B.subtype) =
         A5ReverseIndex.relativeFrequency A (C.comap A.mkQ) (D.map B.subtype) B hA hB
           (dualFactor A B C D (compress X C D)) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.relativeFrequency

8. theorem OAI.UniqueGamesTheorem.Appendix.A5FrequencyTransport.isAntecedent_relativeFrequency_dualFactor line 116

   Source documentation

   Package the actual naturally transported label into its counted antecedent fiber, retaining the original map as the witness.

   theorem isAntecedent_relativeFrequency_dualFactor
       (A : Submodule F2 V) (B : Submodule F2 W)
       (C : Submodule F2 (V ⧸ A)) (D : Submodule F2 B)
       (hA : A ≤ C.comap A.mkQ) (hB : D.map B.subtype ≤ B)
       (X : B →ₗ[F2] (V ⧸ A))
       (hdis : Disjoint X.range C) (hcover : D ⊔ X.ker = ⊤) :
       AntecedentCount.IsAntecedent ((D.map B.subtype).comap B.subtype)
         ((C.comap A.mkQ).map A.mkQ)
         (A5ReverseIndex.relativeFrequency A (C.comap A.mkQ) (D.map B.subtype) B hA hB
           (dualFactor A B C D (compress X C D))) X := by
   …

   Mentions: OAI.UniqueGamesTheorem.Appendix.AntecedentCount.IsAntecedent, OAI.UniqueGamesTheorem.Appendix.A5ReverseIndex.relativeFrequency

9. abbrev OAI.UniqueGamesTheorem.Appendix.A5Passage.OuterIndex line 149
10. def OAI.UniqueGamesTheorem.Appendix.A5Passage.LiftedA line 152
11. def OAI.UniqueGamesTheorem.Appendix.A5Passage.LiftedB line 155
12. abbrev OAI.UniqueGamesTheorem.Appendix.A5Passage.Pair line 158
13. abbrev OAI.UniqueGamesTheorem.Appendix.A5Passage.Passage line 161
14. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.comap_mkQ_injective line 164
15. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.map_subtype_injective line 173
16. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.outer_eq_of_lifted line 194
17. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.recover_liftedA line 199
18. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.recover_liftedB line 202
19. def OAI.UniqueGamesTheorem.Appendix.A5Passage.forget line 205
20. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.forget_injective line 208
21. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.forget_val line 228
22. instance OAI.UniqueGamesTheorem.Appendix.A5Passage.pairFintype line 233
23. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.dim_pairA line 245
24. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.codim_pairB line 256
25. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.pair_order line 270
26. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.pair_order_le line 277
27. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.pair_rank line 284
28. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.descendant_rank line 292
29. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.effective_order_rank line 301
30. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.effective_order_rank_le line 314
31. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.effective_order_rank_pos line 330
32. def OAI.UniqueGamesTheorem.Appendix.A5Passage.descendantSum line 341
33. theorem OAI.UniqueGamesTheorem.Appendix.A5Passage.descendantSum_nonneg line 350
34. abbrev OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.Index line 370
35. def OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.descendant line 374
36. def OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.sourceI line 380
37. def OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.sourceJ line 383
38. def OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.targetRank line 386
39. theorem OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.descendant_rank line 391
40. theorem OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.original_size line 397
41. theorem OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.original_order_bounds line 404
42. theorem OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.descendant_size_le line 411
43. theorem OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.earlierA_le line 418
44. theorem OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.earlierB_le line 427
45. abbrev OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.Fiber line 432
46. def OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.encode line 437

    Source documentation

    The encoder keeps the actual earlier pair and actual earlier map.

    def encode (d : ℕ) (r : A13Index.Triple (E := E) (F := F)) (i j : ℕ)
    …

    Mentions: OAI.UniqueGamesTheorem.Appendix.A13Index.Triple

47. def OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.earlierTriple line 448
48. theorem OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.earlierTriple_encode line 455
49. theorem OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.encode_injective line 466

    Source documentation

    Fixing the result and retained earlier data fixes both the complementary pair and its outer hybrid index. No additional outer-index factor occurs.

    theorem encode_injective (d : ℕ)
        (r : A13Index.Triple (E := E) (F := F)) (i j : ℕ) :
    …

    Mentions: OAI.UniqueGamesTheorem.Appendix.A13Index.Triple

50. theorem OAI.UniqueGamesTheorem.Appendix.A5ForwardIndex.card_fiber_le line 496

    Source documentation

    Actual cardinality bound for every fiber used by the weighted reversal.

    theorem card_fiber_le (d : ℕ) (r : A13Index.Triple (E := E) (F := F)) (i j : ℕ) :
    …

    Mentions: OAI.UniqueGamesTheorem.Appendix.A13Index.Triple

51. def OAI.UniqueGamesTheorem.Appendix.A5ReverseSum.actualMoment line 547
52. def OAI.UniqueGamesTheorem.Appendix.A5ReverseSum.targetWeight line 551
53. theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseSum.targetWeight_nonneg line 556
54. theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseSum.targetWeight_descendant line 563
55. theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseSum.sum_triples_cutoff line 575

    Source documentation

    The target cutoff is exactly the actual finite hybrid index.

    theorem sum_triples_cutoff (d : ℕ)
        (H : ∀ (A : Submodule F2 E) (B : Submodule F2 F),
          (B →ₗ[F2] (E ⧸ A)) → ℝ) :
        (∑ r : A13Index.Triple (E := E) (F := F),
    …

    Mentions: OAI.UniqueGamesTheorem.Appendix.A13Index.Triple

56. theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseSum.target_sum_eq line 606
57. theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseSum.source_summand_eq line 637
58. theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseSum.source_sum_eq line 647
59. theorem OAI.UniqueGamesTheorem.Appendix.A5ReverseSum.weighted_descendantSum_le line 668

    Source documentation

    The weighted sum of actual A.5 descendants is bounded by damped actual map-derivative moments over all hybrid restrictions of order at most d.

    theorem weighted_descendantSum_le (d : ℕ) (hd : 1 ≤ d)
        (f : (E →ₗ[F2] F) → ℝ) :
        (∑ r : A13Index.BoundedPositiveTriple (E := E) (F := F) d,
    …

    Mentions: OAI.UniqueGamesTheorem.Appendix.A13Index.BoundedPositiveTriple

60. def OAI.UniqueGamesTheorem.Appendix.A5Induction.BoundAtDegree line 708

    Source documentation

    The strong-induction motive quantifies over the actual changing domains. Quotients and subspaces preserve the fixed universe levels.

    def BoundAtDegree (d : ℕ) : Prop :=
    …

61. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.damping_le line 718
62. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.coefficient_absorption line 736
63. def OAI.UniqueGamesTheorem.Appendix.A5Induction.dampedMapMoment line 774

    Source documentation

    The actual weighted map-derivative sum left by the finite reindexing.

    def dampedMapMoment (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) : ℝ :=
    …

64. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.dampedMapMoment_le line 779
65. def OAI.UniqueGamesTheorem.Appendix.A5Induction.dampedHybridMoment line 805
66. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.dampedHybridMoment_le line 809
67. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.hybridProjector_zero_pair line 828
68. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.energy_sq_le_hybridMomentSum line 834
69. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.degree_zero_bound line 869
70. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.recurrence_closure line 876

    Source documentation

    Close the actual recurrence once its finite index expansion is supplied. This lemma states that recurrence explicitly; it is not the public A.5 theorem.

    theorem recurrence_closure (d : ℕ) (hd : 1 ≤ d)
        (f : (E →ₗ[F2] F) → ℝ) (hf : DegreeAtMost d f)
        (hrec : (𝔼 M, f M ^ 4) / 162 ≤
          (2 : ℝ) ^ (6 * d * d) * (𝔼 M, f M ^ 2)^2 +
            (2 : ℝ) ^ (100 * d * d) * dampedHybridMoment d f) :
        (𝔼 M, f M ^ 4) ≤ (2 : ℝ) ^ (100 * d * d) * hybridMomentSum d f := by
    …

    Mentions: OAI.UniqueGamesTheorem.Appendix.A5Induction.dampedHybridMoment

71. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.lifted_outer_dimensions line 912

    Source documentation

    Dimension bounds for the outer subspaces used by the actual A.5 operator identity, obtained from the order of an actual derivative-space index.

    theorem lifted_outer_dimensions (X : F →ₗ[F2] E)
        (C : Submodule F2 (E ⧸ X.range)) (D : Submodule F2 X.ker)
        (d : ℕ) (hcut : Module.finrank F2 X.range + order C D ≤ d) :
        Module.finrank F2 (C.comap X.range.mkQ) ≤ d ∧
          Module.finrank F2 (F ⧸ D.map X.ker.subtype) ≤ d := by
    …

72. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.a5_energySquare_le_power line 928

    Source documentation

    The native A.5 energy inequality with its actually proved numerical complement factor. The only cutoff is the rank plus the outer derivative order.

    theorem a5_energySquare_le_power (X : F →ₗ[F2] E)
        (C : Submodule F2 (E ⧸ X.range)) (D : Submodule F2 X.ker)
        [Fintype (OperatorPartitions.A5GeometricIndex X
          (C.comap X.range.mkQ) (D.map X.ker.subtype))]
        (d : ℕ) (hcut : Module.finrank F2 X.range + order C D ≤ d)
        (f : (E →ₗ[F2] F) → ℝ) (S : Parameter X.range X.ker) :
        (𝔼 N, hybridDerivative C D S (mapDerivative X f) N ^ 2) ^ 2 ≤
          (2 : ℝ) ^ (6 * d * Module.finrank F2 X.range) *
            ∑ p : OperatorPartitions.A5GeometricIndex X
              (C.comap X.range.mkQ) (D.map X.ker.subtype),
              (𝔼 N, mapDerivative (LinearIdentities.compress X p.val.1 p.val.2)
                (hybridDerivative p.val.1 p.val.2 (embed X.range X.ker S) f) N ^ 2)^2 := by
    …

    Mentions: OAI.UniqueGamesTheorem.Appendix.OperatorPartitions.A5GeometricIndex, OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress

73. def OAI.UniqueGamesTheorem.Appendix.A5Induction.postA5Sum line 994

    Source documentation

    Actual A.5 descendants before recombining the first hybrid restriction.

    def postA5Sum (X : F →ₗ[F2] E) (e : ℕ) (f : (E →ₗ[F2] F) → ℝ) : ℝ :=
    …

74. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.mapDerivative_hybridMomentSum_le line 999
75. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.postA5Sum_hybrid_average line 1026

    Source documentation

    Recombination uses the natural domain and codomain isomorphisms. The intermediate shifts need only be the actual embedded derivative parameters.

    theorem postA5Sum_hybrid_average (A : Submodule F2 E) (B : Submodule F2 F)
        (X : B →ₗ[F2] (E ⧸ A)) (e : ℕ) (f : (E →ₗ[F2] F) → ℝ) :
        (𝔼 T, postA5Sum X e (hybridDerivative A B T f)) =
          A5Passage.descendantSum A B X e f := by
    …

    Mentions: OAI.UniqueGamesTheorem.Appendix.A5Induction.postA5Sum, OAI.UniqueGamesTheorem.Appendix.A5Passage.descendantSum

76. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.a15_of_strong_induction line 1046

    Source documentation

    The actual A.15 induction step for one positive-order derivative triple. The induction hypothesis is used only at the strictly smaller degree d-t, on its genuine quotient-domain and kernel-codomain spaces.

    theorem a15_of_strong_induction (d t : ℕ) (A : Submodule F2 E)
        (B : Submodule F2 F) (X : B →ₗ[F2] (E ⧸ A))
        (ht : t = order A B + Module.finrank F2 X.range)
        (htpos : 0 < t) (htd : t ≤ d)
        (ih : ∀ e, e < d → BoundAtDegree.{u, v} e)
        (f : (E →ₗ[F2] F) → ℝ) (hf : DegreeAtMost d f) :
        (𝔼 T, 𝔼 N, mapDerivative X (hybridDerivative A B T f) N ^ 4) ≤
          (2 : ℝ) ^ (100 * (d - t) * (d - t) + 6 * d * Module.finrank F2 X.range) *
            A5Passage.descendantSum A B X (d - t) f := by
    …

    Mentions: OAI.UniqueGamesTheorem.Appendix.A5Passage.descendantSum

77. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.boundedTripleSum_le_descendants line 1084

    Source documentation

    Apply the genuine lower-degree induction step to every term of the checked A.13 sum, preserving its original positive-order cutoff.

    theorem boundedTripleSum_le_descendants (d : ℕ)
        (ih : ∀ e, e < d → BoundAtDegree.{u, v} e)
        (f : (E →ₗ[F2] F) → ℝ) (hf : DegreeAtMost d f) :
        A13Reduction.boundedPositiveTripleSum d f ≤
          ∑ p : A13Index.BoundedPositiveTriple (E := E) (F := F) d,
    …

    Mentions: OAI.UniqueGamesTheorem.Appendix.A13Reduction.boundedPositiveTripleSum, OAI.UniqueGamesTheorem.Appendix.A13Index.BoundedPositiveTriple

78. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.boundAtDegree line 1121

    Source documentation

    Proposition A.5 on every finite-dimensional binary linear-map space, proved by strong induction with all changing domains in the motive.

    theorem boundAtDegree (d : ℕ) : BoundAtDegree.{u, v} d := by
    …

79. theorem OAI.UniqueGamesTheorem.Appendix.A5Induction.derivative_inequality line 1145