OAI/Analysis/MatrixScaling/Expansion.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic and finite-block expansion inequalities.

  1. def OAI.Kaplansky.IntrinsicExpanding line 19
  2. theorem OAI.Kaplansky.intrinsicExpanding_equiv line 23
  3. theorem OAI.Kaplansky.basis_matrix_action line 38
  4. theorem OAI.Kaplansky.expanding_in_basis line 50
  5. def OAI.Kaplansky.prodSubmoduleKernelEquiv line 74

    Source documentation

    The kernel of the last-block projection is the first-block intersection.

    def prodSubmoduleKernelEquiv (S : Submodule ℂ (E × F)) :
    S.comap (LinearMap.inl ℂ E F) ≃ₗ[ℂ]
      LinearMap.ker ((LinearMap.snd ℂ E F).comp S.subtype) where
…
  6. theorem OAI.Kaplansky.prod_submodule_finrank line 101
  7. def OAI.Kaplansky.ExpandingThrough line 110

    Source documentation

    Expansion restricted to the dimensions used by the sixteen small-subspace maps.

    def ExpandingThrough (m : ℕ) (T : Fin n → E →ₗ[ℂ] G) : Prop :=
…
  8. theorem OAI.Kaplansky.expandingThrough_prod line 116
  9. theorem OAI.Kaplansky.expandingThrough_equiv line 157
  10. def OAI.Kaplansky.piSuccLinearEquiv line 175
  11. def OAI.Kaplansky.blockDiagonal line 185
  12. theorem OAI.Kaplansky.expandingThrough_blocks line 193
  13. theorem OAI.Kaplansky.image_iSup_finrank_le line 226
  14. theorem OAI.Kaplansky.combined_expanding line 239