GraphOrbitSelection.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Actual orbit samples retaining the rescaled graph signal

The finite matrix moment estimate and the Hilbert sign selection are combined here. The signal is the image of the graph vector under the specified bounded operator; its invariance is derived from the common unitary graph action.

def OAI.KadisonKastler.rescaledGraphOperatorMap line 25
Source documentation
The graph formula is linear on all ambient operators.
```
def rescaledGraphOperatorMap (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ) :
    (H →L[ℂ] H) →ₗ[ℂ] TomitaGraphHilbert H where
…
```
Mentions: OAI.KadisonKastler.TomitaGraphHilbert

def OAI.KadisonKastler.rescaledGraphSignalMap line 41

Source documentation

The actual graph signal, viewed as a real-linear map for sign sums.

def rescaledGraphSignalMap (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) :
    (H →L[ℂ] H) →ₗ[ℝ] TomitaGraphHilbert H :=
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert

theorem OAI.KadisonKastler.rescaledGraphSignalMap_apply line 46

theorem OAI.KadisonKastler.norm_graphSignal_unitaryDoubleOrbit line 53

Source documentation

Commutation with the unitary graph action preserves the signal on an actual two-sided orbit.

theorem norm_graphSignal_unitaryDoubleOrbit
    (M : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (Ω : H) (c : ℝ) (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H)
    (u v : unitary (H →L[ℂ] H))
    (hvright : conjugationOperator J (v : H →L[ℂ] H) ∈ M.commutant)
    (huright : conjugationOperator J (u : H →L[ℂ] H) ∈ M.commutant)
    (hvΩ : conjugationOperator J (v : H →L[ℂ] H) Ω = star (v : H →L[ℂ] H) Ω)
    (huΩ : conjugationOperator J (u : H →L[ℂ] H) Ω = star (u : H →L[ℂ] H) Ω)
    (hT : T * (rescaledGraphAction J hJ u (star v) :
        TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) =
      (rescaledGraphAction J hJ u (star v) :
        TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) * T)
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.rescaledGraphAction

theorem OAI.KadisonKastler.graphProjectionDefect_commutes line 84
Source documentation
The defect between two graph projections commutes with every common graph unitary that commutes with the two projections.
```
theorem graphProjectionDefect_commutes
    (P Q A : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H)
    (hP : P * A = A * P) (hQ : Q * A = A * Q) :
    ((1 - Q) * P) * A = A * ((1 - Q) * P) := by
…
```
Mentions: OAI.KadisonKastler.TomitaGraphHilbert

theorem OAI.KadisonKastler.rescaledGraphProjectionDefect_commutes line 97

Source documentation

In a common prepared position, the actual graph defect has the required common matrix-orbit invariance.

theorem rescaledGraphProjectionDefect_commutes
    (M N : VonNeumannAlgebra H) (R : StarSubalgebra ℂ (H →L[ℂ] H))
    (hRM : R ≤ M.toStarSubalgebra) (hRN : R ≤ N.toStarSubalgebra)
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J) (Ω : H) (c : ℝ)
    (hMcomm : ∀ a ∈ R, conjugationOperator J (star a) ∈ M.commutant)
    (hNcomm : ∀ a ∈ R, conjugationOperator J (star a) ∈ N.commutant)
    (hvector : ∀ a ∈ R, conjugationOperator J (star a) Ω = a Ω)
    (u v : unitary (H →L[ℂ] H))
    (hu : (u : H →L[ℂ] H) ∈ R) (hv : (v : H →L[ℂ] H) ∈ R) :
    ((1 - rescaledGraphProjection N J Ω c) * rescaledGraphProjection M J Ω c) *
        (rescaledGraphAction J hJ u v : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) =
      (rescaledGraphAction J hJ u v : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) *
…

Mentions: OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.rescaledGraphProjection, OAI.KadisonKastler.rescaledGraphAction, OAI.KadisonKastler.TomitaGraphHilbert

theorem OAI.KadisonKastler.exists_matrixOrbit_signal_and_cost line 130

Source documentation

The matrix cost construction and a constant orbit signal select one actual sampled operator, rather than a separate sample for each bound.

theorem exists_matrixOrbit_signal_and_cost
    {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    {k : ℝ} (hk : 1 ≤ k) (hxnorm : ‖x Ω‖ ^ 2 + k * ‖star x Ω‖ ^ 2 = 1)
    (L : (H →L[ℂ] H) →ₗ[ℝ] V) {s : ℝ} (hs : 0 < s)
    (hsignal : ∀ j g, ‖L (matrixOrbitSample (E j) x g)‖ ^ 2 = s) :
    ∃ j m, ∃ ω : Fin m → MatrixOrbitIndex (d j), ∃ ε : Fin m → Bool,
      1 ≤ m ∧
      s / 2 ≤ ‖L (normalizedFiniteSignSum
        (fun i => matrixOrbitSample (E j) x (ω i)) ε)‖ ^ 2 ∧
      graphMomentCost Ω k (normalizedFiniteSignSum
        (fun i => matrixOrbitSample (E j) x (ω i)) ε) ≤ 240 := by
…

Mentions: OAI.KadisonKastler.matrixOrbitSample, OAI.KadisonKastler.MatrixOrbitIndex, OAI.KadisonKastler.normalizedFiniteSignSum, OAI.KadisonKastler.graphMomentCost

theorem OAI.KadisonKastler.exists_rescaledGraph_orbit_signal_and_cost line 150

Source documentation

The genuine common graph action discharges the signal-invariance premise in the simultaneous selection theorem.

theorem exists_rescaledGraph_orbit_signal_and_cost
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    {k : ℝ} (hk : 1 ≤ k) (hxnorm : ‖x Ω‖ ^ 2 + k * ‖star x Ω‖ ^ 2 = 1)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H)
    (hs : 0 < ‖T (rescaledGraphVector J Ω (Real.sqrt k) x)‖)
    (hcomm : ∀ j a, a ∈ (E j).algebra → conjugationOperator J (star a) ∈ M.commutant)
    (hvector : ∀ j a, a ∈ (E j).algebra → conjugationOperator J (star a) Ω = a Ω)
    (hT : ∀ j (u v : unitary (H →L[ℂ] H)), (u : H →L[ℂ] H) ∈ (E j).algebra →
      (v : H →L[ℂ] H) ∈ (E j).algebra →
      T * (rescaledGraphAction J hJ u v : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) =
        (rescaledGraphAction J hJ u v : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) * T) :
    ∃ j m, ∃ ω : Fin m → MatrixOrbitIndex (d j), ∃ ε : Fin m → Bool,
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.rescaledGraphAction, OAI.KadisonKastler.MatrixOrbitIndex