EndpointDensity.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Density for unrestricted endpoints and centered tensor letters

The two endpoint variables and the finitely many centered letters have different ambient Hilbert spaces. Nested dense matrix stages nevertheless give a common stage, so their continuous coefficient identities extend together.

theorem OAI.KadisonSimilarity.exists_common_dependent_stage line 21

Source documentation

A finite dependent tuple in nested dense stages has a common stage.

theorem exists_common_dependent_stage {ι : Type*} [Fintype ι] {V : ι → Type*}
    (S : ℕ → ∀ i, Set (V i)) (hmono : ∀ i, Monotone (fun n => S n i))
    (x : ∀ i, V i) (hx : ∀ i, x i ∈ ⋃ n, S n i) :
    ∃ n, ∀ i, x i ∈ S n i := by
…

theorem OAI.KadisonSimilarity.continuous_eq_of_nested_dependent_stages line 32

Source documentation

Dependent finite-coordinate version of continuity from nested dense stages.

theorem continuous_eq_of_nested_dependent_stages {ι : Type*} [Fintype ι]
    {V : ι → Type*} [∀ i, TopologicalSpace (V i)]
    (S : ℕ → ∀ i, Set (V i)) (hmono : ∀ i, Monotone (fun n => S n i))
    (hdense : ∀ i, Dense (⋃ n, S n i))
    (f g : (∀ i, V i) → ℂ) (hf : Continuous f) (hg : Continuous g)
    (hstage : ∀ n x, (∀ i, x i ∈ S n i) → f x = g x) : f = g := by
…

theorem OAI.KadisonSimilarity.continuous_endpointWord line 51
Source documentation
Continuity of the completed word, including its unrestricted endpoint.
```
theorem continuous_endpointWord (n : ℕ) :
    Continuous (fun p : E × (Fin n → F) => endpointWord p.1 p.2) := by
…
```
Mentions: OAI.KadisonSimilarity.endpointWord

theorem OAI.KadisonSimilarity.continuous_eq_of_two_nested_stages line 62

Source documentation

Two groups of finite coordinates can use different Hilbert spaces.

theorem continuous_eq_of_two_nested_stages {ι κ : Type*} [Fintype ι] [Fintype κ]
    (S : ℕ → Set E) (T : ℕ → Set F) (hS : Monotone S) (hT : Monotone T)
    (hdS : Dense (⋃ n, S n)) (hdT : Dense (⋃ n, T n))
    (f g : (ι → E) × (κ → F) → ℂ) (hf : Continuous f) (hg : Continuous g)
    (hstage : ∀ n p, (∀ i, p.1 i ∈ S n) → (∀ j, p.2 j ∈ T n) → f p = g p) :
    f = g := by
…

abbrev OAI.KadisonSimilarity.EndpointLetters line 84
Source documentation
The pair of endpoint letters and all centered tail letters.
```
abbrev EndpointLetters (E F : Type u) (k l : ℕ) :=
…
```
def OAI.KadisonSimilarity.endpointTracialCoefficient line 87
theorem OAI.KadisonSimilarity.continuous_endpointTracialCoefficient line 93

theorem OAI.KadisonSimilarity.endpoint_pairing_identity_of_stages line 111

Source documentation

Extend a stage endpoint pairing formula to all endpoints and tail letters.

theorem endpoint_pairing_identity_of_stages {k l : ℕ}
    (Y : EndpointTensor E F k →L[ℂ] EndpointTensor E F l)
    (J : F → F) (hJ : Continuous J) (B : F →L[ℂ] F →L[ℂ] ℂ)
    (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
    (S : ℕ → Set E) (T : ℕ → Set F) (hS : Monotone S) (hT : Monotone T)
    (hdS : Dense (⋃ n, S n)) (hdT : Dense (⋃ n, T n))
    (hstage : ∀ n d a v, d ∈ S n → a ∈ S n → (∀ i, v i ∈ T n) →
      inner ℂ (endpointWord a (fun j => J (v (.inr j))))
        (Y (endpointWord d (fun i => v (.inl i)))) =
      inner ℂ a d * ∑ P, c P * pairingPolynomial sourceFirstRank B P v) :
    ∀ d a v,
      inner ℂ (endpointWord a (fun j => J (v (.inr j))))
…

Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.endpointWord, OAI.KadisonSimilarity.pairingPolynomial, OAI.KadisonSimilarity.sourceFirstRank