OAI/Analysis/NuclearUltrapower/InitialMatching.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NuclearUltrapower.matrixMap_injective line 12
2. theorem OAI.NuclearUltrapower.matchingTuple_coe line 26
3. theorem OAI.NuclearUltrapower.matching_energy_coe line 35
4. theorem OAI.NuclearUltrapower.not_matches_coefficient_bound line 44

   Source documentation

   Failure of matching is a matrix norm bound, with no relation imposed on u.

   theorem not_matches_coefficient_bound (hρ : Function.Injective ρ)
       (π : FiniteUnitaryRep.{u,v} Γ) {n : Type*} [Fintype n] [DecidableEq n]
       (b : OrthonormalBasis n ℂ π) (a : ℝ) (ha : a ≤ 4 * (S.card : ℝ))
       (hm : ¬ Matches ρ S u a π) :
       ‖(4 * (S.card : ℝ)) • (1 : CStarMatrix n n B) -
         laplacian S (fun s => coefficientMatrix (fun i j => b.repr (π.action s (b j)) i) (u s : B))‖
         ≤ 4 * (S.card : ℝ) - a := by
   …

   Mentions: OAI.NuclearUltrapower.Matches, OAI.NuclearUltrapower.laplacian, OAI.NuclearUltrapower.coefficientMatrix

5. theorem OAI.NuclearUltrapower.coefficient_bound_no_invariant line 100

   Source documentation

   The full algebra can see an invariant tensor in any representation. A strict complemented-matrix bound would exclude that tensor.

   theorem coefficient_bound_no_invariant (hψ : ∀ g, ψ (w g) = (σ g : K →L[ℂ] K))
       (a : ℝ) (ha : 0 < a)
       (hb : ‖(4 * (S.card : ℝ)) • (1 : CStarMatrix n n A) -
         laplacian S (fun s => coefficientMatrix (fun i j => b.repr (π s (b j)) i) (w s))‖ ≤
           4 * (S.card : ℝ) - a)
       (z : K ⊗[ℂ] F) (hz : ∀ s ∈ S, TensorProduct.congrIsometry (σ s) (π s) z = z) : z = 0 := by
   …

   Mentions: OAI.NuclearUltrapower.laplacian, OAI.NuclearUltrapower.coefficientMatrix

6. theorem OAI.NuclearUltrapower.initial_match line 169

   Source documentation

   A full-algebra invariant tensor forces matching on an ultrafilter-large set. This is fixed-size matrix amplification, not an illicit varying-size one.

   theorem initial_match (π : FiniteUnitaryRep.{u,u} Γ) (a : ℝ)
       (ha0 : 0 < a) (ha : a ≤ 4 * (S.card : ℝ))
       (z : K ⊗[ℂ] π) (hz0 : z ≠ 0)
       (hz : ∀ s ∈ S, TensorProduct.congrIsometry (σ s) (π.action s) z = z) :
       ∀ᶠ n in (ω : Filter ℕ), Matches ρ S (fun g => u g n) a π := by
   …

   Mentions: OAI.NuclearUltrapower.Matches