OAI/NumberTheory/TwoPoint/Bounds/CoordinateEmbedding.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.extendByZero_basis line 16
2. lemma OAI.TwoPointCorrelations.extendByZero_injective line 31
3. lemma OAI.TwoPointCorrelations.formalDeparture_extend line 38
4. theorem OAI.TwoPointCorrelations.selected_rank_rename_iff line 47

   Source documentation

   In particular, a rank witness in the ambient prime pool is equivalent to the witness on its observed equality classes.

   theorem selected_rank_rename_iff (e : α → β) (he : Function.Injective e)
       (label : ℕ → α) (coefficient : ℕ → ℝ) (left right : ρ → ℕ) (control : ρ → α) :
       LinearIndependent ℝ (Sum.elim
         (fun i => formalDeparture label coefficient (left i) - formalDeparture label coefficient (right i))
         (fun i => Pi.basisFun ℝ α (control i))) ↔
       LinearIndependent ℝ (Sum.elim
         (fun i => formalDeparture (e ∘ label) coefficient (left i) -
           formalDeparture (e ∘ label) coefficient (right i))
         (fun i => Pi.basisFun ℝ β (e (control i)))) := by
   …

   Mentions: OAI.TwoPointCorrelations.formalDeparture