OAI/RepresentationTheory/FiniteUnitary/Reconstruction.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RowColumn.UnitaryFrame.positive_functional_bound line 14
2. theorem OAI.RowColumn.UnitaryFrame.reconstruction_bound line 29

   Source documentation

   Finite-dimensional unitary reconstruction with polynomial Fourier cost. Only the actual operator norm of B occurs; the auxiliary Hilbert norm is used solely to construct the frame and does not alter that norm.

   theorem reconstruction_bound (τ : A →ₗ[ℂ] ℂ) (core : InnerProductSpace.Core ℂ A)
       (hinner : ∀ x y, core.inner x y = τ (star x*y))
       (u : G →* unitary A)
       (hspan : Submodule.span ℂ (Set.range fun g : G => (u g : A)) = ⊤)
       (B : A) (ℓ : A →ₗ[ℂ] ℂ) (R : ℝ) (_ : 0 ≤ R)
       (hU : ∀ g, ‖ℓ (u g : A)‖ ≤ R) :
       ‖ℓ B‖ ≤ 4 * (Module.finrank ℂ A : ℝ) * ‖B‖ * R := by
   …

3. theorem OAI.RowColumn.FiniteStarAlgebra.complementary_central_projection line 71

   Source documentation

   A finite-dimensional two-sided star ideal has a central orthogonal unit. The two inner-product identities hold for the actual Hilbert–Schmidt trace. This constructs the central support used in the occupied-board filter.

   theorem complementary_central_projection (core : InnerProductSpace.Core ℂ A) (K : Submodule ℂ A)
       (hL : ∀ a x, x ∈ K → a*x ∈ K) (hR : ∀ a x, x ∈ K → x*a ∈ K)
       (hstar : ∀ x, x ∈ K → star x ∈ K)
       (hadjL : ∀ a x y : A, core.inner (a*x) y = core.inner x (star a*y))
       (hadjR : ∀ a x y : A, core.inner (x*a) y = core.inner x (y*star a)) :
       ∃ q : A, star q = q ∧ q*q = q ∧ (∀ a, q*a = a*q) ∧
         1-q ∈ K ∧ (∀ x, x ∈ K → q*x = 0 ∧ x*q = 0) := by
   …

4. abbrev OAI.RowColumn.FiniteStarAlgebra.Ambient line 135
5. def OAI.RowColumn.FiniteStarAlgebra.algebraToEnd line 137
6. lemma OAI.RowColumn.FiniteStarAlgebra.algebraToEnd_injective line 142
7. def OAI.RowColumn.FiniteStarAlgebra.algebraCore line 151
8. def OAI.RowColumn.FiniteStarAlgebra.physicalTrace line 159
9. lemma OAI.RowColumn.FiniteStarAlgebra.core_inner_trace line 162
10. lemma OAI.RowColumn.FiniteStarAlgebra.physicalTrace_mul_comm line 169
11. def OAI.RowColumn.FiniteStarAlgebra.restrictHom line 175

    Source documentation

    Restriction to a subspace preserved by the whole star algebra is a genuine star homomorphism (both the subspace and its orthogonal complement are reducing).

    def restrictHom (A : StarSubalgebra ℂ (Ambient (E := E))) (F : Submodule ℂ E)
    …

    Mentions: OAI.RowColumn.FiniteStarAlgebra.Ambient

12. theorem OAI.RowColumn.FiniteStarAlgebra.exists_central_support line 195

    Source documentation

    Central support of a reducing physical subspace. Its algebraic kernel is removed, so no other unsupported sector can inflate the Fourier norm.

    theorem exists_central_support (A : StarSubalgebra ℂ (Ambient (E := E))) (F : Submodule ℂ E)
    …

    Mentions: OAI.RowColumn.FiniteStarAlgebra.Ambient

13. def OAI.RowColumn.FiniteStarAlgebra.supportedAlgebra line 223
14. lemma OAI.RowColumn.FiniteStarAlgebra.supportedAlgebra_closed line 236
15. theorem OAI.RowColumn.FiniteStarAlgebra.norm_supported_eq line 243

    Source documentation

    Removing the kernel by its central support makes restriction isometric. This avoids choosing irreducible compact-group carriers or using unproved Schur--Weyl decompositions.

    theorem norm_supported_eq (φ : A →⋆ₐ[ℂ] B) (q : A) (hs : star q = q)
        (hqq : q*q=q) (hc : ∀ a, q*a=a*q) (hq : φ q=1)
        (hkill : ∀ a, φ a=0 → q*a=0) (a : A) : ‖q*a‖ = ‖φ a‖ := by
    …

16. def OAI.RowColumn.Isotypic.carrier line 274
17. lemma OAI.RowColumn.Isotypic.mem_carrier line 278
18. lemma OAI.RowColumn.Isotypic.projection_intertwines line 281
19. theorem OAI.RowColumn.Isotypic.eigenspace_finrank line 302

    Source documentation

    On an isotypic unitary representation, every eigenspace of an operator in the group commutant has dimension at least that of the irreducible type.

    theorem eigenspace_finrank [Representation.IsIrreducible ρ]
        (hspan : carrier ρ τ = ⊤)
        (hτ : ∀ g x y, inner ℂ (τ g x) (τ g y) = inner ℂ x y)
        (T : E →ₗ[ℂ] E) (hT : ∀ g x, T (τ g x) = τ g (T x))
        (μ : ℂ) (hμ : Module.End.HasEigenvalue T μ) :
        Module.finrank ℂ V ≤ Module.finrank ℂ (Module.End.eigenspace T μ) := by
    …

    Mentions: OAI.RowColumn.Isotypic.carrier

20. lemma OAI.RowColumn.Isotypic.carrier_invariant line 348
21. lemma OAI.RowColumn.Isotypic.carrier_commutant line 359
22. def OAI.RowColumn.Isotypic.restricted line 372
23. def OAI.RowColumn.Isotypic.restrictIntertwiner line 377
24. lemma OAI.RowColumn.Isotypic.restricted_unitary line 385
25. lemma OAI.RowColumn.Isotypic.restricted_isotypic line 391
26. lemma OAI.RowColumn.SpectralMultiplicity.positive_norm_le_of_eigenvalues line 412
27. theorem OAI.RowColumn.SpectralMultiplicity.norm_le_trace_div line 432

    Source documentation

    An eigenvalue supported on at least d dimensions pays a trace factor d. This is the precise spectral normalization needed for the global filter.

    theorem norm_le_trace_div (T : E →L[ℂ] E) (hT : T.IsPositive) (d : ℕ) (hd : 0 < d)
        (hmult : ∀ μ : ℂ, Module.End.HasEigenvalue T.toLinearMap μ →
          d ≤ Module.finrank ℂ (Module.End.eigenspace T.toLinearMap μ)) :
        ‖T‖ ≤ (LinearMap.trace ℂ E T.toLinearMap).re / d := by
    …

28. lemma OAI.RowColumn.SpectralMultiplicity.trace_compression line 472
29. lemma OAI.RowColumn.SpectralMultiplicity.trace_compression_le line 479
30. lemma OAI.RowColumn.SpectralMultiplicity.restrict_positive line 496
31. lemma OAI.RowColumn.SpectralMultiplicity.trace_restrict_le line 505
32. instance OAI.RowColumn.FiniteStarAlgebra.algebraFiniteDimensional line 535
33. instance OAI.RowColumn.FiniteStarAlgebra.algebraIsClosed line 538
34. lemma OAI.RowColumn.FiniteStarAlgebra.supported_restriction_norm line 541
35. theorem OAI.RowColumn.FiniteStarAlgebra.exists_isotypic_filter line 579

    Source documentation

    The exact dimension normalization of the occupied-board global filter. No highest-weight entropy or Schur--Weyl hypothesis is required: restriction of the supported algebra is faithful, and every eigenspace contains the irreducible carrier.

    theorem exists_isotypic_filter (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
        (τ : Representation ℂ G E)
        (hτ : ∀ g x y, inner ℂ (τ g x) (τ g y) = inner ℂ x y)
        (A : StarSubalgebra ℂ (E →L[ℂ] E))
        (hA : ∀ a : A, ∀ g x, (a : E →L[ℂ] E) (τ g x) = τ g ((a : E →L[ℂ] E) x)) :
        ∃ q : A, star q = q ∧ q*q=q ∧ (∀ a, q*a=a*q) ∧
          (∀ x ∈ Isotypic.carrier ρ τ, (q : E →L[ℂ] E) x = x) ∧
          ∀ a : A, (a : E →L[ℂ] E).IsPositive →
            ‖q*a‖ ≤ (physicalTrace A a).re / Module.finrank ℂ V := by
    …

    Mentions: OAI.RowColumn.Isotypic.carrier, OAI.RowColumn.FiniteStarAlgebra.physicalTrace

36. theorem OAI.RowColumn.UnitaryFrame.reconstruction_hilbert_bound line 625

    Source documentation

    The finite Fourier reconstruction bound for arbitrary Hilbert-valued linear maps, in particular weighted Hilbert–Schmidt sandwich maps.

    theorem reconstruction_hilbert_bound (τ : A →ₗ[ℂ] ℂ) (core : InnerProductSpace.Core ℂ A)
        (hinner : ∀ x y, core.inner x y = τ (star x*y))
        (u : G →* unitary A)
        (hspan : Submodule.span ℂ (Set.range fun g : G => (u g : A)) = ⊤)
        (B : A) (F : A →ₗ[ℂ] E) (R : ℝ) (hR : 0 ≤ R)
        (hU : ∀ g, ‖F (u g : A)‖ ≤ R) :
        ‖F B‖ ≤ 4 * (Module.finrank ℂ A : ℝ) * ‖B‖ * R := by
    …

37. lemma OAI.RowColumn.supported_fourth line 653
38. theorem OAI.RowColumn.filterNorm_sq line 663

    Source documentation

    The quarter-root estimate at the level of the genuine operator norm. The two fourth-moment bounds imply the exact squared sandwich bound.

    theorem filterNorm_sq (q F G : A) (hsq : IsSelfAdjoint q) (hqq : q*q=q)
        (hF : IsSelfAdjoint F) (hG : IsSelfAdjoint G) (hcF : Commute q F) (hcG : Commute q G)
        (d : ℝ) (_ : 0 < d) (hFb : ‖q * F^4‖ ≤ 1/d) (hGb : ‖q * G^4‖ ≤ 1/d) :
        ‖F*q*G‖^2 ≤ 1/d := by
    …