Exact source: MathlibAnnex/Analysis/Normed/Operator/Determinant.lean
Pinned GitHub source · Raw UTF-8 source
Back to Determinant integrals under strong $L^n$ convergence
1import Mathlib.Analysis.Normed.Module.FiniteDimension2import Mathlib.LinearAlgebra.Matrix.Determinant.Basic3import Mathlib.LinearAlgebra.Matrix.ToLin4import Mathlib.Tactic56/-!7# Determinant difference estimates for finite sup-norm coordinate spaces89For a finite type `ι`, the function space `ι → ℝ` has the sup norm. The dual norm10of a matrix row is therefore its `ℓ¹` norm. Replacing rows one at a time gives a11locally Lipschitz estimate for the determinant of continuous linear endomorphisms.1213The stronger bound uses `max ‖P‖ ‖Q‖`; the source-compatible bound with14`‖P‖ + ‖Q‖` follows immediately. These statements are specific to the operator15norm induced by the sup norm on the displayed Pi spaces; they are not Euclidean16operator-norm statements.17-/1819noncomputable section2021open Equiv Finset22open scoped BigOperators2324namespace MathlibAnnex2526namespace Matrix2728universe u2930/-- The `ℓ¹` norm of one row of a finite real matrix. -/31def rowL1Norm {ι : Type u} [Fintype ι]32 (M : _root_.Matrix ι ι ℝ) (i : ι) : ℝ :=33 ∑ j, |M i j|3435private theorem abs_det_le_sum_perm_products36 {ι : Type u} [Fintype ι] [DecidableEq ι]37 (M : _root_.Matrix ι ι ℝ) :38 |M.det| ≤ ∑ σ : Equiv.Perm ι, ∏ i, |M (σ i) i| := by39 rw [_root_.Matrix.det_apply']40 calc41 |∑ σ : Equiv.Perm ι,42 ((((Equiv.Perm.sign σ : Units ℤ) : ℤ) : ℝ) *43 ∏ i, M (σ i) i)| ≤44 ∑ σ : Equiv.Perm ι,45 |((((Equiv.Perm.sign σ : Units ℤ) : ℤ) : ℝ) *46 ∏ i, M (σ i) i)| :=47 abs_sum_le_sum_abs _ _48 _ = ∑ σ : Equiv.Perm ι, ∏ i, |M (σ i) i| := by49 apply Finset.sum_congr rfl50 intro σ _hσ51 have hsignZ : |(((Equiv.Perm.sign σ : Units ℤ) : ℤ))| = 1 :=52 Equiv.Perm.sign_abs σ53 have hsignR : |((((Equiv.Perm.sign σ : Units ℤ) : ℤ) : ℝ))| = 1 := by54 exact_mod_cast hsignZ55 rw [abs_mul, hsignR, one_mul, abs_prod]5657private theorem perm_product_reindex_by_rows58 {ι : Type u} [Fintype ι] [DecidableEq ι]59 (M : _root_.Matrix ι ι ℝ) (σ : Equiv.Perm ι) :60 (∏ i, |M (σ i) i|) = ∏ i, |M i (σ.symm i)| := by61 apply Fintype.prod_equiv σ62 intro i63 simp6465private theorem sum_perm_products_le_sum_all_row_choices66 {ι : Type u} [Fintype ι] [DecidableEq ι]67 (M : _root_.Matrix ι ι ℝ) :68 (∑ σ : Equiv.Perm ι, ∏ i, |M i (σ.symm i)|) ≤69 ∑ f : ι → ι, ∏ i, |M i (f i)| := by70 classical71 let e : Equiv.Perm ι → (ι → ι) := fun σ => σ.symm72 have he : Function.Injective e := by73 intro σ τ h74 apply Equiv.symm_bijective.injective75 apply Equiv.ext76 exact congrFun h77 let S : Finset (ι → ι) := Finset.univ.image e78 calc79 (∑ σ : Equiv.Perm ι, ∏ i, |M i (σ.symm i)|) =80 S.sum (fun f => ∏ i, |M i (f i)|) := by81 dsimp [S]82 rw [Finset.sum_image]83 exact he.injOn84 _ ≤ Finset.univ.sum (fun f : ι → ι => ∏ i, |M i (f i)|) := by85 apply Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ S)86 intro f _hf _hnot87 positivity8889/-- Hadamard's determinant bound using the product of row `ℓ¹` norms. -/90theorem abs_det_le_prod_rowL1Norm91 {ι : Type u} [Fintype ι] [DecidableEq ι]92 (M : _root_.Matrix ι ι ℝ) :93 |M.det| ≤ ∏ i, rowL1Norm M i := by94 calc95 |M.det| ≤ ∑ σ : Equiv.Perm ι, ∏ i, |M (σ i) i| :=96 abs_det_le_sum_perm_products M97 _ = ∑ σ : Equiv.Perm ι, ∏ i, |M i (σ.symm i)| := by98 apply Finset.sum_congr rfl99 intro σ _hσ100 exact perm_product_reindex_by_rows M σ101 _ ≤ ∑ f : ι → ι, ∏ i, |M i (f i)| :=102 sum_perm_products_le_sum_all_row_choices M103 _ = ∏ i, rowL1Norm M i := by104 change (∑ f : ι → ι, ∏ i, |M i (f i)|) =105 ∏ i, ∑ j, |M i j|106 simpa only [Finset.sum_filter, Finset.mem_univ, ↓reduceIte,107 Fintype.piFinset_univ] using108 (Finset.prod_univ_sum (fun _ : ι => Finset.univ)109 (fun i j => |M i j|)).symm110111end Matrix112113namespace ContinuousLinearMap114115universe u116117private def stdMatrix {ι : Type u} [Fintype ι] [DecidableEq ι]118 (A : (ι → ℝ) →L[ℝ] (ι → ℝ)) : _root_.Matrix ι ι ℝ :=119 fun i j => A (Pi.single j 1) i120121private theorem stdMatrix_eq_toMatrix'122 {ι : Type u} [Fintype ι] [DecidableEq ι]123 (A : (ι → ℝ) →L[ℝ] (ι → ℝ)) :124 stdMatrix A = LinearMap.toMatrix' (A : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)) := by125 ext i j126 rfl127128private theorem stdMatrix_mulVec129 {ι : Type u} [Fintype ι] [DecidableEq ι]130 (A : (ι → ℝ) →L[ℝ] (ι → ℝ)) (x : ι → ℝ) :131 (stdMatrix A).mulVec x = A x := by132 rw [stdMatrix_eq_toMatrix']133 exact LinearMap.toMatrix'_mulVec (A : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)) x134135@[simp] private theorem stdMatrix_sub136 {ι : Type u} [Fintype ι] [DecidableEq ι]137 (P Q : (ι → ℝ) →L[ℝ] (ι → ℝ)) :138 stdMatrix (P - Q) = stdMatrix P - stdMatrix Q := by139 ext i j140 simp [stdMatrix]141142private def rowSign {ι : Type u} [Fintype ι] [DecidableEq ι]143 (M : _root_.Matrix ι ι ℝ) (i : ι) : ι → ℝ :=144 fun j => if 0 ≤ M i j then 1 else -1145146private theorem norm_rowSign_le_one147 {ι : Type u} [Fintype ι] [DecidableEq ι]148 (M : _root_.Matrix ι ι ℝ) (i : ι) :149 ‖rowSign M i‖ ≤ 1 := by150 apply (pi_norm_le_iff_of_nonneg zero_le_one).2151 intro j152 by_cases h : 0 ≤ M i j153 · simp [rowSign, h]154 · simp [rowSign, h]155156private theorem mulVec_rowSign_apply157 {ι : Type u} [Fintype ι] [DecidableEq ι]158 (M : _root_.Matrix ι ι ℝ) (i : ι) :159 M.mulVec (rowSign M i) i = Matrix.rowL1Norm M i := by160 unfold _root_.Matrix.mulVec Matrix.rowL1Norm161 apply Finset.sum_congr rfl162 intro j _163 by_cases h : 0 ≤ M i j164 · simp [rowSign, h, abs_of_nonneg h]165 · have h' : M i j ≤ 0 := le_of_not_ge h166 simp [rowSign, h, abs_of_nonpos h']167168private theorem rowL1_stdMatrix_le_opNorm169 {ι : Type u} [Fintype ι] [DecidableEq ι]170 (A : (ι → ℝ) →L[ℝ] (ι → ℝ)) (i : ι) :171 Matrix.rowL1Norm (stdMatrix A) i ≤ ‖A‖ := by172 let σ : ι → ℝ := rowSign (stdMatrix A) i173 have hσ : ‖σ‖ ≤ 1 := norm_rowSign_le_one (stdMatrix A) i174 have hrow : Matrix.rowL1Norm (stdMatrix A) i = A σ i := by175 calc176 Matrix.rowL1Norm (stdMatrix A) i = (stdMatrix A).mulVec σ i :=177 (mulVec_rowSign_apply (stdMatrix A) i).symm178 _ = A σ i := congrFun (stdMatrix_mulVec A σ) i179 calc180 Matrix.rowL1Norm (stdMatrix A) i = A σ i := hrow181 _ ≤ |A σ i| := le_abs_self _182 _ = ‖A σ i‖ := (Real.norm_eq_abs _).symm183 _ ≤ ‖A σ‖ := norm_le_pi_norm (A σ) i184 _ ≤ ‖A‖ * ‖σ‖ := A.le_opNorm σ185 _ ≤ ‖A‖ * 1 := mul_le_mul_of_nonneg_left hσ (norm_nonneg A)186 _ = ‖A‖ := mul_one _187188private def rowsFrom {ι : Type u} [Fintype ι] [DecidableEq ι]189 (P Q : _root_.Matrix ι ι ℝ) (s : Finset ι) : _root_.Matrix ι ι ℝ :=190 fun i => if i ∈ s then P i else Q i191192@[simp] private theorem rowsFrom_apply_of_mem193 {ι : Type u} [Fintype ι] [DecidableEq ι]194 (P Q : _root_.Matrix ι ι ℝ) (s : Finset ι) {i : ι} (hi : i ∈ s) :195 rowsFrom P Q s i = P i := by196 simp [rowsFrom, hi]197198@[simp] private theorem rowsFrom_apply_of_not_mem199 {ι : Type u} [Fintype ι] [DecidableEq ι]200 (P Q : _root_.Matrix ι ι ℝ) (s : Finset ι) {i : ι} (hi : i ∉ s) :201 rowsFrom P Q s i = Q i := by202 simp [rowsFrom, hi]203204@[simp] private theorem rowsFrom_empty205 {ι : Type u} [Fintype ι] [DecidableEq ι]206 (P Q : _root_.Matrix ι ι ℝ) : rowsFrom P Q ∅ = Q := by207 ext i j208 simp [rowsFrom]209210@[simp] private theorem rowsFrom_univ211 {ι : Type u} [Fintype ι] [DecidableEq ι]212 (P Q : _root_.Matrix ι ι ℝ) : rowsFrom P Q Finset.univ = P := by213 ext i j214 simp [rowsFrom]215216private def oneRowDifference217 {ι : Type u} [Fintype ι] [DecidableEq ι]218 (P Q : _root_.Matrix ι ι ℝ) (s : Finset ι) (i : ι) :219 _root_.Matrix ι ι ℝ :=220 (rowsFrom P Q s).updateRow i (P i - Q i)221222private theorem det_rowsFrom_insert_sub223 {ι : Type u} [Fintype ι] [DecidableEq ι]224 (P Q : _root_.Matrix ι ι ℝ) (s : Finset ι) (i : ι) (hi : i ∉ s) :225 (rowsFrom P Q (insert i s)).det - (rowsFrom P Q s).det =226 (oneRowDifference P Q s i).det := by227 have hins : rowsFrom P Q (insert i s) =228 (rowsFrom P Q s).updateRow i (P i) := by229 ext r c230 by_cases hri : r = i231 · subst r232 simp [rowsFrom, hi, _root_.Matrix.updateRow]233 · simp [rowsFrom, _root_.Matrix.updateRow, hri]234 have hbase : (rowsFrom P Q s).updateRow i (Q i) = rowsFrom P Q s := by235 simpa [rowsFrom, hi] using236 _root_.Matrix.updateRow_eq_self (rowsFrom P Q s) i237 have hrow : P i = (P i - Q i) + Q i := by238 ext c239 simp240 rw [hins, hrow, _root_.Matrix.det_updateRow_add, hbase]241 simp [oneRowDifference]242243private theorem prod_le_pow_mul_of_distinguished244 {ι : Type u} [Fintype ι] [DecidableEq ι]245 (i : ι) (f : ι → ℝ) {S δ : ℝ}246 (hf : ∀ j, 0 ≤ f j) (_hS : 0 ≤ S) (hδ : 0 ≤ δ)247 (hi : f i ≤ δ) (hrest : ∀ j, j ≠ i → f j ≤ S) :248 (∏ j, f j) ≤ S ^ (Fintype.card ι - 1) * δ := by249 have hmem : i ∈ (Finset.univ : Finset ι) := Finset.mem_univ i250 calc251 (∏ j, f j) = f i * (Finset.univ.erase i).prod f := by252 symm253 exact Finset.mul_prod_erase (Finset.univ : Finset ι) f hmem254 _ ≤ δ * (Finset.univ.erase i).prod (fun _ => S) := by255 apply mul_le_mul hi256 · apply Finset.prod_le_prod257 · intro j _258 exact hf j259 · intro j hj260 exact hrest j (Finset.ne_of_mem_erase hj)261 · exact Finset.prod_nonneg fun j _ => hf j262 · exact hδ263 _ = δ * S ^ (Fintype.card ι - 1) := by264 congr 1265 rw [Finset.prod_const]266 congr 1267 simp268 _ = S ^ (Fintype.card ι - 1) * δ := mul_comm _ _269270private theorem abs_det_rowsFrom_insert_sub_le_max271 {ι : Type u} [Fintype ι] [DecidableEq ι]272 (P Q : (ι → ℝ) →L[ℝ] (ι → ℝ)) (s : Finset ι)273 (i : ι) (hi : i ∉ s) :274 |(rowsFrom (stdMatrix P) (stdMatrix Q) (insert i s)).det -275 (rowsFrom (stdMatrix P) (stdMatrix Q) s).det| ≤276 (max ‖P‖ ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖ := by277 rw [det_rowsFrom_insert_sub (stdMatrix P) (stdMatrix Q) s i hi]278 apply (Matrix.abs_det_le_prod_rowL1Norm _).trans279 apply prod_le_pow_mul_of_distinguished i280 · intro j281 unfold Matrix.rowL1Norm282 positivity283 · positivity284 · positivity285 · have h := rowL1_stdMatrix_le_opNorm (P - Q) i286 rw [stdMatrix_sub] at h287 simpa [oneRowDifference, Matrix.rowL1Norm, _root_.Matrix.updateRow] using h288 · intro j hji289 by_cases hjs : j ∈ s290 · simpa [oneRowDifference, Matrix.rowL1Norm, _root_.Matrix.updateRow,291 hji, rowsFrom, hjs] using292 (rowL1_stdMatrix_le_opNorm P j).trans (le_max_left _ _)293 · simpa [oneRowDifference, Matrix.rowL1Norm, _root_.Matrix.updateRow,294 hji, rowsFrom, hjs] using295 (rowL1_stdMatrix_le_opNorm Q j).trans (le_max_right _ _)296297private theorem abs_det_rowsFrom_sub_le_max298 {ι : Type u} [Fintype ι] [DecidableEq ι]299 (P Q : (ι → ℝ) →L[ℝ] (ι → ℝ)) (s : Finset ι) :300 |(rowsFrom (stdMatrix P) (stdMatrix Q) s).det - (stdMatrix Q).det| ≤301 (s.card : ℝ) * (max ‖P‖ ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖ := by302 classical303 induction s using Finset.induction_on with304 | empty => simp305 | @insert i s hi ih =>306 calc307 |(rowsFrom (stdMatrix P) (stdMatrix Q) (insert i s)).det -308 (stdMatrix Q).det| ≤309 |(rowsFrom (stdMatrix P) (stdMatrix Q) (insert i s)).det -310 (rowsFrom (stdMatrix P) (stdMatrix Q) s).det| +311 |(rowsFrom (stdMatrix P) (stdMatrix Q) s).det -312 (stdMatrix Q).det| := abs_sub_le _ _ _313 _ ≤ (max ‖P‖ ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖ +314 (s.card : ℝ) * (max ‖P‖ ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖ :=315 add_le_add (abs_det_rowsFrom_insert_sub_le_max P Q s i hi) ih316 _ = ((insert i s).card : ℝ) *317 (max ‖P‖ ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖ := by318 simp [hi]319 ring320321private theorem det_stdMatrix322 {ι : Type u} [Fintype ι] [DecidableEq ι]323 (A : (ι → ℝ) →L[ℝ] (ι → ℝ)) :324 (stdMatrix A).det = LinearMap.det (A : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)) := by325 rw [stdMatrix_eq_toMatrix']326 exact LinearMap.det_toMatrix' (A : (ι → ℝ) →ₗ[ℝ] (ι → ℝ))327328/-- Strong determinant difference estimate for finite Pi spaces with their sup norm. -/329theorem abs_det_sub_le_max330 {ι : Type u} [Fintype ι] [DecidableEq ι]331 (P Q : (ι → ℝ) →L[ℝ] (ι → ℝ)) :332 |LinearMap.det (P : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)) -333 LinearMap.det (Q : (ι → ℝ) →ₗ[ℝ] (ι → ℝ))| ≤334 (Fintype.card ι : ℝ) *335 (max ‖P‖ ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖ := by336 simpa [det_stdMatrix] using337 abs_det_rowsFrom_sub_le_max P Q (Finset.univ : Finset ι)338339/-- Source-compatible determinant difference estimate using `‖P‖ + ‖Q‖`. -/340theorem abs_det_sub_le341 {ι : Type u} [Fintype ι] [DecidableEq ι]342 (P Q : (ι → ℝ) →L[ℝ] (ι → ℝ)) :343 |LinearMap.det (P : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)) -344 LinearMap.det (Q : (ι → ℝ) →ₗ[ℝ] (ι → ℝ))| ≤345 (Fintype.card ι : ℝ) *346 (‖P‖ + ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖ := by347 calc348 |LinearMap.det (P : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)) -349 LinearMap.det (Q : (ι → ℝ) →ₗ[ℝ] (ι → ℝ))| ≤350 (Fintype.card ι : ℝ) *351 (max ‖P‖ ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖ :=352 abs_det_sub_le_max P Q353 _ ≤ (Fintype.card ι : ℝ) *354 (‖P‖ + ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖ := by355 have hmax : max ‖P‖ ‖Q‖ ≤ ‖P‖ + ‖Q‖ := by356 exact max_le357 (le_add_of_nonneg_right (norm_nonneg Q))358 (le_add_of_nonneg_left (norm_nonneg P))359 gcongr360361/-- Norm-valued form of `abs_det_sub_le`. -/362theorem norm_det_sub_le363 {ι : Type u} [Fintype ι] [DecidableEq ι]364 (P Q : (ι → ℝ) →L[ℝ] (ι → ℝ)) :365 ‖LinearMap.det (P : (ι → ℝ) →ₗ[ℝ] (ι → ℝ)) -366 LinearMap.det (Q : (ι → ℝ) →ₗ[ℝ] (ι → ℝ))‖ ≤367 (Fintype.card ι : ℝ) *368 (‖P‖ + ‖Q‖) ^ (Fintype.card ι - 1) * ‖P - Q‖ := by369 simpa only [Real.norm_eq_abs] using abs_det_sub_le P Q370371end ContinuousLinearMap372end MathlibAnnex