HilbertInduction.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

def OAI.NuclearUltrapower.lpUnitary line 14

Source documentation

A coordinate permutation with unitary entries on a Hilbert direct sum.

def lpUnitary {ι : Type u} {V : Type v} [NormedAddCommGroup V]
    [InnerProductSpace ℂ V] (e : Equiv.Perm ι) (T : ι → V ≃ₗᵢ[ℂ] V) :
    lp (fun _ : ι => V) 2 ≃ₗᵢ[ℂ] lp (fun _ : ι => V) 2 := by
…

theorem OAI.NuclearUltrapower.lpUnitary_apply line 42
def OAI.NuclearUltrapower.cosetRep line 50
Source documentation
A normalized transversal; the identity coset is represented by the identity.
```
def cosetRep (i : G ⧸ H) : G := by
…
```
Mentions: OAI.NuclearUltrapower.G
theorem OAI.NuclearUltrapower.cosetRep_identity line 54
theorem OAI.NuclearUltrapower.cosetRep_mk line 57
def OAI.NuclearUltrapower.cosetCocycle line 65
Source documentation
The transversal cocycle, with source coordinate i and target g • i.
```
def cosetCocycle (g : G) (i : G ⧸ H) : H :=
…
```
Mentions: OAI.NuclearUltrapower.G
theorem OAI.NuclearUltrapower.cosetCocycle_one line 72
theorem OAI.NuclearUltrapower.cosetCocycle_mul line 76
def OAI.NuclearUltrapower.inducedUnitary line 86
Source documentation
Unitary induction with no finite-index assumption.
```
def inducedUnitary : G →* (lp (fun _ : G ⧸ H => V) 2 ≃ₗᵢ[ℂ]
    lp (fun _ : G ⧸ H => V) 2) where
…
```
Mentions: OAI.NuclearUltrapower.G
theorem OAI.NuclearUltrapower.inducedUnitary_apply line 98
theorem OAI.NuclearUltrapower.subgroup_smul_identity line 102
Source documentation
Subgroup elements fix the identity left coset.
```
@[simp] theorem subgroup_smul_identity (h : H) :
    (h : G) • (QuotientGroup.mk 1 : G ⧸ H) = QuotientGroup.mk 1 := by
…
```
Mentions: OAI.NuclearUltrapower.G
theorem OAI.NuclearUltrapower.cosetCocycle_identity line 108
theorem OAI.NuclearUltrapower.cosetRep_smul_identity line 113
theorem OAI.NuclearUltrapower.induced_identity_coordinate line 118
theorem OAI.NuclearUltrapower.induced_translate_coordinate line 127
Source documentation
Translation of a coordinate to the identity has cocycle one.
```
theorem induced_translate_coordinate (i : G ⧸ H)
    (x : lp (fun _ : G ⧸ H => V) 2) :
    inducedUnitary H α (cosetRep H i)⁻¹ x (QuotientGroup.mk 1) = x i := by
…
```
Mentions: OAI.NuclearUltrapower.G, OAI.NuclearUltrapower.inducedUnitary, OAI.NuclearUltrapower.cosetRep
def OAI.NuclearUltrapower.inductionInclusion line 143
Source documentation
The original representation embeds on the identity coordinate.
```
def inductionInclusion : V →ₗᵢ[ℂ] lp (fun _ : G ⧸ H => V) 2 := by
…
```
Mentions: OAI.NuclearUltrapower.G
theorem OAI.NuclearUltrapower.inductionInclusion_apply line 149
theorem OAI.NuclearUltrapower.inductionInclusion_intertwines line 152
abbrev OAI.NuclearUltrapower.L2 line 179
def OAI.NuclearUltrapower.l2Single line 182
Source documentation
Coordinate lines in a Hilbert direct sum.
```
def l2Single {I : Type u} (i : I) : ℂ →ₗᵢ[ℂ] L2 I := by
…
```
Mentions: OAI.NuclearUltrapower.L2
theorem OAI.NuclearUltrapower.l2Single_apply line 187
theorem OAI.NuclearUltrapower.l2Single_orthogonal line 190
def OAI.NuclearUltrapower.l2Embedding line 198
Source documentation
An injection of coordinate sets induces an honest Hilbert isometry.
```
def l2Embedding {I : Type u} {J : Type v} (e : I ↪ J) : L2 I →ₗᵢ[ℂ] L2 J :=
…
```
Mentions: OAI.NuclearUltrapower.L2
theorem OAI.NuclearUltrapower.l2Embedding_single line 202
theorem OAI.NuclearUltrapower.l2Embedding_adjoint_apply line 209
Source documentation
The adjoint of coordinate extension is coordinate restriction.
```
@[simp] theorem l2Embedding_adjoint_apply {I : Type u} {J : Type v} (e : I ↪ J)
    (x : L2 J) (i : I) : (l2Embedding e).toContinuousLinearMap.adjoint x i = x (e i) := by
…
```
Mentions: OAI.NuclearUltrapower.L2, OAI.NuclearUltrapower.l2Embedding

theorem OAI.NuclearUltrapower.l2_clm_ext line 218

Source documentation

Bounded maps on a Hilbert direct sum are determined by coordinate vectors.

theorem l2_clm_ext {I : Type u} {E : Type v} [NormedAddCommGroup E] [NormedSpace ℂ E]
    {T U : L2 I →L[ℂ] E} (h : ∀ i c, T (lp.single 2 i c) = U (lp.single 2 i c)) : T = U := by
…

Mentions: OAI.NuclearUltrapower.L2