RestrictionTransport.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Exact transport of nested affine restrictions

The nested quotient-domain/range inclusion has exactly the effective annihilator and target obtained by comap and map. Its parameterization is linearly equivalent to the direct effective restriction, independently of any Fourier frequency. Thus normalized second moments and the outer average of their squares agree while retaining the full affine translate.

def OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.nestedEmbedding line 33

Source documentation

Compose the two actual quotient-domain and target-subspace embeddings.

def nestedEmbedding (A : Submodule F2 E) (B : Submodule F2 F)
    (C : Submodule F2 (E ⧸ A)) (D : Submodule F2 B) :
    Parameter C D →ₗ[F2] (E →ₗ[F2] F) :=
…

theorem OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.nestedEmbedding_injective line 38

theorem OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.exists_nested_embed_iff line 47

Source documentation

Exact effective annihilator and target of a nested restriction.

theorem exists_nested_embed_iff (A : Submodule F2 E) (B : Submodule F2 F)
    (C : Submodule F2 (E ⧸ A)) (D : Submodule F2 B) (M : E →ₗ[F2] F) :
    (∃ N : Parameter C D, nestedEmbedding A B C D N = M) ↔
      C.comap A.mkQ ≤ M.ker ∧ M.range ≤ D.map B.subtype := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.nestedEmbedding

theorem OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.nested_range_eq line 99
Source documentation
Nested and effective direct restrictions describe exactly the same perturbations.
```
theorem nested_range_eq (A : Submodule F2 E) (B : Submodule F2 F)
    (C : Submodule F2 (E ⧸ A)) (D : Submodule F2 B) :
    (nestedEmbedding A B C D).range =
      (embedding (C.comap A.mkQ) (D.map B.subtype)).range := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.nestedEmbedding
theorem OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.exists_range_preimage line 116
def OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.sameRangeEquiv line 120
Source documentation
The actual linear change of parameters between two injective presentations.
```
def sameRangeEquiv (f : P →ₗ[K] G) (g : Q →ₗ[K] G)
    (hf : Function.Injective f) (hg : Function.Injective g)
    (h : f.range = g.range) : P ≃ₗ[K] Q := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.sameRangeEquiv_commutes line 150

theorem OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.expect_eq_of_same_range line 159

Source documentation

Injective parameter changes preserve normalized uniform expectations.

theorem expect_eq_of_same_range (f : P →ₗ[K] G) (g : Q →ₗ[K] G)
    (hf : Function.Injective f) (hg : Function.Injective g)
    (h : f.range = g.range) (observable : G → ℝ) :
    (𝔼 x, observable (f x)) = 𝔼 y, observable (g y) := by
…

theorem OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.restriction_secondMoment_eq_of_same_range line 167

Source documentation

Preserve second moments at the same full ambient translate.

theorem restriction_secondMoment_eq_of_same_range
    (f : P →ₗ[K] G) (g : Q →ₗ[K] G)
    (hf : Function.Injective f) (hg : Function.Injective g)
    (h : f.range = g.range) (observable : G → ℝ) (T : G) :
    (𝔼 x, observable (T + f x) ^ 2) = 𝔼 y, observable (T + g y) ^ 2 :=
…

theorem OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.restriction_energySquare_average_eq_of_same_range line 175

Source documentation

Preserve the outer mean of squared restriction energies, with the square outside.

theorem restriction_energySquare_average_eq_of_same_range [Fintype G]
    (f : P →ₗ[K] G) (g : Q →ₗ[K] G)
    (hf : Function.Injective f) (hg : Function.Injective g)
    (h : f.range = g.range) (observable : G → ℝ) :
    (𝔼 T, (𝔼 x, observable (T + f x) ^ 2) ^ 2) =
      𝔼 T, (𝔼 y, observable (T + g y) ^ 2) ^ 2 := by
…

theorem OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.nested_restriction_secondMoment_eq line 193

Source documentation

The genuine nested affine restriction has the effective direct second moment.

theorem nested_restriction_secondMoment_eq
    (A : Submodule F2 E) (B : Submodule F2 F)
    (C : Submodule F2 (E ⧸ A)) (D : Submodule F2 B)
    (h : (E →ₗ[F2] F) → ℝ) (T : E →ₗ[F2] F) :
    (𝔼 N : Parameter C D, h (T + nestedEmbedding A B C D N) ^ 2) =
      𝔼 M : Parameter (C.comap A.mkQ) (D.map B.subtype),
        h (T + embed (C.comap A.mkQ) (D.map B.subtype) M) ^ 2 := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.nestedEmbedding

theorem OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.nested_restriction_energySquare_average_eq line 210

Source documentation

Squared normalized energies also agree before averaging over the full translate.

theorem nested_restriction_energySquare_average_eq [Fintype (E →ₗ[F2] F)]
    (A : Submodule F2 E) (B : Submodule F2 F)
    (C : Submodule F2 (E ⧸ A)) (D : Submodule F2 B)
    (h : (E →ₗ[F2] F) → ℝ) :
    (𝔼 T, (𝔼 N, h (T + nestedEmbedding A B C D N) ^ 2) ^ 2) =
      𝔼 T, (𝔼 M, h (T + embed (C.comap A.mkQ) (D.map B.subtype) M) ^ 2) ^ 2 := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.RestrictionTransport.nestedEmbedding

theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a5_preimage_eq_ker line 228
Source documentation
A subspace disjoint from the image has exactly the original kernel as preimage.
```
theorem a5_preimage_eq_ker (X : W →ₗ[K] V) (A₀ : Submodule K V)
    (hd : Disjoint A₀ (LinearMap.range X)) : A₀.comap X = LinearMap.ker X := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a5_range_domRestrict_eq_of_cover line 240
Source documentation
Restricting to a subspace that covers the domain modulo the kernel preserves the image.
```
theorem a5_range_domRestrict_eq_of_cover (X : W →ₗ[K] V) (B₀ : Submodule K W)
    (hc : B₀ ⊔ LinearMap.ker X = ⊤) :
    LinearMap.range (X.domRestrict B₀) = LinearMap.range X := by
…
```

theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a5_effective_annihilator line 252

Source documentation

The A.5 compressed image pulls back to its exact effective annihilator.

theorem a5_effective_annihilator (X : W →ₗ[K] V)
    (A₀ A : Submodule K V) (B₀ : Submodule K W)
    (hA : A₀ ⊔ LinearMap.range X = A)
    (hc : B₀ ⊔ LinearMap.ker X = ⊤) :
    (LinearMap.range (compress X A₀ B₀)).comap A₀.mkQ = A := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress

theorem OAI.UniqueGamesTheorem.Appendix.LinearIdentities.a5_effective_codomain line 261

Source documentation

The A.5 compressed kernel maps to its exact effective codomain.

theorem a5_effective_codomain (X : W →ₗ[K] V)
    (A₀ : Submodule K V) (B B₀ : Submodule K W)
    (hd : Disjoint A₀ (LinearMap.range X))
    (hB : B₀ ⊓ LinearMap.ker X = B) :
    (LinearMap.ker (compress X A₀ B₀)).map B₀.subtype = B := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.LinearIdentities.compress