MixingOperators.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.KervaireMixing.Slot line 26
Source documentation
A slot is a disk number, a disk kind, and a position in the cyclic word.
```
abbrev Slot (I K : Type*) := (K ⊕ K) × I
```
def OAI.KervaireMixing.successor line 29
Source documentation
The opposite cyclic orders on positive and negative word disks.
```
def successor (ρ : Equiv.Perm I) : Equiv.Perm (Slot I K) where
…
```
Mentions: OAI.KervaireMixing.Slot

def OAI.KervaireMixing.labels line 40

Source documentation

Coefficient inverses for the signed incidence operator.

def labels (ρ : Equiv.Perm I) (a : I → A) : Slot I K → A
  | (Sum.inl _, i) => (a i)⁻¹
  | (Sum.inr _, i) => a (ρ.symm i)

/-- The scalar mixing involution; no group coefficients occur in it. -/

Mentions: OAI.KervaireMixing.Slot

def OAI.KervaireMixing.mixingMatrix line 45
Source documentation
The scalar mixing involution; no group coefficients occur in it.
```
def mixingMatrix (X : Matrix K K ℂ) : Matrix (Slot I K) (Slot I K) ℂ :=
…
```
Mentions: OAI.KervaireMixing.Slot
theorem OAI.KervaireMixing.mixingMatrix_star line 49
theorem OAI.KervaireMixing.mixingMatrix_sq line 55
theorem OAI.KervaireMixing.mixingMatrix_unitary line 65
def OAI.KervaireMixing.S line 71
Source documentation
The coefficient shift S and scalar mixer J in the actual regular Hilbert space.
```
def S (ρ : Equiv.Perm I) (a : I → A) : Operator (Slot I K) A :=
…
```
Mentions: OAI.KervaireMixing.Slot
def OAI.KervaireMixing.J line 73
theorem OAI.KervaireMixing.S_unitary line 76
theorem OAI.KervaireMixing.J_sq line 79
theorem OAI.KervaireMixing.J_star line 86
theorem OAI.KervaireMixing.J_unitary line 91
theorem OAI.KervaireMixing.S_commutant line 97
theorem OAI.KervaireMixing.J_commutant line 99
theorem OAI.KervaireMixing.scalarTensor_delta line 103
theorem OAI.KervaireMixing.trace_SJ line 110
Source documentation
The mixed shift exchanges disk kinds, so its unnormalized trace is zero.
```
theorem trace_SJ (ρ : Equiv.Perm I) (a : I → A) (X : Matrix K K ℂ) :
    KervaireMatrix.trace (S ρ a * J (I := I) X) = 0 := by
…
```
Mentions: OAI.KervaireMatrix.trace, OAI.KervaireMixing.S, OAI.KervaireMixing.J
theorem OAI.KervaireMixing.star_SJ line 120
Source documentation
The exact corner reversal makes SJ self-adjoint for every mixer X.
```
theorem star_SJ (ρ : Equiv.Perm I) (a : I → A) (X : Matrix K K ℂ) :
    star (S ρ a * J (I := I) X) = S ρ a * J (I := I) X := by
…
```
Mentions: OAI.KervaireMixing.S, OAI.KervaireMixing.J

theorem OAI.KervaireMixing.phase_SJ line 145

Source documentation

The exact phase identity at arbitrary group coefficients.

theorem phase_SJ [Nonempty I] [Nonempty K]
    (ρ : Equiv.Perm I) (a : I → A) (X : Matrix.unitaryGroup K ℂ) :
    let _ := isStarNormal_of_mem_unitary
…

lemma OAI.KervaireCycle.perm_pow_embedding line 166
lemma OAI.KervaireCycle.orbitWeight_embedding line 172
lemma OAI.KervaireMatrix.weightedShift_moment line 184
lemma OAI.KervaireMatrix.vectorPhase_cycle_embedding line 190

lemma OAI.KervaireMatrix.phase_cycles line 205

Source documentation

Exact cyclewise decomposition of boundary phase; all circuit words are in A.

lemma phase_cycles {Z : Type*} [Fintype Z] (n : Z → ℕ)
    (e : (Σ z, Fin (n z+1)) ≃ D) (σ : Equiv.Perm D)
    (he : ∀ z i, σ (e ⟨z,i⟩) = e ⟨z,finRotate (n z+1) i⟩)
    (u : D → ℂ) (a : D → A) (hu : ∀ i, u i ∈ unitary ℂ) :
    let _ := isStarNormal_of_mem_unitary (weightedShift_unitary σ u a hu)
…

Mentions: OAI.KervaireMatrix.weightedShift_unitary

lemma OAI.KervaireRegular.groupPhase_one line 237
lemma OAI.KervaireRegular.groupPhase_rotation_one line 260

lemma OAI.KervaireRegular.trivial_of_boundary_inequalities line 270

Source documentation

The final right-cut limiting argument in the planar component theorem.

lemma trivial_of_boundary_inequalities {Z : Type*} [Fintype Z] [Nonempty Z]
    (z₀ : Z) (c : Z → A)
    (h : ∀ ε : ℝ, 0 < ε → ε < 1 →
      groupPhase (scalarRotation (((Fintype.card Z : ℝ)-1)*ε)) (scalarRotation_unitary _) (c z₀)
        + ((Fintype.card Z : ℝ)-1)*(1-ε) ≤ (Fintype.card Z : ℝ)-1) :
    c z₀ = 1 := by
…

Mentions: OAI.KervaireRegular.groupPhase

lemma OAI.KervaireCycle.orbitWeight_eq_prod line 308
lemma OAI.KervaireCycle.orbitWeight_rotate_prod line 314
lemma OAI.KervaireCycle.orbitWeight_scalarRotation line 322

lemma OAI.KervaireBoundary.divergence_cycle line 337

Source documentation

Summation over the fibers of the explicit boundary-cycle decomposition.

lemma divergence_cycle (n : Z → ℕ) (e : (Σ z, Fin (n z+1)) ≃ D) (γ : D → ℝ) (z : Z) :
    (∑ d, if (e.symm d).1 = z then γ d else 0) = ∑ i, γ (e ⟨z,i⟩) := by
…

lemma OAI.KervaireBoundary.total_cycle_length line 342

lemma OAI.KervaireBoundary.phase_boundary_cycles line 351

Source documentation

Cycle phase specializes to prescribed real boundary fluxes.

lemma phase_boundary_cycles (n : Z → ℕ) (e : (Σ z, Fin (n z+1)) ≃ D)
    (σ : Equiv.Perm D) (he : ∀ z i, σ (e ⟨z,i⟩) = e ⟨z,finRotate (n z+1) i⟩)
    (γ : D → ℝ) (a : D → A) (η : Z → ℝ)
    (hη : ∀ z, (∑ d, if (e.symm d).1 = z then γ d else 0) = η z) :
    let _ := isStarNormal_of_mem_unitary (weightedShift_unitary σ (fun d ↦ scalarRotation (γ d)) a
…