OAI/Analysis/Daugavet/Enlargement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ExactModuli.KW.EnlargementData line 11
2. theorem OAI.ExactModuli.KW.finite_dimensional_enlargement line 28

   Source documentation

   The complete quantitative Kadets–Werner finite-dimensional enlargement.

   theorem finite_dimensional_enlargement {κ : Type} [Fintype κ] [Nonempty κ]
       (G : Submodule ℝ KWL1) [FiniteDimensional ℝ G] (_hG : G ≠ ⊥)
       (hcoords : FiniteCoordinates G) (u : κ → G) (hu : ∀ k, ‖u k‖ = 1)
       {h : ℝ} (hh : 0 < h) (hh1 : h < 1) :
       Nonempty (EnlargementData G (fun k => (u k : KWL1)) h) := by
   …

   Mentions: OAI.ExactModuli.KW.KWL1, OAI.ExactModuli.KW.FiniteCoordinates, OAI.ExactModuli.KW.EnlargementData