OAI/Analysis/Unitarizability/Frames.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Dixmier.SignMatrix.extendVector line 17
2. theorem OAI.Dixmier.SignMatrix.extendVector_norm line 20
3. theorem OAI.Dixmier.SignMatrix.synthesis_extendVector line 27
4. theorem OAI.Dixmier.SignMatrix.synthesis_restrict_norm line 34
5. theorem OAI.Dixmier.SignMatrix.all_subfamilies line 42

   Source documentation

   Extend each smaller subset to size p, then restrict a coordinate synthesis operator.

   theorem all_subfamilies {k p : ℕ} (hp : p ≤ Fintype.card I) (σ : Fin k × I → Bool)
       (hσ : ∀ e : Fin p ↪ I, ‖synthesis σ e‖ ≤ 10) :
       ∀ J : Finset I, J.card ≤ p →
         ‖FiniteSynthesis.synthesis (fun i => ComplexFrames.ofReal (vector σ i)) J‖ ≤ 10 := by
   …

   Mentions: OAI.Dixmier.SignMatrix.synthesis, OAI.Dixmier.FiniteSynthesis.synthesis, OAI.Dixmier.ComplexFrames.ofReal, OAI.Dixmier.SignMatrix.vector

6. theorem OAI.Dixmier.SignMatrix.frames line 71

   Source documentation

   Frames with k=ceil(2r log(2n)), p=min(2r,n), and bound 10.

   theorem frames {n r : ℕ} (hn : 2 ≤ n) (hr : 1 ≤ r) :
       ∃ v : Fin n → EuclideanSpace ℂ (Fin (FrameParameters.dimension n r)),
         (∀ i, ‖v i‖ = 1) ∧
         FiniteSynthesis.FrameBound v (FrameParameters.subfamilySize n r) 10 := by
   …

   Mentions: OAI.Dixmier.FrameParameters.dimension, OAI.Dixmier.FiniteSynthesis.FrameBound, OAI.Dixmier.FrameParameters.subfamilySize

7. theorem OAI.Dixmier.SignMatrix.frames_for_fintype line 85

   Source documentation

   The frame lemma for arbitrary finite label types.

   theorem frames_for_fintype {r : ℕ} (hn : 2 ≤ Fintype.card I) (hr : 1 ≤ r) :
       ∃ v : I → EuclideanSpace ℂ (Fin (FrameParameters.dimension (Fintype.card I) r)),
         (∀ i, ‖v i‖ = 1) ∧
         FiniteSynthesis.FrameBound v (FrameParameters.subfamilySize (Fintype.card I) r) 10 := by
   …

   Mentions: OAI.Dixmier.FrameParameters.dimension, OAI.Dixmier.FiniteSynthesis.FrameBound, OAI.Dixmier.FrameParameters.subfamilySize