OAI/RepresentationTheory/FiniteUnitary/Uncertainty.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CubeShuffle.PermutationHilbert.H line 10

   Also declared: ComparatorChallenges/OccupiedOverlap.lean:130 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:130 (same declaration text).

2. def OAI.CubeShuffle.PermutationHilbert.act line 12
3. lemma OAI.CubeShuffle.PermutationHilbert.act_apply line 15
4. lemma OAI.CubeShuffle.PermutationHilbert.act_single line 18
5. lemma OAI.CubeShuffle.PermutationHilbert.trace_projection line 22
6. lemma OAI.CubeShuffle.PermutationHilbert.projection_diagonal line 35
7. lemma OAI.CubeShuffle.PermutationHilbert.projection_comm line 48
8. lemma OAI.CubeShuffle.PermutationHilbert.uniform_diagonal line 57

   Source documentation

   A transitive invariant subspace has constant diagonal orthogonal projection.

   lemma uniform_diagonal (W : Submodule ℂ (H X))
       (htrans : ∀ x y : X, ∃ p : Equiv.Perm X, p x = y ∧
         W.map (act p).toLinearEquiv.toLinearMap = W) (x : X) :
       (Fintype.card X:ℝ) * ‖W.starProjection (EuclideanSpace.single x (1:ℂ))‖^2 =
         Module.finrank ℂ W := by
   …

   Mentions: OAI.CubeShuffle.PermutationHilbert.H, OAI.CubeShuffle.PermutationHilbert.act

9. theorem OAI.CubeShuffle.PermutationHilbert.uncertainty line 75

   Source documentation

   The uncertainty bound, with no assumption of irreducibility.

   theorem uncertainty (W : Submodule ℂ (H X))
       (htrans : ∀ x y : X, ∃ p : Equiv.Perm X, p x = y ∧
         W.map (act p).toLinearEquiv.toLinearMap = W)
       (v : H X) (hv : v ∈ W) (x : X) :
       (Fintype.card X:ℝ) * ‖v x‖^2 ≤ (Module.finrank ℂ W:ℝ) * ‖v‖^2 := by
   …

   Mentions: OAI.CubeShuffle.PermutationHilbert.H, OAI.CubeShuffle.PermutationHilbert.act

10. lemma OAI.CubeShuffle.PermutationHilbert.trace_projection_real line 102
11. theorem OAI.CubeShuffle.PermutationHilbert.footprint_dimension line 111

    Source documentation

    A coordinate footprint fixed by a subgroup supplies an unconditional lower bound on invariant multiplicity. This is the trace form of the branching estimate, valid for every transitive invariant submodule.

    theorem footprint_dimension (W K : Submodule ℂ (H X)) (hKW : K ≤ W)
        (htrans : ∀ x y : X, ∃ p : Equiv.Perm X, p x = y ∧
          W.map (act p).toLinearEquiv.toLinearMap = W)
        (S : Finset X) (hS : ∀ x ∈ S, W.starProjection (EuclideanSpace.single x (1:ℂ)) ∈ K) :
        (S.card:ℝ) * (Module.finrank ℂ W:ℝ) ≤
          (Fintype.card X:ℝ) * (Module.finrank ℂ K:ℝ) := by
    …

    Mentions: OAI.CubeShuffle.PermutationHilbert.H, OAI.CubeShuffle.PermutationHilbert.act