NuclearFiniteness.lean`

60 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.NuclearUltrapower.HilbertUltraproduct.map_one line 20
def OAI.NuclearUltrapower.HilbertUltraproduct.unitalOperatorRep line 29
Source documentation
The Hilbert-ultraproduct operator action is unital, including zero spaces.
```
def unitalOperatorRep : lp (fun i => E i →L[ℂ] E i) ∞ →⋆ₐ[ℂ]
    (HilbertUltraproduct E ω →L[ℂ] HilbertUltraproduct E ω) where
…
```
Mentions: OAI.NuclearUltrapower.HilbertUltraproduct
def OAI.NuclearUltrapower.VariableUltra.sequenceHom line 52
Source documentation
Contractive coordinate homomorphisms preserve boundedness, with no dimension bound.
```
def sequenceHom (f : ∀ i, A i →⋆ₐ[ℂ] C i) : Seq A →⋆ₐ[ℂ] Seq C where
…
```
Mentions: OAI.NuclearUltrapower.VariableUltra.Seq
theorem OAI.NuclearUltrapower.VariableUltra.sequenceHom_apply line 64
theorem OAI.NuclearUltrapower.VariableUltra.coordinateRep_respects line 75
def OAI.NuclearUltrapower.VariableUltra.quotientHilbertRep line 86
Source documentation
Every uniformly varying coordinate representation descends to the quotient.
```
def quotientHilbertRep : Algebra A ω →⋆ₐ[ℂ]
    (HilbertUltraproduct E ω →L[ℂ] HilbertUltraproduct E ω) where
…
```
Mentions: OAI.NuclearUltrapower.VariableUltra.Algebra, OAI.NuclearUltrapower.HilbertUltraproduct
theorem OAI.NuclearUltrapower.VariableUltra.quotientHilbertRep_mk line 95
theorem OAI.NuclearUltrapower.VariableUltra.quotientHilbertRep_commute_left line 98
Source documentation
Coordinatewise commutation survives the quotient and its Hilbert action.
```
theorem quotientHilbertRep_commute_left
    (x : Seq (fun i => E i →L[ℂ] E i)) (q : Algebra A ω)
    (h : ∀ i a, Commute (x i) (f i a)) :
    Commute (HilbertUltraproduct.unitalOperatorRep (E := E) ω x)
…
```
Mentions: OAI.NuclearUltrapower.VariableUltra.Seq, OAI.NuclearUltrapower.VariableUltra.Algebra, OAI.NuclearUltrapower.HilbertUltraproduct.unitalOperatorRep
instance OAI.NuclearUltrapower.tensorHilbertNontrivial line 114
def OAI.NuclearUltrapower.tensorLeftSequence line 136
Source documentation
First tensor factor, represented uniformly at every coordinate.
```
def tensorLeftSequence : B →⋆ₐ[ℂ] VariableUltra.Seq (fun i => TensorHilbert E (F i) →L[ℂ] TensorHilbert E (F i)) where
…
```
Mentions: OAI.NuclearUltrapower.VariableUltra.Seq, OAI.NuclearUltrapower.TensorHilbert
theorem OAI.NuclearUltrapower.tensorLeftSequence_apply line 151
def OAI.NuclearUltrapower.tensorAlpha line 154
theorem OAI.NuclearUltrapower.tensorAlpha_apply line 159
def OAI.NuclearUltrapower.tensorBeta line 163
theorem OAI.NuclearUltrapower.tensorAlphaBeta_commute line 169
Source documentation
The two factor representations commute after taking the Hilbert ultraproduct.
```
theorem tensorAlphaBeta_commute (b : B)
    (q : VariableUltra.Algebra (fun i => F i →L[ℂ] F i) ω) :
    Commute (tensorAlpha (F := F) ρ ω b) (tensorBeta (E := E) ω q) := by
…
```
Mentions: OAI.NuclearUltrapower.VariableUltra.Algebra, OAI.NuclearUltrapower.tensorAlpha, OAI.NuclearUltrapower.tensorBeta
def OAI.NuclearUltrapower.complementPoly line 191
theorem OAI.NuclearUltrapower.map_complementPoly line 194
theorem OAI.NuclearUltrapower.complementEval_poly line 198
def OAI.NuclearUltrapower.finiteQuotientTuple line 212
Source documentation
The actual quotient group tuple from the varying finite-dimensional family.
```
def finiteQuotientTuple : Γ →* unitary (VariableUltra.operatorQuotient (fun i => π i) ω) :=
…
```
Mentions: OAI.NuclearUltrapower.VariableUltra.operatorQuotient
theorem OAI.NuclearUltrapower.tupleRepresentation_finite line 216
def OAI.NuclearUltrapower.rightRepSequence line 222
Source documentation
Coordinate second factors, before passing to either quotient.
```
def rightRepSequence (g : Γ) : VariableUltra.Seq
    (fun i => TensorHilbert E (π i) →L[ℂ] TensorHilbert E (π i)) :=
…
```
Mentions: OAI.NuclearUltrapower.VariableUltra.Seq, OAI.NuclearUltrapower.TensorHilbert
def OAI.NuclearUltrapower.coordinateComplement line 228
Source documentation
The complemented Laplacian as one uniformly bounded operator sequence.
```
def coordinateComplement (S : Finset Γ) (u : Γ → unitary B) : VariableUltra.Seq
    (fun i => TensorHilbert E (π i) →L[ℂ] TensorHilbert E (π i)) :=
…
```
Mentions: OAI.NuclearUltrapower.VariableUltra.Seq, OAI.NuclearUltrapower.TensorHilbert
theorem OAI.NuclearUltrapower.tensorBeta_finiteQuotient line 233
def OAI.NuclearUltrapower.finiteTensorHilbert line 240
Source documentation
Named bundled coordinates keep all tensor/Hilbert instances shared.
```
def finiteTensorHilbert : ComplexHilbert.{v} :=
…
```
def OAI.NuclearUltrapower.finiteTensorAlpha line 243
def OAI.NuclearUltrapower.finiteTensorBeta line 246
def OAI.NuclearUltrapower.finiteTensorAction line 250
theorem OAI.NuclearUltrapower.finiteTensorAlpha_val line 255
theorem OAI.NuclearUltrapower.finiteTensorBeta_val line 259
theorem OAI.NuclearUltrapower.map_coordinateComplement line 263
theorem OAI.NuclearUltrapower.commuting_coordinateComplement line 271
Source documentation
Commuting evaluation is the image of the actual bounded coordinate sequence.
```
theorem commuting_coordinateComplement (S : Finset Γ) (u : Γ → unitary B) :
    commutingEval (finiteTensorHilbert (E := E) π ω)
…
```
Mentions: OAI.NuclearUltrapower.commutingEval, OAI.NuclearUltrapower.finiteTensorHilbert
theorem OAI.NuclearUltrapower.nuclear_coordinate_bound line 281

theorem OAI.NuclearUltrapower.nuclear_no_inequivalent_matches line 308

Source documentation

Quantitative finiteness obstruction: an inequivalent irreducible sequence cannot have a uniformly small spectral minimum for a fixed nuclear tuple.

theorem nuclear_no_inequivalent_matches
    (hB : IsNuclear.{v,v} B) (S : Finset Γ) (κ a : ℝ)
    (hS : S.Nonempty) (hκ0 : 0 < κ) (hκ : κ ≤ 4 * (S.card : ℝ))
    (hgap : HasKazhdanGap.{u,v} S κ) (ha : a < κ ^ 2 / (4 * (S.card : ℝ)))
    (hω : ∀ i : ℕ, ({i} : Set ℕ) ∉ (ω : Filter ℕ))
    (hirr : ∀ i, (π i).Irreducible)
    (hne : Pairwise (fun i j => ¬ (π i).Equivalent (π j)))
    (u : Γ → unitary B)
    (hsmall : ∀ i, 4 * (S.card : ℝ) - a < ‖coordinateComplement ρ π S u i‖) : False := by
…

Mentions: OAI.NuclearUltrapower.coordinateComplement

def OAI.NuclearUltrapower.HilbertUltraproduct.boundedUnitary line 342
Source documentation
A unitary family is uniformly bounded, independently of Hilbert dimension.
```
def boundedUnitary (U : ∀ i, E i ≃ₗᵢ[ℂ] E i) : lp (fun i => E i →L[ℂ] E i) ∞ :=
…
```
theorem OAI.NuclearUltrapower.HilbertUltraproduct.boundedUnitary_apply line 349
def OAI.NuclearUltrapower.HilbertUltraproduct.preUnitary line 353
Source documentation
Coordinate unitaries preserve the ultralimit seminorm.
```
def preUnitary (U : ∀ i, E i ≃ₗᵢ[ℂ] E i) :
    UltraPreHilbert E ω ≃ₗᵢ[ℂ] UltraPreHilbert E ω where
…
```
Mentions: OAI.NuclearUltrapower.UltraPreHilbert
def OAI.NuclearUltrapower.HilbertUltraproduct.unitary line 371
Source documentation
Coordinate unitaries act unitarily on the completed Hilbert ultraproduct.
```
def unitary (U : ∀ i, E i ≃ₗᵢ[ℂ] E i) :
    HilbertUltraproduct E ω ≃ₗᵢ[ℂ] HilbertUltraproduct E ω :=
…
```
Mentions: OAI.NuclearUltrapower.HilbertUltraproduct
theorem OAI.NuclearUltrapower.HilbertUltraproduct.unitary_coe line 378
theorem OAI.NuclearUltrapower.HilbertUltraproduct.unitary_toContinuousLinearMap line 384
Source documentation
Compatibility with the faithful operator realization.
```
theorem unitary_toContinuousLinearMap (U : ∀ i, E i ≃ₗᵢ[ℂ] E i) :
    (unitary ω U : HilbertUltraproduct E ω →L[ℂ] HilbertUltraproduct E ω) =
      map ω (boundedUnitary U) := by
…
```
Mentions: OAI.NuclearUltrapower.HilbertUltraproduct.unitary, OAI.NuclearUltrapower.HilbertUltraproduct, OAI.NuclearUltrapower.HilbertUltraproduct.map, OAI.NuclearUltrapower.HilbertUltraproduct.boundedUnitary
theorem OAI.NuclearUltrapower.HilbertUltraproduct.unitary_one line 392
theorem OAI.NuclearUltrapower.HilbertUltraproduct.unitary_mul line 402
theorem OAI.NuclearUltrapower.HilbertUltraproduct.unitary_eq_of_tendsto line 415
Source documentation
Operator-norm null changes in a family of unitaries do not change its Hilbert-ultraproduct action.
```
theorem unitary_eq_of_tendsto (U V : ∀ i, E i ≃ₗᵢ[ℂ] E i)
    (h : Tendsto (fun i => ‖(U i : E i →L[ℂ] E i) - (V i : E i →L[ℂ] E i)‖)
      (ω : Filter ι) (𝓝 0)) : unitary ω U = unitary ω V := by
…
```
Mentions: OAI.NuclearUltrapower.HilbertUltraproduct.unitary

def OAI.NuclearUltrapower.HilbertUltraproduct.approximateRepresentation line 427

Source documentation

Pointwise asymptotic multiplicativity suffices. There is no hidden intersection over all group relations, nor any dimension bound.

def approximateRepresentation {Γ : Type w} [Group Γ]
    (U : Γ → ∀ i, E i ≃ₗᵢ[ℂ] E i)
    (h1 : Tendsto (fun i => ‖(U 1 i : E i →L[ℂ] E i) -
      ((1 : E i ≃ₗᵢ[ℂ] E i) : E i →L[ℂ] E i)‖) (ω : Filter ι) (𝓝 0))
    (hmul : ∀ g h, Tendsto (fun i => ‖(U (g * h) i : E i →L[ℂ] E i) -
      ((U g i * U h i) : E i →L[ℂ] E i)‖) (ω : Filter ι) (𝓝 0)) :
    Γ →* (HilbertUltraproduct E ω ≃ₗᵢ[ℂ] HilbertUltraproduct E ω) where
…

Mentions: OAI.NuclearUltrapower.HilbertUltraproduct

def OAI.NuclearUltrapower.tupleEnergy line 455
Source documentation
The quadratic form of the matching Laplacian.
```
def tupleEnergy (S : Finset Γ) (U : Γ → E ≃ₗᵢ[ℂ] E) (x : E) : ℝ :=
…
```
theorem OAI.NuclearUltrapower.tupleEnergy_nonneg line 458
theorem OAI.NuclearUltrapower.tupleEnergy_bound line 461
theorem OAI.NuclearUltrapower.tupleEnergy_smul line 472
theorem OAI.NuclearUltrapower.tupleEnergy_continuous line 476
def OAI.NuclearUltrapower.bottomEnergy line 485
Source documentation
Bottom Rayleigh energy, equal to the bottom of the matching spectrum in a faithful representation. This definition retains arbitrary Hilbert dimension.
```
def bottomEnergy (S : Finset Γ) (U : Γ → E ≃ₗᵢ[ℂ] E) : ℝ :=
…
```
theorem OAI.NuclearUltrapower.energyValues_nonempty line 488
theorem OAI.NuclearUltrapower.energyValues_bddBelow line 494
theorem OAI.NuclearUltrapower.bottomEnergy_nonneg line 500
theorem OAI.NuclearUltrapower.bottomEnergy_le line 505
theorem OAI.NuclearUltrapower.bottomEnergy_bound line 509
theorem OAI.NuclearUltrapower.bottomEnergy_mul_norm line 516
theorem OAI.NuclearUltrapower.exists_energy_lt line 532
theorem OAI.NuclearUltrapower.HilbertUltraproduct.tupleEnergy_tendsto line 548
Source documentation
Finite Laplacian energies pass to the Hilbert ultraproduct exactly.
```
theorem tupleEnergy_tendsto (S : Finset Γ) (U : Γ → ∀ i, E i ≃ₗᵢ[ℂ] E i)
    (x : UltraPreHilbert E ω) :
    Tendsto (fun i => tupleEnergy S (fun g => U g i) (UltraPreHilbert.family ω x i))
      (ω : Filter ι) (𝓝 (tupleEnergy S (fun g => unitary ω (U g))
        (x : HilbertUltraproduct E ω))) := by
…
```
Mentions: OAI.NuclearUltrapower.UltraPreHilbert, OAI.NuclearUltrapower.tupleEnergy, OAI.NuclearUltrapower.UltraPreHilbert.family, OAI.NuclearUltrapower.HilbertUltraproduct.unitary, OAI.NuclearUltrapower.HilbertUltraproduct
theorem OAI.NuclearUltrapower.HilbertUltraproduct.bottomEnergy_tendsto line 565
Source documentation
Bottom matching energies always have an ultralimit, with the uniform upper bound 4 |S| and no dimension restriction.
```
theorem bottomEnergy_tendsto (S : Finset Γ) (U : Γ → ∀ i, E i ≃ₗᵢ[ℂ] E i) :
    Tendsto (fun i => bottomEnergy S (fun g => U g i)) (ω : Filter ι)
      (𝓝 (limUnder (ω : Filter ι) (fun i => bottomEnergy S (fun g => U g i)))) := by
…
```
Mentions: OAI.NuclearUltrapower.bottomEnergy
theorem OAI.NuclearUltrapower.HilbertUltraproduct.limit_energy_lower line 576
Source documentation
Lower coordinate Rayleigh bounds pass to every vector of the completion, not merely to vectors given by elementary tensors or bounded families.
```
theorem limit_energy_lower (S : Finset Γ) (U : Γ → ∀ i, E i ≃ₗᵢ[ℂ] E i)
    {r : ℝ} (hr : Tendsto (fun i => bottomEnergy S (fun g => U g i))
      (ω : Filter ι) (𝓝 r)) (x : HilbertUltraproduct E ω) :
    r * ‖x‖ ^ 2 ≤ tupleEnergy S (fun g => unitary ω (U g)) x := by
…
```
Mentions: OAI.NuclearUltrapower.bottomEnergy, OAI.NuclearUltrapower.HilbertUltraproduct, OAI.NuclearUltrapower.tupleEnergy, OAI.NuclearUltrapower.HilbertUltraproduct.unitary

theorem OAI.NuclearUltrapower.HilbertUltraproduct.varying_gap line 591

Source documentation

Varying-dimensional spectral gap, expressed in the equivalent Rayleigh formulation from the tensor-norm formulation. No uniform dimension bound and no coordinate group relations are assumed.

theorem varying_gap [Group Γ] (S : Finset Γ) (κ : ℝ)
    (hgap : HasKazhdanGap.{w, max u v} S κ)
    (U : Γ → ∀ i, E i ≃ₗᵢ[ℂ] E i)
    (h1 : Tendsto (fun i => ‖(U 1 i : E i →L[ℂ] E i) -
      ((1 : E i ≃ₗᵢ[ℂ] E i) : E i →L[ℂ] E i)‖) (ω : Filter ι) (𝓝 0))
    (hmul : ∀ g h, Tendsto (fun i => ‖(U (g * h) i : E i →L[ℂ] E i) -
      ((U g i * U h i) : E i →L[ℂ] E i)‖) (ω : Filter ι) (𝓝 0))
    {r : ℝ} (hr : Tendsto (fun i => bottomEnergy S (fun g => U g i))
      (ω : Filter ι) (𝓝 r)) : r = 0 ∨ κ ≤ r ∧ r ≤ 4 * (S.card : ℝ) := by
…

Mentions: OAI.NuclearUltrapower.bottomEnergy