Exact source: MathlibAnnex/LinearAlgebra/Matrix/VolumeScaledMaximalMinor.lean
Pinned GitHub source · Raw UTF-8 source
Back to Compactness of the signed generator set
1import MathlibAnnex.LinearAlgebra.Matrix.MaximalMinor2import MathlibAnnex.MeasureTheory.Measure.EquivalentSeminormBall3import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd45/-!6# Maximal minors scaled by model ball volume78Rows use the increasing order fixed by `MaximalMinorIndex`. Pairing is the9ordinary real `dotProduct`, with no change of orientation or normalization.10-/1112noncomputable section1314namespace MathlibAnnex.Matrix1516open scoped BigOperators1718/-- The maximal-minor vector multiplied by the model ball's Lebesgue volume. -/19def ballVolumeScaledMaximalMinors {n N : ℕ}20 (M : EquivalentSeminorm (Fin n → ℝ))21 (A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ)) : MaximalMinorIndex n (Fin N) → ℝ :=22 M.closedUnitBallVolume • maximalMinors (LinearMap.toMatrix' A.toLinearMap)2324@[simp] theorem ballVolumeScaledMaximalMinors_zero_of_pos {n N : ℕ}25 (M : EquivalentSeminorm (Fin n → ℝ)) (hn : 0 < n) :26 ballVolumeScaledMaximalMinors M (0 : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ)) = 0 := by27 simp [ballVolumeScaledMaximalMinors, maximalMinors_zero_of_pos hn]2829theorem pairing_ballVolumeScaledMaximalMinors {n N : ℕ}30 (M : EquivalentSeminorm (Fin n → ℝ)) (w : MaximalMinorIndex n (Fin N) → ℝ)31 (A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ)) :32 dotProduct w (ballVolumeScaledMaximalMinors M A) =33 M.closedUnitBallVolume * dotProduct w (maximalMinors (LinearMap.toMatrix' A.toLinearMap)) := by34 simp only [dotProduct, ballVolumeScaledMaximalMinors, Pi.smul_apply, smul_eq_mul,35 Finset.mul_sum]36 apply Finset.sum_congr rfl37 intro i hi38 ring3940private theorem continuous_toMatrix' {n N : ℕ} :41 Continuous (fun A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ) =>42 LinearMap.toMatrix' A.toLinearMap) := by43 apply continuous_matrix44 intro i j45 change Continuous fun A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ) => A (Pi.single j 1) i46 fun_prop4748/-- Continuity of the volume-scaled maximal-minor vector. -/49theorem continuous_ballVolumeScaledMaximalMinors {n N : ℕ}50 (M : EquivalentSeminorm (Fin n → ℝ)) :51 Continuous (ballVolumeScaledMaximalMinors M :52 ((Fin n → ℝ) →L[ℝ] (Fin N → ℝ)) → (MaximalMinorIndex n (Fin N) → ℝ)) := by53 change Continuous fun A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ) =>54 M.closedUnitBallVolume • maximalMinors (LinearMap.toMatrix' A.toLinearMap)55 exact continuous_const.smul (continuous_maximalMinors.comp continuous_toMatrix')5657end MathlibAnnex.Matrix