Chart.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.CoordinateSweeps.PlacementInduction.Chart line 17
Source comment
A transitive action with actual chosen representatives. For the application, Ω is the set of ordered placements; the fiber group fixes the base placement.
```
structure Chart (a : G →* Equiv.Perm Ω) where
…
```
Mentions: OAI.CoordinateSweeps.a
def OAI.CoordinateSweeps.PlacementInduction.Chart.stabilizer line 25
def OAI.CoordinateSweeps.PlacementInduction.Chart.cocycle line 40
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.cocycle_mul line 47
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.cocycle_one line 56
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.cocycle_inv line 62
def OAI.CoordinateSweeps.PlacementInduction.Chart.matrix line 71
Source comment
Literal placement-by-fiber block matrix of the induced unitary action.
```
def matrix (g : G) : Matrix (Ω × Fin ρ.dimension) (Ω × Fin ρ.dimension) ℂ :=
…
```
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.matrix_mul line 75
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.matrix_one line 96
def OAI.CoordinateSweeps.PlacementInduction.Chart.action line 103
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.matrix_inv line 109
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.matrix_unitary line 126
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.trace_matrix line 130
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.invrep_reaches line 147
def OAI.CoordinateSweeps.PlacementInduction.Chart.decompose line 152
Source comment
Actual orbit--stabilizer decomposition, including its fiber cardinal factor.
```
def decompose : G ≃ Ω × C.stabilizer where
…
```
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.card_group line 172
def OAI.CoordinateSweeps.PlacementInduction.Chart.fixedEquiv line 175
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.cocycle_fixed line 192
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.fixed_character_sum line 207
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.induced_character_sum line 222

theorem OAI.CoordinateSweeps.PlacementInduction.Chart.multiplicity_eq line 237

Source comment

Finite Frobenius reciprocity for the literal placement matrices. The RHS is the actual Hom space in restriction, not an assumed branching coefficient.

theorem multiplicity_eq (ρ : UnitaryIrrep C.stabilizer) (τ : UnitaryIrrep G) :
    Module.finrank ℂ (τ.asRepresentation.IntertwiningMap (matrixRepresentation (C.action ρ)))=
      Module.finrank ℂ (ρ.asRepresentation.IntertwiningMap
        (matrixRepresentation (τ.matrix.comp C.stabilizer.subtype))) := by
…

Mentions: OAI.CoordinateSweeps.UnitaryIrrep

theorem OAI.CoordinateSweeps.PlacementInduction.Chart.induced_moment_bound line 260

Source comment

The induced moment really dominates each target moment by its branching multiplicity.

theorem induced_moment_bound (ρ : UnitaryIrrep C.stabilizer) (τ : UnitaryIrrep G)
    {W : Type*} [Fintype W] (w : W → ℂ) (g : W → G) (q : ℕ) :
    (Module.finrank ℂ (ρ.asRepresentation.IntertwiningMap
      (matrixRepresentation (τ.matrix.comp C.stabilizer.subtype))) : ℝ)*
        (Matrix.trace (((averageMatrix τ.matrix w g).conjTranspose*averageMatrix τ.matrix w g)^q)).re ≤
          (Matrix.trace (((averageMatrix (C.action ρ) w g).conjTranspose*averageMatrix (C.action ρ) w g)^q)).re := by
…

Mentions: OAI.CoordinateSweeps.UnitaryIrrep

def OAI.CoordinateSweeps.OrderedPlacements.action line 274
lemma OAI.CoordinateSweeps.OrderedPlacements.action_apply line 284
def OAI.CoordinateSweeps.OrderedPlacements.rangeEquiv line 286
lemma OAI.CoordinateSweeps.OrderedPlacements.rangeEquiv_apply line 290
def OAI.CoordinateSweeps.OrderedPlacements.chart line 299
Source comment
Every ordered placement is reached by an actual permutation extending the bijection on its marked positions. No cardinal or transitivity axiom is used.
```
def chart (x0 : I ↪ X) : PlacementInduction.Chart (action (I := I) (X := X)) where
…
```
Mentions: OAI.CoordinateSweeps.PlacementInduction.Chart, OAI.CoordinateSweeps.OrderedPlacements.action
lemma OAI.CoordinateSweeps.OrderedPlacements.mem_stabilizer_iff line 308
lemma OAI.CoordinateSweeps.OrderedPlacements.card_placements line 319
def OAI.CoordinateSweeps.PlacementInduction.Chart.transition line 329
def OAI.CoordinateSweeps.PlacementInduction.Chart.conditionalBlock line 332
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.transition_nonneg line 338
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.transition_columns line 347
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.transition_rows line 354
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.weight_le_transition line 364
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.zero_transition_sum line 372
theorem OAI.CoordinateSweeps.PlacementInduction.Chart.average_block line 387
def OAI.CoordinateSweeps.PlacementInduction.Chart.pointFix line 412
def OAI.CoordinateSweeps.PlacementInduction.Chart.pointEquiv line 421
def OAI.CoordinateSweeps.PlacementInduction.Chart.pointIrrep line 430
Source comment
The remaining symmetric-group type transported to the actual input placement.
```
def pointIrrep (ρ : UnitaryIrrep C.stabilizer) (x : Ω) : UnitaryIrrep (C.pointFix x) where
…
```
Mentions: OAI.CoordinateSweeps.UnitaryIrrep
def OAI.CoordinateSweeps.PlacementInduction.Chart.transitionResidual line 441
lemma OAI.CoordinateSweeps.PlacementInduction.Chart.cocycle_residual line 447
def OAI.CoordinateSweeps.PlacementInduction.Chart.transitionAverage line 457
Source comment
Normalized residual law on the true point stabilizer. The reference is any compatible transition; it is a unitary frame, not a new hypothesis on the law.
```
def transitionAverage (ρ : UnitaryIrrep C.stabilizer) (w : W → ℝ) (g : W → G)
    (x y : Ω) (ω₀ : W) (h₀ : y=a (g ω₀) x) : Matrix (Fin ρ.dimension) (Fin ρ.dimension) ℂ :=
…
```
Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.a
theorem OAI.CoordinateSweeps.PlacementInduction.Chart.conditionalBlock_eq line 465