Occurrence.lean`

63 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CoordinateSweeps.Placement.DependsOn line 30
Source comment
Dependence only on the listed coordinate values of a placement.
```
def DependsOn (coords : Y → I → U) (A : Finset I) (f : Y → ℂ) : Prop :=
…
```
def OAI.CoordinateSweeps.Placement.topSpace line 35
Source comment
Counting-measure top-level space. Equivalently the orthogonal complement of the span of proper-coordinate cylinder functions (conjugation preserves that span).
```
def topSpace (coords : Y → I → U) : Submodule ℂ (Y → ℂ) where
…
```
def OAI.CoordinateSweeps.Placement.alternatingKernel line 49
Source comment
The source's s-normalized alternating kernel, over all coordinate subsets.
```
def alternatingKernel (s : ℝ) (p : Finset I → X → Y → ℝ) : Matrix X Y ℂ :=
…
```
theorem OAI.CoordinateSweeps.Placement.alternatingKernel_mulVec_top line 56
theorem OAI.CoordinateSweeps.Placement.matrix_l2_norm_le_hs line 77
Source comment
Counting HS norm always dominates the L2 operator norm, rectangular and empty dimensions included. No entrywise max norm is used.
```
theorem matrix_l2_norm_le_hs (A : Matrix X Y ℂ) :
    ‖A‖ ≤ Real.sqrt (∑ x, ∑ y, ‖A x y‖^2) := by
…
```
theorem OAI.CoordinateSweeps.Placement.fullKernel_top_norm_le line 103
theorem OAI.CoordinateSweeps.UnitaryIrrep.adjoint_intertwines line 118

theorem OAI.CoordinateSweeps.UnitaryIrrep.intertwiner_gram_scalar line 138

Source comment

Schur's lemma makes every nonzero intertwiner a scalar coisometry.

theorem intertwiner_gram_scalar {X : Type*} [Fintype X] [DecidableEq X]
    (P : Γ →* Matrix X X ℂ) (hP : ∀ g, (P g).conjTranspose * P g = 1)
    (B : Matrix (Fin ρ.dimension) X ℂ)
    (hB : ∀ g, B * P g = ρ.matrix g * B) :
    ∃ c : ℂ, B * B.conjTranspose = c • (1 : Matrix _ _ ℂ) := by
…

Mentions: OAI.CoordinateSweeps.c

theorem OAI.CoordinateSweeps.UnitaryIrrep.norm_le_compression line 150

Source comment

Exact norm transfer, with no extraneous dimension loss. Q need agree with an averaged permutation operator only on the adjoint intertwiner range.

theorem norm_le_compression {X : Type*} [Fintype X] [DecidableEq X]
    (P : Γ →* Matrix X X ℂ) (hP : ∀ g, (P g).conjTranspose * P g = 1)
    (B : Matrix (Fin ρ.dimension) X ℂ) (hne : B ≠ 0)
    (hB : ∀ g, B * P g = ρ.matrix g * B)
    (K : Matrix (Fin ρ.dimension) (Fin ρ.dimension) ℂ) (Q : Matrix X X ℂ)
    (hQ : Q * B.conjTranspose = B.conjTranspose * K) : ‖K‖ ≤ ‖Q‖ := by
…

def OAI.CoordinateSweeps.fixTwo line 183
Source comment
The pointwise stabilizer of two sites, used in the sparse dimension bridge.
```
def fixTwo {Ω : Type*} (a b : Ω) : Subgroup (Equiv.Perm Ω) where
…
```
Mentions: OAI.CoordinateSweeps.a

theorem OAI.CoordinateSweeps.SparseDimension.commuting_scalar line 200

Source comment

Generic Schur commutant lemma, with no classification assumptions.

theorem commuting_scalar {Γ : Type*} [Group Γ]
    (ρ : Representation ℂ Γ V) [ρ.IsIrreducible]
    (A : Module.End ℂ V) (hA : ∀ g, A * ρ g = ρ g * A) :
    ∃ c : ℂ, A = c • (1 : Module.End ℂ V) := by
…

Mentions: OAI.CoordinateSweeps.c

theorem OAI.CoordinateSweeps.SparseDimension.finrank_eq_one_of_scalars line 215
theorem OAI.CoordinateSweeps.SparseDimension.subrep_bot_toSubmodule line 245
theorem OAI.CoordinateSweeps.SparseDimension.subrep_top_toSubmodule line 248

def OAI.CoordinateSweeps.SparseDimension.nested line 252

Source comment

Flatten a subrepresentation of a subrepresentation without changing its dimension.

def nested {Γ : Type*} [Group Γ] {ρ : Representation ℂ Γ V}
    (S : Subrepresentation ρ) (T : Subrepresentation S.toRepresentation) : Subrepresentation ρ where
…

theorem OAI.CoordinateSweeps.SparseDimension.exists_minimal_constituent line 261

Source comment

Existence of a least-dimensional constituent, proved rather than assumed.

theorem exists_minimal_constituent {Γ : Type*} [Group Γ]
    (ρ : Representation ℂ Γ V) [Nontrivial V] :
    ∃ S : Subrepresentation ρ, 0 < Module.finrank ℂ S.toSubmodule ∧
      S.toRepresentation.IsIrreducible ∧
      ∀ T : Subrepresentation ρ, T ≠ ⊥ →
        Module.finrank ℂ S.toSubmodule ≤ Module.finrank ℂ T.toSubmodule := by
…

theorem OAI.CoordinateSweeps.SparseDimension.exists_constituent_le_half line 308

Source comment

Every reducible finite-group representation has a constituent of at most half its dimension. This uses Maschke over ℂ, not an assumed decomposition.

theorem exists_constituent_le_half {Γ : Type*} [Group Γ] [Fintype Γ]
    (ρ : Representation ℂ Γ V) [Nontrivial V]
    (hn : ¬ρ.IsIrreducible) :
    ∃ S : Subrepresentation ρ, 0 < Module.finrank ℂ S.toSubmodule ∧
      S.toRepresentation.IsIrreducible ∧
      2 * Module.finrank ℂ S.toSubmodule ≤ Module.finrank ℂ V := by
…

theorem OAI.CoordinateSweeps.SparseDimension.finrank_eq_one_of_fixTwo_irreducible line 351
Source comment
Restriction to permutations fixing two distinct sites is not irreducible, unless the full irreducible is one-dimensional. This gives a factor-two dimension descent every two removed cards, needed for sparse types.
```
theorem finrank_eq_one_of_fixTwo_irreducible
    (ρ : Representation ℂ (Equiv.Perm Ω) V) [ρ.IsIrreducible]
    (a b : Ω) (hab : a ≠ b)
    [hirr : Representation.IsIrreducible (ρ.comp (fixTwo a b).subtype)] :
    Module.finrank ℂ V = 1 := by
…
```
Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.fixTwo
theorem OAI.CoordinateSweeps.SparseDimension.irreducible_comp_surjective line 378
def OAI.CoordinateSweeps.SparseDimension.fixTwoHom line 405
Source comment
Permutations of the complementary sites, viewed in the two-point stabilizer.
```
def fixTwoHom (a b : Ω) : Equiv.Perm {x : Ω // x ≠ a ∧ x ≠ b} →* fixTwo a b where
…
```
Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.fixTwo
theorem OAI.CoordinateSweeps.SparseDimension.fixTwoHom_val line 413
theorem OAI.CoordinateSweeps.SparseDimension.fixTwoHom_surjective line 417

theorem OAI.CoordinateSweeps.SparseDimension.exists_half_constituent_fixTwo line 434

Source comment

One factor-two dimension descent, with the remaining symmetric group realized literally as permutations of the complement.

theorem exists_half_constituent_fixTwo
    (ρ : Representation ℂ (Equiv.Perm Ω) V) [ρ.IsIrreducible] [Nontrivial V]
    (hd : Module.finrank ℂ V ≠ 1) (a b : Ω) (hab : a ≠ b) :
    ∃ S : Subrepresentation (ρ.comp (fixTwo a b).subtype),
      0 < Module.finrank ℂ S.toSubmodule ∧
      Representation.IsIrreducible (S.toRepresentation.comp (fixTwoHom a b)) ∧
      2 * Module.finrank ℂ S.toSubmodule ≤ Module.finrank ℂ V := by
…

Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.fixTwo, OAI.CoordinateSweeps.SparseDimension.fixTwoHom

theorem OAI.CoordinateSweeps.SparseDimension.irreducible_nontrivial line 453

theorem OAI.CoordinateSweeps.SparseDimension.sparse_line_by_dim line 463

Source comment

A one-dimensional constituent is already visible after at most twice the base-two logarithm of the dimension many fixed cards. The power formulation avoids rounding conventions and is valid also for dimension one.

theorem sparse_line_by_dim (D : ℕ) :
    ∀ (Ω : Type u) [Fintype Ω] [DecidableEq Ω]
      (V : Type v) [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
      (ρ : Representation ℂ (Equiv.Perm Ω) V) [ρ.IsIrreducible],
      Module.finrank ℂ V = D →
      ∃ (t : ℕ) (A : Finset Ω) (W : Submodule ℂ V),
        Module.finrank ℂ W = 1 ∧ A.card ≤ 2*t ∧ 2^t ≤ D ∧
        ∀ g : Equiv.Perm Ω, (∀ a ∈ A, g a = a) →
          ∀ w ∈ W, ρ g w ∈ W := by
…

Mentions: OAI.CoordinateSweeps.a

theorem OAI.CoordinateSweeps.SparseDimension.exists_sparse_line line 531

Source comment

The rounded-free quantitative sparse dimension bridge for the actual symmetric group, independent of a partition classification.

theorem exists_sparse_line
    (ρ : Representation ℂ (Equiv.Perm Ω) V) [ρ.IsIrreducible] :
    ∃ (t : ℕ) (A : Finset Ω) (W : Submodule ℂ V),
      Module.finrank ℂ W = 1 ∧ A.card ≤ 2*t ∧ 2^t ≤ Module.finrank ℂ V ∧
      ∀ g : Equiv.Perm Ω, (∀ a ∈ A, g a = a) →
        ∀ w ∈ W, ρ g w ∈ W :=
…

Mentions: OAI.CoordinateSweeps.a

def OAI.CoordinateSweeps.SparseDimension.signScalar line 540
Source comment
Ordinary permutation sign, embedded into the complex scalars.
```
def signScalar : Equiv.Perm Ω →* ℂ :=
…
```
theorem OAI.CoordinateSweeps.SparseDimension.signScalar_apply line 543
theorem OAI.CoordinateSweeps.SparseDimension.signScalar_swap line 546
theorem OAI.CoordinateSweeps.SparseDimension.oneDimensional_trivial_or_sign line 552
Source comment
Every one-dimensional representation of a finite symmetric group is literally the trivial or sign representation. This also handles Ω of size 0,1.
```
theorem oneDimensional_trivial_or_sign
    (ρ : Representation ℂ (Equiv.Perm Ω) V) (hd : Module.finrank ℂ V = 1) :
    (∀ g, ρ g = 1) ∨ (∀ g, ρ g = signScalar g • (1 : Module.End ℂ V)) := by
…
```
Mentions: OAI.CoordinateSweeps.SparseDimension.signScalar
theorem OAI.CoordinateSweeps.SparseDimension.orbit_span_top line 596

theorem OAI.CoordinateSweeps.SparseDimension.dimension_le_pow_of_stable_line line 623

Source comment

The upper sparse dimension bound: a line invariant under the stabilizer of k named sites gives at most n^k dimensions in its irreducible orbit.

theorem dimension_le_pow_of_stable_line
    (ρ : Representation ℂ (Equiv.Perm Ω) V) [ρ.IsIrreducible]
    (A : Finset Ω) (W : Submodule ℂ V) (hW : Module.finrank ℂ W = 1)
    (hstable : ∀ g : Equiv.Perm Ω, (∀ a ∈ A, g a = a) → ∀ w ∈ W, ρ g w ∈ W) :
    Module.finrank ℂ V ≤ (Fintype.card Ω)^A.card := by
…

Mentions: OAI.CoordinateSweeps.a

def OAI.CoordinateSweeps.SparseDimension.fixSet line 666
Source comment
Pointwise stabilizer of a named finite set of sites.
```
def fixSet (A : Finset Ω) : Subgroup (Equiv.Perm Ω) where
…
```
def OAI.CoordinateSweeps.SparseDimension.fixSetHom line 675
Source comment
The complementary symmetric group onto the pointwise stabilizer.
```
def fixSetHom (A : Finset Ω) : Equiv.Perm {x : Ω // x ∉ A} →* fixSet A where
…
```
Mentions: OAI.CoordinateSweeps.SparseDimension.fixSet
theorem OAI.CoordinateSweeps.SparseDimension.fixSetHom_val line 682
theorem OAI.CoordinateSweeps.SparseDimension.fixSetHom_surjective line 686

theorem OAI.CoordinateSweeps.SparseDimension.stable_line_trivial_or_sign line 705

Source comment

A stable line under a pointwise stabilizer is a literal trivial or sign line. There is no hypothesis about a partition or a pre-existing embedding.

theorem stable_line_trivial_or_sign
    (ρ : Representation ℂ (Equiv.Perm Ω) V)
    (A : Finset Ω) (W : Submodule ℂ V) (hW : Module.finrank ℂ W = 1)
    (hstable : ∀ g : Equiv.Perm Ω, (∀ a ∈ A, g a = a) → ∀ w ∈ W, ρ g w ∈ W) :
    ∃ u : V, u ≠ 0 ∧
      ((∀ g : Equiv.Perm Ω, (∀ a ∈ A, g a = a) → ρ g u = u) ∨
       (∀ g : Equiv.Perm Ω, (∀ a ∈ A, g a = a) → ρ g u = signScalar g • u)) := by
…

Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.SparseDimension.signScalar

theorem OAI.CoordinateSweeps.SparseDimension.exists_minimal_sparse_line line 739

Source comment

Minimal signed placement level with both dimension bounds. The last clause rules out every earlier line, hence in particular every earlier fixed vector of either the representation or its sign twist.

theorem exists_minimal_sparse_line
    (ρ : Representation ℂ (Equiv.Perm Ω) V) [ρ.IsIrreducible] :
    ∃ (k t : ℕ) (A : Finset Ω) (u : V),
      A.card = k ∧ k ≤ 2*t ∧ 2^t ≤ Module.finrank ℂ V ∧
      Module.finrank ℂ V ≤ (Fintype.card Ω)^k ∧ u ≠ 0 ∧
      ((∀ g : Equiv.Perm Ω, (∀ a ∈ A, g a = a) → ρ g u = u) ∨
       (∀ g : Equiv.Perm Ω, (∀ a ∈ A, g a = a) → ρ g u = signScalar g • u)) ∧
      ∀ B : Finset Ω, B.card < k → ∀ (v : V),
        (∀ g : Equiv.Perm Ω, (∀ a ∈ B, g a = a) → ∃ c : ℂ, ρ g v = c • v) → v = 0 := by
…

Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.SparseDimension.signScalar, OAI.CoordinateSweeps.c

def OAI.CoordinateSweeps.PlacementOccurrence.orbitSynthesis line 782
Source comment
Sum of orbit vectors against placement coordinates. The repeated stabilizer fibers are left in the sum, so no transversal choice is needed.
```
def orbitSynthesis (ρ : Representation ℂ Γ V) (u : V) (x₀ : X) : (X → ℂ) →ₗ[ℂ] V where
…
```
theorem OAI.CoordinateSweeps.PlacementOccurrence.orbitSynthesis_covariant line 789
theorem OAI.CoordinateSweeps.PlacementOccurrence.orbitSynthesis_delta_ne_zero line 799
theorem OAI.CoordinateSweeps.PlacementOccurrence.orbitSynthesis_surjective line 825
theorem OAI.CoordinateSweeps.PlacementOccurrence.subgroup_sum_fixed line 849
theorem OAI.CoordinateSweeps.PlacementOccurrence.orbitSynthesis_subgroup_average line 857
theorem OAI.CoordinateSweeps.PlacementOccurrence.orbitSynthesis_eq_zero_of_no_fixed line 875
theorem OAI.CoordinateSweeps.SparseDimension.signScalar_mul_self line 893
def OAI.CoordinateSweeps.SparseDimension.signTwist line 899
Source comment
Tensoring with the ordinary sign character, on exactly the same space.
```
def signTwist (ρ : Representation ℂ (Equiv.Perm Ω) V) :
    Representation ℂ (Equiv.Perm Ω) V where
…
```
theorem OAI.CoordinateSweeps.SparseDimension.signTwist_apply line 905
def OAI.CoordinateSweeps.SparseDimension.untwistSubrep line 909
Source comment
The same invariant subspaces for ρ and its sign twist.
```
def untwistSubrep (ρ : Representation ℂ (Equiv.Perm Ω) V)
    (S : Subrepresentation (signTwist ρ)) : Subrepresentation ρ where
…
```
Mentions: OAI.CoordinateSweeps.SparseDimension.signTwist
instance OAI.CoordinateSweeps.SparseDimension.signTwist_irreducible line 917
theorem OAI.CoordinateSweeps.SparseDimension.exists_minimal_fixed_vector line 934
Source comment
Either the original representation or its sign twist has a first placement level k with both quantitative dimension bounds and no earlier fixed vector.
```
theorem exists_minimal_fixed_vector [FiniteDimensional ℂ V]
    (ρ : Representation ℂ (Equiv.Perm Ω) V) [ρ.IsIrreducible] :
    ∃ (ε : Bool) (k t : ℕ) (A : Finset Ω) (u : V),
      let τ := if ε then signTwist ρ else ρ
…
```
Mentions: OAI.CoordinateSweeps.SparseDimension.signTwist

theorem OAI.CoordinateSweeps.PlacementOccurrence.synthesis_kills_proper_coordinates line 968

Source comment

Stabilizer of the small placement coordinates really is the pointwise stabilizer of their image, so the exact earlier-level hypothesis applies.

theorem synthesis_kills_proper_coordinates
    (ρ : Representation ℂ (Equiv.Perm Ω) V) (u : V) (x₀ : I ↪ Ω)
    (hnof : ∀ B : Finset Ω, B.card < Fintype.card I → ∀ v : V,
      (∀ g : Equiv.Perm Ω, (∀ a ∈ B, g a = a) → ρ g v = v) → v = 0)
    (A : Finset I) (hA : A ≠ Finset.univ) (f : (I ↪ Ω) → ℂ)
    (hf : ∀ x y : I ↪ Ω, (∀ i ∈ A, x i = y i) → f x = f y) :
    orbitSynthesis ρ u x₀ f = 0 := by
…

Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.PlacementOccurrence.orbitSynthesis

theorem OAI.CoordinateSweeps.Placement.conjTranspose_mulVec_mem_top line 996
theorem OAI.CoordinateSweeps.Placement.alternatingKernel_mul_conjTranspose line 1016
def OAI.CoordinateSweeps.PlacementOccurrence.actionMatrix line 1041
lemma OAI.CoordinateSweeps.PlacementOccurrence.actionMatrix_mulVec line 1045
lemma OAI.CoordinateSweeps.PlacementOccurrence.actionMatrix_unitary line 1052
def OAI.CoordinateSweeps.PlacementOccurrence.synthesisMatrix line 1057
lemma OAI.CoordinateSweeps.PlacementOccurrence.synthesisMatrix_mulVec line 1060
lemma OAI.CoordinateSweeps.PlacementOccurrence.synthesisMatrix_covariant line 1064
lemma OAI.CoordinateSweeps.PlacementOccurrence.synthesisMatrix_ne_zero line 1074
theorem OAI.CoordinateSweeps.PlacementOccurrence.first_level_norm_le line 1091
lemma OAI.CoordinateSweeps.PlacementOccurrence.actionMatrix_entry line 1130