Exact source: MathlibAnnex/Analysis/Normed/Operator/SelectedMinor.lean
Pinned GitHub source · Raw UTF-8 source
Back to Maximal-minor integral differences for Lipschitz perturbations
1import MathlibAnnex.LinearAlgebra.Matrix.MaximalMinor2import Mathlib.Analysis.Normed.Operator.NormedSpace3import Mathlib.LinearAlgebra.Matrix.ToLin4import Mathlib.Topology.Algebra.Module.FiniteDimension5import Mathlib.Tactic67/-!8# Output selection for maximal minors910Contractive output selection acts on continuous linear maps and their operator11spaces. Its determinant is the maximal minor in the canonical increasing row order.12-/1314noncomputable section1516namespace MathlibAnnex17namespace ContinuousLinearMap1819universe u2021/-- Select the output coordinates in the increasing order fixed by a22maximal-minor index. -/23def selectedOutputLinearMap {n : ℕ} {ι : Type u} [Fintype ι] [LinearOrder ι]24 (s : Matrix.MaximalMinorIndex n ι) :25 (ι → ℝ) →ₗ[ℝ] (Fin n → ℝ) where26 toFun y i := y (s.orderedRows i)27 map_add' _ _ := rfl28 map_smul' _ _ := rfl2930/-- Coordinate selection is contractive for the finite Pi sup norms. -/31theorem norm_selectedOutputLinearMap_le32 {n : ℕ} {ι : Type u} [Fintype ι] [LinearOrder ι]33 (s : Matrix.MaximalMinorIndex n ι) (y : ι → ℝ) :34 ‖selectedOutputLinearMap s y‖ ≤ ‖y‖ := by35 apply (pi_norm_le_iff_of_nonneg (norm_nonneg y)).236 intro i37 change ‖y (s.orderedRows i)‖ ≤ ‖y‖38 exact norm_le_pi_norm y _3940/-- Output-coordinate selection as a continuous linear map. -/41noncomputable def selectedOutput42 {n : ℕ} {ι : Type u} [Fintype ι] [LinearOrder ι]43 (s : Matrix.MaximalMinorIndex n ι) :44 (ι → ℝ) →L[ℝ] (Fin n → ℝ) :=45 (selectedOutputLinearMap s).mkContinuous 1 fun y => by46 simpa using norm_selectedOutputLinearMap_le s y4748@[simp] theorem selectedOutput_apply49 {n : ℕ} {ι : Type u} [Fintype ι] [LinearOrder ι]50 (s : Matrix.MaximalMinorIndex n ι) (y : ι → ℝ) (i : Fin n) :51 selectedOutput s y i = y (s.orderedRows i) := rfl5253/-- The square operator obtained by selecting `n` output coordinates. -/54noncomputable def selectedSquare55 {n : ℕ} {ι : Type u} [Fintype ι] [LinearOrder ι]56 (s : Matrix.MaximalMinorIndex n ι)57 (A : (Fin n → ℝ) →L[ℝ] (ι → ℝ)) :58 (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) :=59 (selectedOutput s).comp A6061/-- Output selection bundled as a continuous linear map on operator spaces. -/62noncomputable def selectedSquareCLM63 {n : ℕ} {ι : Type u} [Fintype ι] [LinearOrder ι]64 (s : Matrix.MaximalMinorIndex n ι) :65 ((Fin n → ℝ) →L[ℝ] (ι → ℝ)) →L[ℝ]66 ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) :=67 (selectedOutput s).postcomp (Fin n → ℝ)6869@[simp] theorem selectedSquareCLM_apply70 {n : ℕ} {ι : Type u} [Fintype ι] [LinearOrder ι]71 (s : Matrix.MaximalMinorIndex n ι)72 (A : (Fin n → ℝ) →L[ℝ] (ι → ℝ)) :73 selectedSquareCLM s A = selectedSquare s A := rfl7475/-- The output selection has operator norm at most one. -/76theorem norm_selectedOutput_le_one77 {n : ℕ} {ι : Type u} [Fintype ι] [LinearOrder ι]78 (s : Matrix.MaximalMinorIndex n ι) :79 ‖selectedOutput s‖ ≤ 1 := by80 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one81 intro y82 change ‖selectedOutputLinearMap s y‖ ≤ 1 * ‖y‖83 simpa only [one_mul] using norm_selectedOutputLinearMap_le s y8485/-- Selection is contractive on operator spaces. -/86theorem norm_selectedSquare_le87 {n : ℕ} {ι : Type u} [Fintype ι] [LinearOrder ι]88 (s : Matrix.MaximalMinorIndex n ι)89 (A : (Fin n → ℝ) →L[ℝ] (ι → ℝ)) :90 ‖selectedSquare s A‖ ≤ ‖A‖ := by91 calc92 ‖selectedSquare s A‖ ≤ ‖selectedOutput s‖ * ‖A‖ :=93 ContinuousLinearMap.opNorm_comp_le _ _94 _ ≤ 1 * ‖A‖ :=95 mul_le_mul_of_nonneg_right (norm_selectedOutput_le_one s) (norm_nonneg A)96 _ = ‖A‖ := one_mul _9798@[simp] theorem selectedSquare_sub99 {n : ℕ} {ι : Type u} [Fintype ι] [LinearOrder ι]100 (s : Matrix.MaximalMinorIndex n ι)101 (P Q : (Fin n → ℝ) →L[ℝ] (ι → ℝ)) :102 selectedSquare s (P - Q) = selectedSquare s P - selectedSquare s Q := by103 change selectedSquareCLM s (P - Q) =104 selectedSquareCLM s P - selectedSquareCLM s Q105 exact map_sub (selectedSquareCLM s) P Q106107/-- The determinant of the selected square operator is the maximal minor108of the standard-basis matrix of the original operator. -/109@[simp] theorem det_selectedSquare110 {n : ℕ} {ι : Type u} [Fintype ι] [LinearOrder ι]111 (s : Matrix.MaximalMinorIndex n ι)112 (A : (Fin n → ℝ) →L[ℝ] (ι → ℝ)) :113 LinearMap.det (selectedSquare s A :114 (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ)) =115 Matrix.maximalMinor116 (LinearMap.toMatrix' (A : (Fin n → ℝ) →ₗ[ℝ] (ι → ℝ))) s := by117 rw [← LinearMap.det_toMatrix'118 (selectedSquare s A : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ))]119 unfold Matrix.maximalMinor Matrix.maximalSubmatrix selectedSquare selectedOutput120 congr 1121122end ContinuousLinearMap123end MathlibAnnex