diff --git a/LeanPool/GrothendieckBessel.lean b/LeanPool/GrothendieckBessel.lean new file mode 100644 index 0000000000..11765a46d0 --- /dev/null +++ b/LeanPool/GrothendieckBessel.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import LeanPool.GrothendieckBessel.MainTheorem + + +/-! +# Grothendieck's theorem for Bessel sequences + +Source: arxiv:2608.12280, url:https://github.com/lukasliehr/GrothendieckBessel/tree/f1ad1c7680bce2b1ab4218a02bddd694fb57062a +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +Status: verified +Main declarations: `GrothendieckBessel.main` +Tags: functional-analysis, bessel-sequences, gram-matrices +MSC: 46B15, 46B25, 46C05 +-/ + + + +/-! +# Countable Grothendieck--Bessel Gram representation, with proofs + +Proof-carrying counterpart to the declaration in `Showcase.lean`. +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + + +noncomputable section + +open MeasureTheory +open scoped BigOperators ComplexConjugate InnerProductSpace + +namespace GrothendieckBessel + +theorem main_withProof + (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] + (x : ℕ → H) (hx : BesselSequenceBoundOne x) : + ∃ f : ℕ → ℝ → ℂ, + (∀ j, AEStronglyMeasurable (f j) μ) ∧ + (∀ j t, t ∈ unitInterval → ‖f j t‖ ≤ 1) ∧ + ∀ j k, + ⟪x k, x j⟫_ℂ = + ∫ t in unitInterval, f j t * star (f k t) := by + exact main_proof H x hx + +/-- +Comparator-facing proved counterpart to `GrothendieckBessel.main` in +`Showcase.lean`. The existing `main_withProof` entry point is retained. +-/ +theorem main + (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] + (x : ℕ → H) (hx : BesselSequenceBoundOne x) : + ∃ f : ℕ → ℝ → ℂ, + (∀ j, AEStronglyMeasurable (f j) μ) ∧ + (∀ j t, t ∈ unitInterval → ‖f j t‖ ≤ 1) ∧ + ∀ j k, + ⟪x k, x j⟫_ℂ = + ∫ t in unitInterval, f j t * star (f k t) := by + exact main_withProof H x hx + +end GrothendieckBessel diff --git a/LeanPool/GrothendieckBessel/AbstractBessel.lean b/LeanPool/GrothendieckBessel/AbstractBessel.lean new file mode 100644 index 0000000000..91a957e9b1 --- /dev/null +++ b/LeanPool/GrothendieckBessel/AbstractBessel.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import LeanPool.GrothendieckBessel.Conventions + +import Mathlib.Tactic.NormNum + +/-! +# Abstract Bessel sequences and their Gram kernels +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + + +noncomputable section + +open scoped BigOperators ComplexConjugate + +namespace GrothendieckBessel + +universe u + +/-- The paper-convention Gram kernel of an abstract Hilbert-space sequence. -/ +def besselGram + {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] + (x : ℕ → H) : ℕ → ℕ → ℂ := + fun j k => inner ℂ (x k) (x j) + +/-- Conjugate symmetry of the abstract Gram kernel. -/ +theorem besselGram_conj_symm + {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] + (x : ℕ → H) : + ∀ j k, besselGram x k j = star (besselGram x j k) := by + intro j k + simp [besselGram] + +/-- The finite Gram quadratic form is the squared norm of the vector sum. -/ +theorem besselGram_quadratic_eq_norm_sq + {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] + (x : ℕ → H) (F : Finset ℕ) (c : ℕ → ℂ) : + (F.sum (fun j => F.sum (fun k => + c j * star (c k) * besselGram x j k))).re = + ‖F.sum (fun j => c j • x j)‖ ^ 2 := by + classical + have hcomplex : + F.sum (fun j => F.sum (fun k => + c j * star (c k) * besselGram x j k)) = + inner ℂ (F.sum (fun j => c j • x j)) + (F.sum (fun j => c j • x j)) := by + simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right] + rw [Finset.sum_comm] + simp [besselGram, mul_assoc, mul_comm, mul_left_comm] + rw [hcomplex, inner_self_eq_norm_sq_to_K] + norm_cast + +/-- A Bessel sequence with bound one has a finite positive-contraction Gram kernel. -/ +theorem besselGram_finite_positive_contraction + {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] + (x : ℕ → H) (hx : BesselSequenceBoundOne x) : + FiniteHermitianPositiveContraction (besselGram x) := by + constructor + · exact besselGram_conj_symm x + · intro F c + rw [besselGram_quadratic_eq_norm_sq x F c] + exact ⟨sq_nonneg _, hx F c⟩ + +end GrothendieckBessel diff --git a/LeanPool/GrothendieckBessel/BallProdromou.lean b/LeanPool/GrothendieckBessel/BallProdromou.lean new file mode 100644 index 0000000000..5273285144 --- /dev/null +++ b/LeanPool/GrothendieckBessel/BallProdromou.lean @@ -0,0 +1,1845 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import LeanPool.GrothendieckBessel.RealConvex +public import Mathlib.Analysis.InnerProductSpace.Dual +public import Mathlib.Analysis.InnerProductSpace.Trace +public import Mathlib.Analysis.LocallyConvex.Separation +public import Mathlib.LinearAlgebra.Dimension.Constructions +public import Mathlib.Analysis.Matrix.PosDef + +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring +import Mathlib.Tactic.Positivity + +/-! +# The Ball--Prodromou cube quadratic maximum +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + +noncomputable section + +open scoped BigOperators +open Set + +namespace OlevskiiGram + +/-- +A Parseval family spans the whole coordinate space. This is the frame identity +used in the Ball--Prodromou proof. +-/ +theorem parsevalFrame_span_top + {n ι : Type*} [Fintype n] [Fintype ι] + (u : ι → n → ℝ) + (hparseval : ∀ x : n → ℝ, ∀ i, + (∑ j, realDot x (u j) * u j i) = x i) : + Submodule.span ℝ (Set.range u) = ⊤ := by + apply le_antisymm le_top + intro x _hx + have hxsum : (∑ j, realDot x (u j) • u j) = x := by + ext i + simpa [Pi.smul_apply] using hparseval x i + rw [← hxsum] + exact Submodule.sum_mem _ fun j _ => + Submodule.smul_mem _ _ (Submodule.subset_span ⟨j, rfl⟩) + +/-- Parseval identity for the squared norm expressed using `realDot`. -/ +theorem parsevalFrame_realDot_self + {n ι : Type*} [Fintype n] [Fintype ι] + (u : ι → n → ℝ) + (hparseval : ∀ x : n → ℝ, ∀ i, + (∑ j, realDot x (u j) * u j i) = x i) + (x : n → ℝ) : + realDot x x = ∑ j, (realDot x (u j)) ^ 2 := by + calc + realDot x x + = ∑ i, x i * x i := by + rfl + _ = ∑ i, x i * (∑ j, realDot x (u j) * u j i) := by + apply Finset.sum_congr rfl + intro i _hi + rw [hparseval x i] + _ = ∑ i, ∑ j, x i * (realDot x (u j) * u j i) := by + simp [Finset.mul_sum] + _ = ∑ j, ∑ i, x i * (realDot x (u j) * u j i) := by + rw [Finset.sum_comm] + _ = ∑ j, realDot x (u j) * realDot x (u j) := by + apply Finset.sum_congr rfl + intro j _hj + simp [realDot, Finset.mul_sum, mul_comm, mul_left_comm] + _ = ∑ j, (realDot x (u j)) ^ 2 := by + simp [pow_two] + +/-- +If the active constraints span the whole coordinate space, then at least +`dim` constraints are active. +-/ +theorem activeConstraintCount_ge_card_of_span_top + {n ι : Type*} [Fintype n] [Fintype ι] + (u : ι → n → ℝ) (x : n → ℝ) + (hspan : activeConstraintSpan u x = ⊤) : + Fintype.card n ≤ activeConstraintCount u x := by + classical + let s : Finset ι := activeConstraintIndexSet u x + let vset : Finset (n → ℝ) := s.image u + have hactive_eq : activeConstraintVectors u x = (vset : Set (n → ℝ)) := by + ext v + constructor + · rintro ⟨j, rfl, hj⟩ + exact Finset.mem_coe.mpr + (Finset.mem_image.mpr + ⟨j, by simpa [s] using (mem_activeConstraintIndexSet_iff u x j).mpr hj, rfl⟩) + · intro hv + rcases Finset.mem_image.mp (Finset.mem_coe.mp hv) with ⟨j, hj, rfl⟩ + exact ⟨j, rfl, (mem_activeConstraintIndexSet_iff u x j).mp (by simpa [s] using hj)⟩ + have hfinrank : + Module.finrank ℝ (n → ℝ) ≤ vset.card := by + calc + Module.finrank ℝ (n → ℝ) + = Module.finrank ℝ (activeConstraintSpan u x) := by + rw [hspan, finrank_top] + _ = Module.finrank ℝ (Submodule.span ℝ (vset : Set (n → ℝ))) := by + rw [activeConstraintSpan, hactive_eq] + _ ≤ vset.card := by + simpa [Set.finrank] using + (finrank_span_finset_le_card (R := ℝ) vset) + calc + Fintype.card n = Module.finrank ℝ (n → ℝ) := by + rw [Module.finrank_fintype_fun_eq_card] + _ ≤ vset.card := hfinrank + _ ≤ s.card := Finset.card_image_le + _ = activeConstraintCount u x := by + simp [activeConstraintCount, s] + +/-- On the active set, the squared frame coefficients sum to the active count. -/ +theorem activeConstraint_sum_sq_eq_count + {n ι : Type*} [Fintype n] [Fintype ι] + (u : ι → n → ℝ) (x : n → ℝ) : + (∑ j ∈ activeConstraintIndexSet u x, (realDot x (u j)) ^ 2) = + (activeConstraintCount u x : ℝ) := by + classical + calc + (∑ j ∈ activeConstraintIndexSet u x, (realDot x (u j)) ^ 2) + = ∑ j ∈ activeConstraintIndexSet u x, (1 : ℝ) := by + apply Finset.sum_congr rfl + intro j hj + have hactive := (mem_activeConstraintIndexSet_iff u x j).mp hj + calc + (realDot x (u j)) ^ 2 = |realDot x (u j)| ^ 2 := by + rw [sq_abs] + _ = 1 := by + rw [hactive] + norm_num + _ = (activeConstraintCount u x : ℝ) := by + simp [activeConstraintCount] + +/-- +The norm-lower step in Ball--Prodromou: a Parseval family and a point whose +active constraints span force `dim ≤ ‖x‖²`. +-/ +theorem parsevalFrame_active_norm_lower + {n ι : Type*} [Fintype n] [Fintype ι] + (u : ι → n → ℝ) + (hparseval : ∀ x : n → ℝ, ∀ i, + (∑ j, realDot x (u j) * u j i) = x i) + (x : n → ℝ) + (hspan : activeConstraintSpan u x = ⊤) : + (Fintype.card n : ℝ) ≤ realDot x x := by + classical + have hcount_nat : Fintype.card n ≤ activeConstraintCount u x := + activeConstraintCount_ge_card_of_span_top u x hspan + have hcount : (Fintype.card n : ℝ) ≤ (activeConstraintCount u x : ℝ) := by + exact_mod_cast hcount_nat + have hactive_sum : + (∑ j ∈ activeConstraintIndexSet u x, (realDot x (u j)) ^ 2) = + (activeConstraintCount u x : ℝ) := + activeConstraint_sum_sq_eq_count u x + have hsubset_sum : + (∑ j ∈ activeConstraintIndexSet u x, (realDot x (u j)) ^ 2) ≤ + ∑ j, (realDot x (u j)) ^ 2 := by + exact Finset.sum_le_univ_sum_of_nonneg fun j => sq_nonneg (realDot x (u j)) + calc + (Fintype.card n : ℝ) ≤ (activeConstraintCount u x : ℝ) := hcount + _ = ∑ j ∈ activeConstraintIndexSet u x, (realDot x (u j)) ^ 2 := hactive_sum.symm + _ ≤ ∑ j, (realDot x (u j)) ^ 2 := hsubset_sum + _ = realDot x x := (parsevalFrame_realDot_self u hparseval x).symm + +/-- +Existence form of the Ball--Prodromou norm-lower step. This is obtained from +the active-constraint maximizer already proved in `RealConvex.lean`. +-/ +theorem exists_parseval_polytope_point_norm_ge_card + {n ι : Type*} [Fintype n] [Fintype ι] + (u : ι → n → ℝ) + (hparseval : ∀ x : n → ℝ, ∀ i, + (∑ j, realDot x (u j) * u j i) = x i) : + ∃ w : n → ℝ, + (∀ j, |realDot w (u j)| ≤ 1) ∧ + (Fintype.card n : ℝ) ≤ realDot w w := by + classical + have hspan : Submodule.span ℝ (Set.range u) = ⊤ := + parsevalFrame_span_top u hparseval + have hconv : + ConvexOn ℝ (constraintPolytope u) (fun _ : n → ℝ => (0 : ℝ)) := + convexOn_const (0 : ℝ) (constraintPolytope_convex u) + rcases activeConstraintMaximizer u (fun _ : n → ℝ => (0 : ℝ)) + hspan continuous_const hconv with + ⟨w, hwpoly, _hwmax, hwactive⟩ + exact ⟨w, hwpoly, parsevalFrame_active_norm_lower u hparseval w hwactive⟩ + +/-- Weighted diagonal quadratic form used for the Ball--Prodromou functions `Φ_m`. -/ +def weightedSquareSum {n : Type*} [Fintype n] (c : n → ℝ) (x : n → ℝ) : ℝ := + ∑ i, c i * x i ^ 2 + +/-- The finite weighted diagonal quadratic form is continuous. -/ +theorem continuous_weightedSquareSum + {n : Type*} [Fintype n] (c : n → ℝ) : + Continuous (weightedSquareSum c) := by + unfold weightedSquareSum + fun_prop + +/-- A weighted diagonal quadratic form with nonnegative weights is convex. -/ +theorem convexOn_weightedSquareSum_nonneg + {n : Type*} [Fintype n] (c : n → ℝ) + (hc : ∀ i, 0 ≤ c i) : + ConvexOn ℝ Set.univ (weightedSquareSum c) := by + refine ⟨convex_univ, ?_⟩ + intro x _hx y _hy a b ha hb hab + unfold weightedSquareSum + calc + (∑ i, c i * (a • x + b • y) i ^ 2) + ≤ ∑ i, (a * (c i * x i ^ 2) + b * (c i * y i ^ 2)) := by + apply Finset.sum_le_sum + intro i _hi + have hsq : + (a * x i + b * y i) ^ 2 ≤ a * x i ^ 2 + b * y i ^ 2 := by + have hnonneg : 0 ≤ a * b * (x i - y i) ^ 2 := + mul_nonneg (mul_nonneg ha hb) (sq_nonneg _) + nlinarith + change c i * (a * x i + b * y i) ^ 2 ≤ + a * (c i * x i ^ 2) + b * (c i * y i ^ 2) + calc + c i * (a * x i + b * y i) ^ 2 + ≤ c i * (a * x i ^ 2 + b * y i ^ 2) := + mul_le_mul_of_nonneg_left hsq (hc i) + _ = a * (c i * x i ^ 2) + b * (c i * y i ^ 2) := by + ring + _ = a * (∑ i, c i * x i ^ 2) + b * (∑ i, c i * y i ^ 2) := by + rw [Finset.sum_add_distrib, Finset.mul_sum, Finset.mul_sum] + +/-- +The same convexity statement restricted to a constraint polytope, in the exact +shape needed by `activeConstraintMaximizer`. +-/ +theorem convexOn_constraintPolytope_weightedSquareSum_nonneg + {n ι : Type*} [Fintype n] + (u : ι → n → ℝ) (c : n → ℝ) + (hc : ∀ i, 0 ≤ c i) : + ConvexOn ℝ (constraintPolytope u) (weightedSquareSum c) := + (convexOn_weightedSquareSum_nonneg c hc).subset + (Set.subset_univ _) (constraintPolytope_convex u) + +/-- +For a Parseval family, every nonnegative weighted diagonal quadratic has a +maximizer on the constraint polytope whose active constraints span and whose +norm has the Ball--Prodromou lower bound. +-/ +theorem exists_parseval_weightedSquareSum_maximizer + {n ι : Type*} [Fintype n] [Fintype ι] + (u : ι → n → ℝ) + (hparseval : ∀ x : n → ℝ, ∀ i, + (∑ j, realDot x (u j) * u j i) = x i) + (c : n → ℝ) (hc : ∀ i, 0 ≤ c i) : + ∃ w : n → ℝ, + w ∈ constraintPolytope u ∧ + (∀ y : n → ℝ, y ∈ constraintPolytope u → + weightedSquareSum c y ≤ weightedSquareSum c w) ∧ + activeConstraintSpan u w = ⊤ ∧ + (Fintype.card n : ℝ) ≤ realDot w w := by + classical + have hspan : Submodule.span ℝ (Set.range u) = ⊤ := + parsevalFrame_span_top u hparseval + rcases activeConstraintMaximizer u (weightedSquareSum c) + hspan (continuous_weightedSquareSum c) + (convexOn_constraintPolytope_weightedSquareSum_nonneg u c hc) with + ⟨w, hwpoly, hwmax, hwactive⟩ + exact ⟨w, hwpoly, hwmax, hwactive, + parsevalFrame_active_norm_lower u hparseval w hwactive⟩ + +/-- +The coefficient vector for the Ball--Prodromou functional +`Φ_m(x) = ∑_{i if (i : ℕ) < m then s i - s m else 0 + +/-- The Ball--Prodromou coefficient vector is nonnegative under eigenvalue monotonicity. -/ +theorem bpPhiWeights_nonneg + (s : ℕ → ℝ) (m : ℕ) + (hmono : ∀ i : ℕ, i < m → s m ≤ s i) : + ∀ i, 0 ≤ bpPhiWeights s m i := by + intro i + by_cases hi : (i : ℕ) < m + · simp [bpPhiWeights, hi, sub_nonneg.mpr (hmono i hi)] + · simp [bpPhiWeights, hi] + +/-- The last coefficient in `bpPhiWeights` is zero. -/ +theorem bpPhiWeights_last (s : ℕ → ℝ) (m : ℕ) : + bpPhiWeights s m ⟨m, Nat.lt_succ_self m⟩ = 0 := by + simp [bpPhiWeights] + +/-- A coefficient before the last index has the expected spectral-gap value. -/ +theorem bpPhiWeights_of_lt + (s : ℕ → ℝ) {i m : ℕ} (hi : i < m) : + bpPhiWeights s m ⟨i, Nat.lt_trans hi (Nat.lt_succ_self m)⟩ = s i - s m := by + simp [bpPhiWeights, hi] + +/-- +The active-constraint maximizer specialized to the Ball--Prodromou functional +on `Fin (m+1)`. +-/ +theorem exists_bpPhiMaximizer + {ι : Type*} [Fintype ι] + (u : ι → Fin (m + 1) → ℝ) + (hparseval : ∀ x : Fin (m + 1) → ℝ, ∀ i, + (∑ j, realDot x (u j) * u j i) = x i) + (s : ℕ → ℝ) + (hmono : ∀ i : ℕ, i < m → s m ≤ s i) : + ∃ w : Fin (m + 1) → ℝ, + w ∈ constraintPolytope u ∧ + (∀ y : Fin (m + 1) → ℝ, y ∈ constraintPolytope u → + weightedSquareSum (bpPhiWeights s m) y ≤ + weightedSquareSum (bpPhiWeights s m) w) ∧ + activeConstraintSpan u w = ⊤ ∧ + ((m + 1 : ℕ) : ℝ) ≤ realDot w w := by + classical + rcases exists_parseval_weightedSquareSum_maximizer u hparseval + (bpPhiWeights s m) (bpPhiWeights_nonneg s m hmono) with + ⟨w, hwpoly, hwmax, hwactive, hnorm⟩ + refine ⟨w, hwpoly, hwmax, hwactive, ?_⟩ + simpa using hnorm + +/-- Coordinate form of `realDot x x` on `Fin n`. -/ +theorem realDot_self_fin_eq_sum_univ {n : ℕ} (x : Fin n → ℝ) : + realDot x x = ∑ i : Fin n, x i ^ 2 := by + simp [realDot, pow_two] + +/-- `bpPhiWeights` turns `weightedSquareSum` into the expected prefix sum. -/ +theorem weightedSquareSum_bpPhiWeights + (s : ℕ → ℝ) (m : ℕ) (x : Fin (m + 1) → ℝ) : + weightedSquareSum (bpPhiWeights s m) x = + ∑ i : Fin m, + (s i - s m) * x i.castSucc ^ 2 := by + unfold weightedSquareSum + rw [Fin.sum_univ_castSucc] + simp [bpPhiWeights] + +/-- Drop the last coordinate from each constraint vector. -/ +def dropLastConstraints {ι : Type*} {m : ℕ} + (u : ι → Fin (m + 1) → ℝ) : ι → Fin m → ℝ := + fun j i => u j i.castSucc + +/-- Extend a vector by a zero final coordinate. -/ +def extendByZero {m : ℕ} (x : Fin m → ℝ) : Fin (m + 1) → ℝ := + Fin.snoc x 0 + +@[simp] +theorem extendByZero_castSucc {m : ℕ} (x : Fin m → ℝ) (i : Fin m) : + extendByZero x i.castSucc = x i := by + simp [extendByZero] + +@[simp] +theorem extendByZero_last {m : ℕ} (x : Fin m → ℝ) : + extendByZero x (Fin.last m) = 0 := by + simp [extendByZero] + +/-- The previous Ball--Prodromou functional evaluated on a zero-extension. -/ +theorem weightedSquareSum_bpPhiWeights_extendByZero + (s : ℕ → ℝ) (m : ℕ) (x : Fin m → ℝ) : + weightedSquareSum (bpPhiWeights s m) (extendByZero x) = + ∑ i : Fin m, (s i - s m) * x i ^ 2 := by + rw [weightedSquareSum_bpPhiWeights] + simp + +/-- +The dot product of a zero-extension with a full constraint vector is the dot +product against the truncated constraint vector. +-/ +theorem realDot_extendByZero_dropLastConstraints + {ι : Type*} {m : ℕ} + (u : ι → Fin (m + 1) → ℝ) (x : Fin m → ℝ) (j : ι) : + realDot (extendByZero x) (u j) = + realDot x (dropLastConstraints u j) := by + unfold realDot dropLastConstraints + rw [Fin.sum_univ_castSucc] + simp + +/-- Truncating the final coordinate preserves the Parseval identity. -/ +theorem parseval_dropLastConstraints + {ι : Type*} [Fintype ι] {m : ℕ} + (u : ι → Fin (m + 1) → ℝ) + (hparseval : ∀ x : Fin (m + 1) → ℝ, ∀ i, + (∑ j, realDot x (u j) * u j i) = x i) : + ∀ x : Fin m → ℝ, ∀ i, + (∑ j, realDot x (dropLastConstraints u j) * + dropLastConstraints u j i) = x i := by + intro x i + have h := hparseval (extendByZero x) i.castSucc + simpa [dropLastConstraints, realDot_extendByZero_dropLastConstraints u x] using h + +/-- +The TeX inclusion `C_{m-1} ⊆ C_m`: a feasible point for the truncated +constraints remains feasible after adding a zero last coordinate. +-/ +theorem extendByZero_mem_constraintPolytope + {ι : Type*} {m : ℕ} + (u : ι → Fin (m + 1) → ℝ) {x : Fin m → ℝ} + (hx : x ∈ constraintPolytope (dropLastConstraints u)) : + extendByZero x ∈ constraintPolytope u := by + intro j + simpa [realDot_extendByZero_dropLastConstraints] using hx j + +/-- +The maximizer comparison used in the Ball--Prodromou induction: a maximizer on +`C_m` dominates the zero-extension of any feasible point from `C_{m-1}`. +-/ +theorem bpPhi_maximizer_comparison_dropLast + {ι : Type*} {m : ℕ} + (u : ι → Fin (m + 1) → ℝ) (s : ℕ → ℝ) + {wCur : Fin (m + 1) → ℝ} {wPrev : Fin m → ℝ} + (hmax : ∀ y : Fin (m + 1) → ℝ, y ∈ constraintPolytope u → + weightedSquareSum (bpPhiWeights s m) y ≤ + weightedSquareSum (bpPhiWeights s m) wCur) + (hPrev : wPrev ∈ constraintPolytope (dropLastConstraints u)) : + weightedSquareSum (bpPhiWeights s m) (extendByZero wPrev) ≤ + weightedSquareSum (bpPhiWeights s m) wCur := + hmax (extendByZero wPrev) (extendByZero_mem_constraintPolytope u hPrev) + +/-- +The same comparison in explicit coordinate-sum form: +`∑_{i + have hmono0 : ∀ i : ℕ, i < 0 → s 0 ≤ s i := by + intro i hi + exact False.elim (Nat.not_lt_zero i hi) + rcases exists_bpPhiMaximizer u hparseval s hmono0 with + ⟨w, hwpoly, _hwmax, _hwactive, hnorm⟩ + refine ⟨w, hwpoly, ?_⟩ + have hnormsum : (((0 : ℕ) : ℝ) + 1) ≤ ∑ i : Fin (0 + 1), w i ^ 2 := by + simpa [realDot_self_fin_eq_sum_univ] using hnorm + have hgap : 0 ≤ s 0 - s 1 := sub_nonneg.mpr (hanti (Nat.zero_le 1)) + have hmaxEmpty : + (∑ i : Fin 0, (s i - s 0) * (fun _ : Fin 0 => (0 : ℝ)) i ^ 2) ≤ + ∑ i : Fin 0, (s i - s 0) * w i.castSucc ^ 2 := by + simp + have hprevEmpty : + (∑ i : Fin 0, (s i - s 0)) ≤ + ∑ i : Fin 0, (s i - s 0) * (fun _ : Fin 0 => (0 : ℝ)) i ^ 2 := by + simp + simpa using + bp_induction_step_fin s (fun _ : Fin 0 => (0 : ℝ)) w + hmaxEmpty hprevEmpty hnormsum hgap + | succ m ih => + have hprevParseval : + ∀ x : Fin (m + 1) → ℝ, ∀ i, + (∑ j, realDot x (dropLastConstraints u j) * + dropLastConstraints u j i) = x i := + parseval_dropLastConstraints u hparseval + rcases ih (dropLastConstraints u) hprevParseval with + ⟨wPrev, hwPrevPoly, hprev⟩ + have hmono : ∀ i : ℕ, i < m + 1 → s (m + 1) ≤ s i := by + intro i hi + exact hanti (Nat.le_of_lt hi) + rcases exists_bpPhiMaximizer u hparseval s hmono with + ⟨wCur, hwCurPoly, hwCurMax, _hwCurActive, hCurNorm⟩ + refine ⟨wCur, hwCurPoly, ?_⟩ + have hmaxsum : + (∑ i : Fin (m + 1), (s i - s (m + 1)) * wPrev i ^ 2) ≤ + ∑ i : Fin (m + 1), + (s i - s (m + 1)) * wCur i.castSucc ^ 2 := + bpPhi_maximizer_comparison_dropLast_sum u s + (wCur := wCur) (wPrev := wPrev) hwCurMax hwPrevPoly + have hnormsum : + (((m + 1 : ℕ) : ℝ) + 1) ≤ + ∑ i : Fin ((m + 1) + 1), wCur i ^ 2 := by + simpa [realDot_self_fin_eq_sum_univ] using hCurNorm + have hgap : 0 ≤ s (m + 1) - s ((m + 1) + 1) := + sub_nonneg.mpr (hanti (Nat.le_succ (m + 1))) + simpa [Nat.succ_eq_add_one, add_assoc] using + bp_induction_step_fin s wPrev wCur hmaxsum hprev hnormsum hgap + +/-- +Diagonal Ball--Prodromou theorem in coordinates. + +This is the core of the paper's Ball--Prodromou proof after choosing an +orthonormal eigenbasis and setting the next eigenvalue to zero. +-/ +theorem ballProdromou_diagonal + {ι : Type*} [Fintype ι] (m : ℕ) + (u : ι → Fin (m + 1) → ℝ) + (hparseval : ∀ x : Fin (m + 1) → ℝ, ∀ i, + (∑ j, realDot x (u j) * u j i) = x i) + (s : ℕ → ℝ) + (hanti : ∀ {i k : ℕ}, i ≤ k → s k ≤ s i) + (hs_last : s (m + 1) = 0) : + ∃ w : Fin (m + 1) → ℝ, + w ∈ constraintPolytope u ∧ + (∑ i : Fin (m + 1), s i) ≤ + ∑ i : Fin (m + 1), s i * w i ^ 2 := by + rcases exists_bpInductionWitness m u hparseval s hanti with + ⟨w, hwpoly, hineq⟩ + refine ⟨w, hwpoly, ?_⟩ + simpa [hs_last] using hineq + +/-- +The spectral-coordinate data needed to turn the diagonal Ball--Prodromou theorem +into the cube quadratic maximum. + +In the paper this data comes from the positive spectral subspace of a symmetric +matrix `A`: `u j` are the coordinates of the projected standard basis vectors, +`s` is the decreasing eigenvalue list with one terminal zero, and `τ` is the +trace of the positive part. +-/ +def HasBallProdromouDiagonalModel + {d : Type*} [Fintype d] (A : Matrix d d ℝ) (τ : ℝ) : Prop := + ∃ (m : ℕ) (u : d → Fin (m + 1) → ℝ) (s : ℕ → ℝ), + (∀ x : Fin (m + 1) → ℝ, ∀ i, + (∑ j, realDot x (u j) * u j i) = x i) ∧ + (∀ {i k : ℕ}, i ≤ k → s k ≤ s i) ∧ + s (m + 1) = 0 ∧ + τ = ∑ i : Fin (m + 1), s i ∧ + ∀ w : Fin (m + 1) → ℝ, + realQuadraticForm A (fun j => realDot w (u j)) = + ∑ i : Fin (m + 1), s i * w i ^ 2 + +/-- +Ball--Prodromou implies the cube quadratic maximum once the positive spectral +subspace has been expressed in diagonal coordinates. +-/ +theorem cubeQuadraticMaximum_from_diagonalBP + {d : Type*} [Fintype d] (A : Matrix d d ℝ) (τ : ℝ) + (hmodel : HasBallProdromouDiagonalModel A τ) : + ∃ x : d → ℝ, InRealUnitCube x ∧ τ ≤ realQuadraticForm A x := by + classical + rcases hmodel with + ⟨m, u, s, hparseval, hanti, hs_last, htrace, hquad⟩ + rcases ballProdromou_diagonal m u hparseval s hanti hs_last with + ⟨w, hwpoly, hineq⟩ + let x : d → ℝ := fun j => realDot w (u j) + refine ⟨x, ?_, ?_⟩ + · intro j + exact hwpoly j + · calc + τ = ∑ i : Fin (m + 1), s i := htrace + _ ≤ ∑ i : Fin (m + 1), s i * w i ^ 2 := hineq + _ = realQuadraticForm A x := (hquad w).symm + +/-- +For a fixed symmetric test matrix, the positive-part support-function bound and +the Ball--Prodromou diagonal model give the support inequality needed for the +convex-hull separation argument. +-/ +theorem supportInequality_from_diagonalBP + {d : Type*} [Fintype d] [DecidableEq d] + (A Apos : Matrix d d ℝ) + (hsupport : HasPositivePartSupportFunction A Apos) + (hmodel : HasBallProdromouDiagonalModel A Apos.trace) : + ∃ x : d → ℝ, + InRealUnitCube x ∧ + ∀ G : Matrix d d ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ realQuadraticForm A x := by + rcases cubeQuadraticMaximum_from_diagonalBP A Apos.trace hmodel with + ⟨x, hcube, hx⟩ + refine ⟨x, hcube, ?_⟩ + intro G hGsym hG + exact (hsupport.1 G hGsym hG).trans hx + +/-- Ambient vector represented by coordinates in an orthonormal row system. -/ +def ambientOfEigenCoordinates + {d : Type*} {m : ℕ} + (v : Fin (m + 1) → d → ℝ) (w : Fin (m + 1) → ℝ) : d → ℝ := + fun j => ∑ i, w i * v i j + +/-- Constraint vectors obtained from rows of an ambient orthonormal system. -/ +def coordinateConstraintVectors + {d : Type*} {m : ℕ} + (v : Fin (m + 1) → d → ℝ) : d → Fin (m + 1) → ℝ := + fun j i => v i j + +/-- The project coordinate dot product agrees with the Euclidean inner product. -/ +theorem realDot_euclidean_eq_inner + {d : Type*} [Fintype d] + (x y : EuclideanSpace ℝ d) : + realDot (fun i => x i) (fun i => y i) = inner ℝ x y := by + simp [realDot, EuclideanSpace.inner_eq_star_dotProduct, dotProduct, mul_comm] + +/-- Coordinate form of the matrix action `A.toEuclideanLin`. -/ +theorem toEuclideanLin_apply_eq_sum + {d : Type*} [Fintype d] [DecidableEq d] + (A : Matrix d d ℝ) (x : EuclideanSpace ℝ d) (i : d) : + (A.toEuclideanLin x) i = ∑ j, A i j * x j := by + have h := congrFun (Matrix.ofLp_toLpLin (p := 2) (q := 2) A x) i + simp [Matrix.toLin'_apply, Matrix.mulVec, dotProduct] at h ⊢ + +/-- Coordinate quadratic forms are Euclidean inner products against `A.toEuclideanLin`. -/ +theorem realQuadraticForm_euclidean_eq_inner + {d : Type*} [Fintype d] [DecidableEq d] + (A : Matrix d d ℝ) (x : EuclideanSpace ℝ d) : + realQuadraticForm A (fun i => x i) = inner ℝ x (A.toEuclideanLin x) := by + calc + realQuadraticForm A (fun i => x i) + = ∑ i, x i * (A.toEuclideanLin x) i := by + apply Finset.sum_congr rfl + intro i _hi + rw [toEuclideanLin_apply_eq_sum A x i] + _ = realDot (fun i => x i) (fun i => (A.toEuclideanLin x) i) := by + rfl + _ = inner ℝ x (A.toEuclideanLin x) := + realDot_euclidean_eq_inner x (A.toEuclideanLin x) + +/-- +The projected standard-basis vectors form a Parseval family when the coordinate +rows are orthonormal. +-/ +theorem parseval_coordinateConstraintVectors + {d : Type*} [Fintype d] {m : ℕ} + (v : Fin (m + 1) → d → ℝ) + (horth : ∀ i k, realDot (v i) (v k) = if i = k then 1 else 0) : + ∀ x : Fin (m + 1) → ℝ, ∀ i, + (∑ j, realDot x (coordinateConstraintVectors v j) * + coordinateConstraintVectors v j i) = x i := by + classical + intro x i + calc + (∑ j, realDot x (coordinateConstraintVectors v j) * + coordinateConstraintVectors v j i) + = ∑ j, ∑ k, (x k * v k j) * v i j := by + simp [coordinateConstraintVectors, realDot, Finset.sum_mul] + _ = ∑ k, ∑ j, (x k * v k j) * v i j := by + rw [Finset.sum_comm] + _ = ∑ k, x k * realDot (v k) (v i) := by + apply Finset.sum_congr rfl + intro k _hk + simp [realDot, Finset.mul_sum, mul_assoc] + _ = ∑ k, x k * (if k = i then 1 else 0) := by + simp [horth] + _ = x i := by + simp + +/-- +If the rows are orthonormal eigenvectors of `A`, then the quadratic form of `A` +is diagonal on their span. +-/ +theorem realQuadraticForm_ambientOfEigenCoordinates + {d : Type*} [Fintype d] {m : ℕ} + (A : Matrix d d ℝ) (v : Fin (m + 1) → d → ℝ) (s : ℕ → ℝ) + (horth : ∀ i k, realDot (v i) (v k) = if i = k then 1 else 0) + (heigen : ∀ r j, (∑ k, A j k * v r k) = s r * v r j) + (w : Fin (m + 1) → ℝ) : + realQuadraticForm A (ambientOfEigenCoordinates v w) = + ∑ r : Fin (m + 1), s r * w r ^ 2 := by + classical + have hmul : + ∀ j, (∑ k, A j k * (∑ t, w t * v t k)) = + ∑ t, w t * (s t * v t j) := by + intro j + calc + (∑ k, A j k * (∑ t, w t * v t k)) + = ∑ k, ∑ t, A j k * (w t * v t k) := by + simp [Finset.mul_sum] + _ = ∑ t, ∑ k, A j k * (w t * v t k) := by + rw [Finset.sum_comm] + _ = ∑ t, w t * (∑ k, A j k * v t k) := by + apply Finset.sum_congr rfl + intro t _ht + calc + (∑ k, A j k * (w t * v t k)) + = ∑ k, w t * (A j k * v t k) := by + apply Finset.sum_congr rfl + intro k _hk + ring + _ = w t * (∑ k, A j k * v t k) := by + rw [Finset.mul_sum] + _ = ∑ t, w t * (s t * v t j) := by + simp [heigen] + have hexpand : + (∑ j, (∑ r, w r * v r j) * + (∑ t, w t * (s t * v t j))) = + ∑ r, ∑ t, w r * (w t * s t) * realDot (v r) (v t) := by + calc + (∑ j, (∑ r, w r * v r j) * + (∑ t, w t * (s t * v t j))) + = ∑ j, ∑ t, ∑ r, + (w r * v r j) * (w t * (s t * v t j)) := by + simp [Finset.sum_mul, Finset.mul_sum] + _ = ∑ j, ∑ r, ∑ t, + (w r * v r j) * (w t * (s t * v t j)) := by + apply Finset.sum_congr rfl + intro j _hj + rw [Finset.sum_comm] + _ = ∑ r, ∑ t, ∑ j, + (w r * v r j) * (w t * (s t * v t j)) := by + rw [Finset.sum_comm] + apply Finset.sum_congr rfl + intro r _hr + rw [Finset.sum_comm] + _ = ∑ r, ∑ t, w r * (w t * s t) * realDot (v r) (v t) := by + apply Finset.sum_congr rfl + intro r _hr + apply Finset.sum_congr rfl + intro t _ht + simp [realDot, Finset.mul_sum, mul_comm, mul_left_comm] + unfold realQuadraticForm ambientOfEigenCoordinates + calc + (∑ j, (∑ r, w r * v r j) * + ∑ k, A j k * (∑ t, w t * v t k)) + = ∑ j, (∑ r, w r * v r j) * + (∑ t, w t * (s t * v t j)) := by + apply Finset.sum_congr rfl + intro j _hj + rw [hmul j] + _ = ∑ r, ∑ t, w r * (w t * s t) * realDot (v r) (v t) := hexpand + _ = ∑ r : Fin (m + 1), s r * w r ^ 2 := by + simp [horth, pow_two, mul_comm, mul_left_comm] + +/-- +Explicit finite-dimensional spectral-coordinate data sufficient for the +Ball--Prodromou diagonal model. +-/ +def HasPositiveEigenCoordinateData + {d : Type*} [Fintype d] (A : Matrix d d ℝ) (τ : ℝ) : Prop := + ∃ (m : ℕ) (v : Fin (m + 1) → d → ℝ) (s : ℕ → ℝ), + (∀ i k, realDot (v i) (v k) = if i = k then 1 else 0) ∧ + (∀ r j, (∑ k, A j k * v r k) = s r * v r j) ∧ + (∀ {i k : ℕ}, i ≤ k → s k ≤ s i) ∧ + s (m + 1) = 0 ∧ + τ = ∑ i : Fin (m + 1), s i + +/-- +For a positive semidefinite real symmetric matrix indexed by `Fin (m+1)`, +Mathlib's Hermitian spectral theorem supplies the explicit eigen-coordinate data +needed by the Ball--Prodromou diagonal model. +-/ +theorem hasPositiveEigenCoordinateData_of_realPSD_fin + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) (hPSD : RealPSD A) + (hantiEig : Antitone (realSymmetric_isHermitian A hSym).eigenvalues) : + HasPositiveEigenCoordinateData A A.trace := by + classical + have hHerm : A.IsHermitian := realSymmetric_isHermitian A hSym + have hPos : A.PosSemidef := realPSD_posSemidef A hSym hPSD + let v : Fin (m + 1) → Fin (m + 1) → ℝ := + fun i => ⇑(hHerm.eigenvectorBasis i) + let s : ℕ → ℝ := + fun k => if hk : k ≤ m then hHerm.eigenvalues ⟨k, Nat.lt_succ_of_le hk⟩ else 0 + refine ⟨m, v, s, ?_, ?_, ?_, ?_, ?_⟩ + · intro i k + have horth := (orthonormal_iff_ite.mp hHerm.eigenvectorBasis.orthonormal) i k + simpa [v, realDot, EuclideanSpace.inner_eq_star_dotProduct, dotProduct, + mul_comm] using horth + · intro r j + have h := congrFun (hHerm.mulVec_eigenvectorBasis r) j + have hr : (r : ℕ) ≤ m := Nat.lt_succ_iff.mp r.isLt + simpa [v, s, hr, Matrix.mulVec, dotProduct, Pi.smul_apply] using h + · have hantiFin : Antitone hHerm.eigenvalues := hantiEig + intro i k hik + by_cases hk : k ≤ m + · have hi : i ≤ m := le_trans hik hk + have hfin : (⟨i, Nat.lt_succ_of_le hi⟩ : Fin (m + 1)) ≤ + ⟨k, Nat.lt_succ_of_le hk⟩ := by + exact hik + simpa [s, hi, hk] using hantiFin hfin + · by_cases hi : i ≤ m + · have hnonneg : 0 ≤ hHerm.eigenvalues ⟨i, Nat.lt_succ_of_le hi⟩ := + hPos.eigenvalues_nonneg ⟨i, Nat.lt_succ_of_le hi⟩ + simpa [s, hi, hk] using hnonneg + · simp [s, hi, hk] + · simp [s] + · have htrace := hHerm.trace_eq_sum_eigenvalues + rw [htrace] + apply Finset.sum_congr rfl + intro i _hi + have hi : (i : ℕ) ≤ m := Nat.lt_succ_iff.mp i.isLt + simp [s, hi] + +/-- The sorted self-adjoint eigenvalues supplied by Mathlib are antitone. -/ +theorem symmetricToEuclidean_eigenvalues_antitone_fin + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) : + Antitone + ((Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym)).eigenvalues + (finrank_euclideanSpace_fin : + Module.finrank ℝ (EuclideanSpace ℝ (Fin (m + 1))) = m + 1)) := by + exact (Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym)).eigenvalues_antitone finrank_euclideanSpace_fin + +/-- +Mathlib's sorted self-adjoint eigenbasis consists of eigenvectors for +`A.toEuclideanLin`. +-/ +theorem symmetricToEuclidean_apply_eigenvectorBasis_fin + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) (i : Fin (m + 1)) : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin (m + 1))) = m + 1 := + finrank_euclideanSpace_fin + A.toEuclideanLin (hT.eigenvectorBasis hn i) = + (hT.eigenvalues hn i : ℝ) • hT.eigenvectorBasis hn i := by + intro hT hn + exact hT.apply_eigenvectorBasis hn i + +/-- Coordinate orthonormality of Mathlib's sorted Euclidean eigenbasis. -/ +theorem symmetricToEuclidean_eigenvectorBasis_realDot + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin (m + 1))) = m + 1 := + finrank_euclideanSpace_fin + ∀ i k, + realDot (fun j => (hT.eigenvectorBasis hn i) j) + (fun j => (hT.eigenvectorBasis hn k) j) = + if i = k then 1 else 0 := by + intro hT hn i k + have horth := (orthonormal_iff_ite.mp (hT.eigenvectorBasis hn).orthonormal) i k + rw [realDot_euclidean_eq_inner] + exact horth + +/-- Coordinate form of the sorted Euclidean eigenvector equation. -/ +theorem symmetricToEuclidean_eigenvectorBasis_coord + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin (m + 1))) = m + 1 := + finrank_euclideanSpace_fin + ∀ r j, + (∑ k, A j k * (hT.eigenvectorBasis hn r) k) = + hT.eigenvalues hn r * (hT.eigenvectorBasis hn r) j := by + intro hT hn r j + have h := congrArg (fun y : EuclideanSpace ℝ (Fin (m + 1)) => y j) + (hT.apply_eigenvectorBasis hn r) + rw [toEuclideanLin_apply_eq_sum A (hT.eigenvectorBasis hn r) j] at h + simpa [Pi.smul_apply, smul_eq_mul] using h + +/-- Sorted Euclidean eigenvalues are nonnegative under the project PSD predicate. -/ +theorem symmetricToEuclidean_eigenvalues_nonneg_of_realPSD_fin + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) (hPSD : RealPSD A) : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin (m + 1))) = m + 1 := + finrank_euclideanSpace_fin + ∀ i, 0 ≤ hT.eigenvalues hn i := by + intro hT hn i + let y : EuclideanSpace ℝ (Fin (m + 1)) := hT.eigenvectorBasis hn i + have horth := (orthonormal_iff_ite.mp (hT.eigenvectorBasis hn).orthonormal) i i + have hinner_self : inner ℝ y y = 1 := by + simp [y] + have hnorm_sq : ‖y‖ ^ 2 = 1 := by + simpa [real_inner_self_eq_norm_sq] using hinner_self + have heig : A.toEuclideanLin y = (hT.eigenvalues hn i : ℝ) • y := by + simp [y, hT.apply_eigenvectorBasis hn i] + have hquad : realQuadraticForm A (fun j => y j) = hT.eigenvalues hn i := by + calc + realQuadraticForm A (fun j => y j) + = inner ℝ y (A.toEuclideanLin y) := + realQuadraticForm_euclidean_eq_inner A y + _ = inner ℝ y ((hT.eigenvalues hn i : ℝ) • y) := by + rw [heig] + _ = hT.eigenvalues hn i := by + rw [inner_smul_right, real_inner_self_eq_norm_sq, hnorm_sq] + simp + simpa [hquad] using hPSD (fun j => y j) + +/-- The trace of a real matrix agrees with the sum of Mathlib's sorted eigenvalues. -/ +theorem symmetricToEuclidean_trace_eq_sum_eigenvalues_fin + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin (m + 1))) = m + 1 := + finrank_euclideanSpace_fin + A.trace = ∑ i, hT.eigenvalues hn i := by + intro hT hn + have hmatrix_trace : + LinearMap.trace ℝ (EuclideanSpace ℝ (Fin (m + 1))) A.toEuclideanLin = + A.trace := by + rw [Matrix.toEuclideanLin_eq_toLin_orthonormal] + simp + calc + A.trace = + LinearMap.trace ℝ (EuclideanSpace ℝ (Fin (m + 1))) A.toEuclideanLin := + hmatrix_trace.symm + _ = ∑ i, hT.eigenvalues hn i := by + simpa using hT.trace_eq_sum_eigenvalues hn + +private theorem positiveEigenCoordinateData_of_sorted_segment + {d : Type*} [Fintype d] [DecidableEq d] {N m : ℕ} + (hN : m + 1 ≤ N) + (A : Matrix d d ℝ) (hSym : RealSymmetric A) + (τ : ℝ) + (hn : Module.finrank ℝ (EuclideanSpace ℝ d) = N) + (hpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + ∀ r : Fin (m + 1), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) + (htrace : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + τ = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r)) : + HasPositiveEigenCoordinateData A τ := by + classical + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let embed : Fin (m + 1) → Fin (N) := Fin.castLE hN + let v : Fin (m + 1) → d → ℝ := + fun i => ⇑(hT.eigenvectorBasis hn (embed i)) + let s : ℕ → ℝ := + fun k => + if hk : k ≤ m then + hT.eigenvalues hn (embed ⟨k, Nat.lt_succ_of_le hk⟩) + else 0 + refine ⟨m, v, s, ?_, ?_, ?_, ?_, ?_⟩ + · intro i k + have horth := (orthonormal_iff_ite.mp (hT.eigenvectorBasis hn).orthonormal) + (embed i) (embed k) + rw [realDot_euclidean_eq_inner] + simpa [v, embed, Fin.ext_iff] using horth + · intro r j + have hr : (r : ℕ) ≤ m := Nat.lt_succ_iff.mp r.isLt + have hidx : embed ⟨(r : ℕ), Nat.lt_succ_of_le hr⟩ = embed r := by + ext + simp [embed] + have h := congrArg (fun y : EuclideanSpace ℝ d => y j) + (hT.apply_eigenvectorBasis hn (embed r)) + rw [toEuclideanLin_apply_eq_sum A (hT.eigenvectorBasis hn (embed r)) j] at h + simpa [v, s, hr, hidx, Pi.smul_apply, smul_eq_mul] using h + · intro i k hik + by_cases hk : k ≤ m + · have hi : i ≤ m := le_trans hik hk + have hfin : (embed ⟨i, Nat.lt_succ_of_le hi⟩ : Fin (N)) ≤ + embed ⟨k, Nat.lt_succ_of_le hk⟩ := by + exact hik + have hanti := hT.eigenvalues_antitone hn hfin + simpa [s, hi, hk] using hanti + · by_cases hi : i ≤ m + · have hnonneg := hpos ⟨i, Nat.lt_succ_of_le hi⟩ + change 0 ≤ hT.eigenvalues hn + (Fin.castLE hN (⟨i, Nat.lt_succ_of_le hi⟩ : Fin (m + 1))) at hnonneg + simpa [s, hi, hk, embed] using hnonneg + · simp [s, hi, hk] + · simp [s] + · rw [htrace] + apply Finset.sum_congr rfl + intro i _hi + have hi : (i : ℕ) ≤ m := Nat.lt_succ_iff.mp i.isLt + have hidx : + embed ⟨(i : ℕ), Nat.lt_succ_of_le hi⟩ = Fin.castLE hN i := by + ext + simp [embed] + simp [s, hi, hidx] + +/-- +Mathlib's sorted Euclidean spectral data gives the project's positive +eigen-coordinate data once the trace has been identified with the sorted +eigenvalue sum. +-/ +theorem hasPositiveEigenCoordinateData_of_realPSD_fin_sorted_of_trace + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) (hPSD : RealPSD A) + (htraceSorted : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin (m + 1))) = m + 1 := + finrank_euclideanSpace_fin + A.trace = ∑ i, hT.eigenvalues hn i) : + HasPositiveEigenCoordinateData A A.trace := by + apply positiveEigenCoordinateData_of_sorted_segment + (Nat.le_refl (m + 1)) A hSym A.trace finrank_euclideanSpace_fin + · simpa using symmetricToEuclidean_eigenvalues_nonneg_of_realPSD_fin A hSym hPSD + · simpa using htraceSorted + +/-- Mathlib's sorted Euclidean spectral data gives the positive eigen-coordinate data. -/ +theorem hasPositiveEigenCoordinateData_of_realPSD_fin_sorted + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) (hPSD : RealPSD A) : + HasPositiveEigenCoordinateData A A.trace := + hasPositiveEigenCoordinateData_of_realPSD_fin_sorted_of_trace A hSym hPSD + (symmetricToEuclidean_trace_eq_sum_eigenvalues_fin A hSym) + +/-- +For a finite sequence, if an initial block is nonnegative and the remaining tail +is nonpositive, then the sum of positive parts is the sum over the initial +block. +-/ +theorem sum_posPart_eq_sum_initialSegment_of_signs + {N m : ℕ} (hN : m + 1 ≤ N) (lam : Fin N → ℝ) + (hpos : ∀ r : Fin (m + 1), 0 ≤ lam (Fin.castLE hN r)) + (hnonpos : ∀ i : Fin N, m + 1 ≤ (i : ℕ) → lam i ≤ 0) : + (∑ i : Fin N, (lam i)⁺) = + ∑ r : Fin (m + 1), lam (Fin.castLE hN r) := by + let f : ℕ → ℝ := fun k => if hk : k < N then (lam ⟨k, hk⟩)⁺ else 0 + let g : ℕ → ℝ := fun k => if hk : k < N then lam ⟨k, hk⟩ else 0 + have htotal_fin_to_range : + (∑ i : Fin N, (lam i)⁺) = ∑ k ∈ Finset.range N, f k := by + rw [Finset.sum_range] + apply Finset.sum_congr rfl + intro i _hi + simp [f] + have hinitial_fin_to_range : + (∑ r : Fin (m + 1), lam (Fin.castLE hN r)) = + ∑ k ∈ Finset.range (m + 1), g k := by + rw [Finset.sum_range] + apply Finset.sum_congr rfl + intro i _hi + have hltN : (i : ℕ) < N := lt_of_lt_of_le i.isLt hN + simp [g, hltN, Fin.castLE] + rw [htotal_fin_to_range, hinitial_fin_to_range] + have hsplit := Finset.sum_range_add f (m + 1) (N - (m + 1)) + have hNadd : m + 1 + (N - (m + 1)) = N := Nat.add_sub_of_le hN + rw [hNadd] at hsplit + rw [hsplit] + have hfirst : + ∑ x ∈ Finset.range (m + 1), f x = + ∑ x ∈ Finset.range (m + 1), g x := by + apply Finset.sum_congr rfl + intro k hk + have hkltm : k < m + 1 := Finset.mem_range.mp hk + have hkltN : k < N := lt_of_lt_of_le hkltm hN + have hrpos := hpos ⟨k, hkltm⟩ + have hrpos' : 0 ≤ lam ⟨k, hkltN⟩ := by + simpa [Fin.castLE] using hrpos + simp [f, g, hkltN, posPart_eq_self.mpr hrpos'] + have htail : ∑ x ∈ Finset.range (N - (m + 1)), f (m + 1 + x) = 0 := by + apply Finset.sum_eq_zero + intro x hx + have hxlt : x < N - (m + 1) := Finset.mem_range.mp hx + have hkltN : m + 1 + x < N := by omega + have hnon := hnonpos ⟨m + 1 + x, hkltN⟩ (by simp) + simp [f, hkltN, posPart_eq_zero.mpr hnon] + rw [hfirst, htail, add_zero] + +/-- +A decreasing finite real sequence is either everywhere nonpositive, or its +nonnegative entries form a nonempty initial segment. +-/ +theorem antitone_fin_nonpos_or_initial_nonneg_segment + {N : ℕ} (lam : Fin N → ℝ) (hanti : Antitone lam) : + (∀ i : Fin N, lam i ≤ 0) ∨ + ∃ m : ℕ, ∃ hN : m + 1 ≤ N, + (∀ r : Fin (m + 1), 0 ≤ lam (Fin.castLE hN r)) ∧ + (∀ i : Fin N, m + 1 ≤ (i : ℕ) → lam i ≤ 0) := by + classical + by_cases hall : ∀ i : Fin N, lam i ≤ 0 + · exact Or.inl hall + · right + have hExistsNot : ∃ i : Fin N, ¬ lam i ≤ 0 := not_forall.mp hall + rcases hExistsNot with ⟨i0, hi0⟩ + have hi0nonneg : 0 ≤ lam i0 := le_of_lt (lt_of_not_ge hi0) + let S : Finset (Fin N) := Finset.univ.filter fun i => 0 ≤ lam i + have hSnonempty : S.Nonempty := by + refine ⟨i0, ?_⟩ + simp [S, hi0nonneg] + rcases Finset.exists_max_image S (fun i : Fin N => (i : ℕ)) hSnonempty with + ⟨imax, himax_mem, himax_max⟩ + let m : ℕ := imax + have hmN : m + 1 ≤ N := Nat.succ_le_of_lt imax.isLt + refine ⟨m, hmN, ?_, ?_⟩ + · intro r + have hrle : (Fin.castLE hmN r : Fin N) ≤ imax := by + exact Nat.lt_succ_iff.mp r.isLt + have himax_nonneg : 0 ≤ lam imax := by + have := (Finset.mem_filter.mp himax_mem).2 + simpa [S] using this + exact himax_nonneg.trans (hanti hrle) + · intro i hi + by_contra hnot + have hinonneg : 0 ≤ lam i := le_of_lt (lt_of_not_ge hnot) + have hi_mem : i ∈ S := by + simp [S, hinonneg] + have hile : (i : ℕ) ≤ m := himax_max i hi_mem + omega + +/-- +Positive initial segment construction for an arbitrary finite coordinate +type, indexed through Mathlib's canonical sorted eigenvalue list. +-/ +theorem hasPositiveEigenCoordinateData_of_sorted_positiveInitialSegment_card + {d : Type*} [Fintype d] [DecidableEq d] {m : ℕ} + (hN : m + 1 ≤ Fintype.card d) + (A : Matrix d d ℝ) (hSym : RealSymmetric A) + (τ : ℝ) + (hpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ d) = Fintype.card d := + finrank_euclideanSpace + ∀ r : Fin (m + 1), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) + (htrace : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ d) = Fintype.card d := + finrank_euclideanSpace + τ = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r)) : + HasPositiveEigenCoordinateData A τ := by + exact positiveEigenCoordinateData_of_sorted_segment hN A hSym τ + finrank_euclideanSpace hpos htrace + +/-- +An initial segment of Mathlib's sorted Euclidean eigenbasis gives the positive +eigen-coordinate data consumed by Ball--Prodromou. The hypotheses say that the +selected `m+1` sorted eigenvalues are nonnegative and have total `τ`. +-/ +theorem hasPositiveEigenCoordinateData_of_sorted_positiveInitialSegment + {N m : ℕ} (hN : m + 1 ≤ N) + (A : Matrix (Fin N) (Fin N) ℝ) (hSym : RealSymmetric A) + (τ : ℝ) + (hpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + ∀ r : Fin (m + 1), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) + (htrace : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + τ = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r)) : + HasPositiveEigenCoordinateData A τ := by + exact positiveEigenCoordinateData_of_sorted_segment hN A hSym τ + finrank_euclideanSpace_fin hpos htrace + +/-- +The explicit eigen-coordinate data obtained from a positive spectral subspace +supplies the diagonal model consumed by Ball--Prodromou. +-/ +theorem hasBallProdromouDiagonalModel_of_eigenCoordinateData + {d : Type*} [Fintype d] (A : Matrix d d ℝ) (τ : ℝ) + (hdata : HasPositiveEigenCoordinateData A τ) : + HasBallProdromouDiagonalModel A τ := by + classical + rcases hdata with ⟨m, v, s, horth, heigen, hanti, hs_last, htrace⟩ + refine ⟨m, coordinateConstraintVectors v, s, ?_, hanti, hs_last, htrace, ?_⟩ + · exact parseval_coordinateConstraintVectors v horth + · intro w + have hamb : + (fun j => realDot w (coordinateConstraintVectors v j)) = + ambientOfEigenCoordinates v w := by + funext j + simp [coordinateConstraintVectors, ambientOfEigenCoordinates, realDot] + rw [hamb] + exact realQuadraticForm_ambientOfEigenCoordinates A v s horth heigen w + +/-- Eigen-coordinate data feeds directly into the BP cube quadratic maximum. -/ +theorem cubeQuadraticMaximum_from_eigenCoordinateData + {d : Type*} [Fintype d] (A : Matrix d d ℝ) (τ : ℝ) + (hdata : HasPositiveEigenCoordinateData A τ) : + ∃ x : d → ℝ, InRealUnitCube x ∧ τ ≤ realQuadraticForm A x := + cubeQuadraticMaximum_from_diagonalBP A τ + (hasBallProdromouDiagonalModel_of_eigenCoordinateData A τ hdata) + +/-- +Any support-function upper bound `tr(AG) ≤ τ`, together with +Ball--Prodromou eigen-coordinate data proving `τ ≤ qᵀAq` for some cube vector, +gives the support inequality needed by the convex-hull argument. +-/ +theorem supportInequality_from_upperBound_and_eigenCoordinateData + {d : Type*} [Fintype d] [DecidableEq d] + (A : Matrix d d ℝ) (τ : ℝ) + (hupper : ∀ G : Matrix d d ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ τ) + (hdata : HasPositiveEigenCoordinateData A τ) : + ∃ x : d → ℝ, + InRealUnitCube x ∧ + ∀ G : Matrix d d ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ realQuadraticForm A x := by + rcases cubeQuadraticMaximum_from_eigenCoordinateData A τ hdata with + ⟨x, hcube, hx⟩ + refine ⟨x, hcube, ?_⟩ + intro G hGsym hGbetween + exact (hupper G hGsym hGbetween).trans hx + +/-- +Positive spectral-coordinate data plus the positive-part support-function +property gives the support inequality used in the convex-hull argument. +-/ +theorem supportInequality_from_eigenCoordinateData + {d : Type*} [Fintype d] [DecidableEq d] + (A Apos : Matrix d d ℝ) + (hsupport : HasPositivePartSupportFunction A Apos) + (hdata : HasPositiveEigenCoordinateData A Apos.trace) : + ∃ x : d → ℝ, + InRealUnitCube x ∧ + ∀ G : Matrix d d ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ realQuadraticForm A x := by + exact supportInequality_from_upperBound_and_eigenCoordinateData A Apos.trace + (fun G hGsym hGbetween => hsupport.1 G hGsym hGbetween) hdata + +/-- +The same support inequality, using the abstract positive/negative spectral-part +criterion for the support-function property. +-/ +theorem supportInequality_from_posNegProjection_and_eigenData + {d : Type*} [Fintype d] [DecidableEq d] + (A Apos Aneg Ppos : Matrix d d ℝ) + (hAeq : A = Apos - Aneg) + (hAposSym : RealSymmetric Apos) (hAnegSym : RealSymmetric Aneg) + (hAposPSD : RealPSD Apos) (hAnegPSD : RealPSD Aneg) + (hPposSym : RealSymmetric Ppos) + (hPposBetween : RealLoewnerBetweenZeroAndOne Ppos) + (hApos_mul_Ppos : Apos * Ppos = Apos) + (hAneg_mul_Ppos : Aneg * Ppos = 0) + (hdata : HasPositiveEigenCoordinateData A Apos.trace) : + ∃ x : d → ℝ, + InRealUnitCube x ∧ + ∀ G : Matrix d d ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ realQuadraticForm A x := by + exact supportInequality_from_eigenCoordinateData A Apos + (hasPositivePartSupportFunction_of_posNegProjection + A Apos Aneg Ppos hAeq hAposSym hAnegSym hAposPSD hAnegPSD + hPposSym hPposBetween hApos_mul_Ppos hAneg_mul_Ppos) + hdata + +/-- +CFC positive part plus a nonnegative sorted initial eigenvalue segment gives +the support inequality for the symmetric test matrix `A`. +-/ +theorem supportInequality_from_cfc_posPart_initialSegment + {N m : ℕ} (hN : m + 1 ≤ N) + (A : Matrix (Fin N) (Fin N) ℝ) (hSym : RealSymmetric A) + (hpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + ∀ r : Fin (m + 1), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) + (htrace : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + (A⁺).trace = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r)) : + ∃ x : Fin N → ℝ, + InRealUnitCube x ∧ + ∀ G : Matrix (Fin N) (Fin N) ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ realQuadraticForm A x := + supportInequality_from_upperBound_and_eigenCoordinateData A (A⁺).trace + (supportUpperBound_cfc_posPart A hSym) + (hasPositiveEigenCoordinateData_of_sorted_positiveInitialSegment + hN A hSym (A⁺).trace hpos htrace) + +/-- +If the CFC positive-part trace is known to be the sum of positive parts of the +sorted eigenvalues, then a sign pattern for an initial segment identifies that +trace with the initial segment sum. +-/ +theorem trace_posPart_eq_sum_initialSegment_of_sorted_signs + {N m : ℕ} (hN : m + 1 ≤ N) + (A : Matrix (Fin N) (Fin N) ℝ) (hSym : RealSymmetric A) + (htracePosParts : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + (A⁺).trace = ∑ i : Fin N, (hT.eigenvalues hn i)⁺) + (hpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + ∀ r : Fin (m + 1), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) + (hnonpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + ∀ i : Fin N, m + 1 ≤ (i : ℕ) → hT.eigenvalues hn i ≤ 0) : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + (A⁺).trace = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r) := by + intro hT hn + rw [htracePosParts] + exact sum_posPart_eq_sum_initialSegment_of_signs hN + (fun i : Fin N => hT.eigenvalues hn i) hpos hnonpos + +/-- +The support inequality follows from a sorted eigenvalue sign pattern, once the +CFC positive-part trace has been identified with the sorted positive-part sum. +-/ +theorem supportInequality_from_cfc_posPart_sorted_signs + {N m : ℕ} (hN : m + 1 ≤ N) + (A : Matrix (Fin N) (Fin N) ℝ) (hSym : RealSymmetric A) + (htracePosParts : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + (A⁺).trace = ∑ i : Fin N, (hT.eigenvalues hn i)⁺) + (hpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + ∀ r : Fin (m + 1), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) + (hnonpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + ∀ i : Fin N, m + 1 ≤ (i : ℕ) → hT.eigenvalues hn i ≤ 0) : + ∃ x : Fin N → ℝ, + InRealUnitCube x ∧ + ∀ G : Matrix (Fin N) (Fin N) ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ realQuadraticForm A x := by + have htrace : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin N)) = N := + finrank_euclideanSpace_fin + (A⁺).trace = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r) := + trace_posPart_eq_sum_initialSegment_of_sorted_signs + hN A hSym htracePosParts hpos hnonpos + exact supportInequality_from_cfc_posPart_initialSegment hN A hSym hpos htrace + +/-- +For an arbitrary finite coordinate type, a sorted eigenvalue sign pattern +identifies the CFC positive-part trace with the nonnegative initial segment. +-/ +theorem trace_posPart_eq_sum_initialSegment_of_sorted_signs_card + {d : Type*} [Fintype d] [DecidableEq d] {m : ℕ} + (hN : m + 1 ≤ Fintype.card d) + (A : Matrix d d ℝ) (hSym : RealSymmetric A) + (hpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ d) = Fintype.card d := + finrank_euclideanSpace + ∀ r : Fin (m + 1), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) + (hnonpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ d) = Fintype.card d := + finrank_euclideanSpace + ∀ i : Fin (Fintype.card d), m + 1 ≤ (i : ℕ) → + hT.eigenvalues hn i ≤ 0) : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ d) = Fintype.card d := + finrank_euclideanSpace + (A⁺).trace = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r) := by + intro hT hn + rw [trace_posPart_eq_sum_eigenvalues₀ A hSym] + exact sum_posPart_eq_sum_initialSegment_of_signs hN + (fun i : Fin (Fintype.card d) => hT.eigenvalues hn i) hpos hnonpos + +/-- +For an arbitrary finite coordinate type, the CFC positive-part support +inequality follows from a sorted eigenvalue sign pattern. +-/ +theorem supportInequality_from_cfc_posPart_sorted_signs_card + {d : Type*} [Fintype d] [DecidableEq d] {m : ℕ} + (hN : m + 1 ≤ Fintype.card d) + (A : Matrix d d ℝ) (hSym : RealSymmetric A) + (hpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ d) = Fintype.card d := + finrank_euclideanSpace + ∀ r : Fin (m + 1), 0 ≤ hT.eigenvalues hn (Fin.castLE hN r)) + (hnonpos : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ d) = Fintype.card d := + finrank_euclideanSpace + ∀ i : Fin (Fintype.card d), m + 1 ≤ (i : ℕ) → + hT.eigenvalues hn i ≤ 0) : + ∃ x : d → ℝ, + InRealUnitCube x ∧ + ∀ G : Matrix d d ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ realQuadraticForm A x := by + have htrace : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ d) = Fintype.card d := + finrank_euclideanSpace + (A⁺).trace = ∑ r : Fin (m + 1), hT.eigenvalues hn (Fin.castLE hN r) := + trace_posPart_eq_sum_initialSegment_of_sorted_signs_card + hN A hSym hpos hnonpos + exact supportInequality_from_upperBound_and_eigenCoordinateData A (A⁺).trace + (supportUpperBound_cfc_posPart A hSym) + (hasPositiveEigenCoordinateData_of_sorted_positiveInitialSegment_card + hN A hSym (A⁺).trace hpos htrace) + +/-- +If the CFC positive part has zero trace, the support inequality is witnessed by +the zero cube vector, for any finite coordinate type. +-/ +theorem supportInequality_of_cfc_posPart_trace_zero_card + {d : Type*} [Fintype d] [DecidableEq d] + (A : Matrix d d ℝ) (hSym : RealSymmetric A) + (htrace0 : (A⁺).trace = 0) : + ∃ x : d → ℝ, + InRealUnitCube x ∧ + ∀ G : Matrix d d ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ realQuadraticForm A x := by + refine ⟨0, ?_, ?_⟩ + · intro i + simp + · intro G hGsym hGbetween + have hupper := supportUpperBound_cfc_posPart A hSym G hGsym hGbetween + rw [htrace0] at hupper + simpa [realQuadraticForm] using hupper + +/-- +Ball--Prodromou plus the CFC positive part gives the support inequality for +every real symmetric test matrix on an arbitrary finite coordinate type. +-/ +theorem supportInequality_from_cfc_posPart_card + {d : Type*} [Fintype d] [DecidableEq d] + (A : Matrix d d ℝ) (hSym : RealSymmetric A) : + ∃ x : d → ℝ, + InRealUnitCube x ∧ + ∀ G : Matrix d d ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ realQuadraticForm A x := by + classical + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ d) = Fintype.card d := + finrank_euclideanSpace + have hcut := + antitone_fin_nonpos_or_initial_nonneg_segment + (fun i : Fin (Fintype.card d) => hT.eigenvalues hn i) + (hT.eigenvalues_antitone hn) + rcases hcut with hall | ⟨m, hN, hpos, hnonpos⟩ + · refine supportInequality_of_cfc_posPart_trace_zero_card A hSym ?_ + rw [trace_posPart_eq_sum_eigenvalues₀ A hSym] + apply Finset.sum_eq_zero + intro i _hi + exact posPart_eq_zero.mpr (hall i) + · exact supportInequality_from_cfc_posPart_sorted_signs_card + hN A hSym hpos hnonpos + +/-- +Ball--Prodromou and separation put every real symmetric `0 ≤ T ≤ I` into the +closed convex hull of flattened rank-one cube matrices. + +The remaining step toward `HasRealConvexDecomposition` is to replace this +closed-hull membership by ordinary convex-hull membership for the compact +rank-one cube image. +-/ +theorem matrixToEuclidean_mem_closedConvexHull_rankOneCube_of_loewner + {d : Type*} [Fintype d] [DecidableEq d] + (T : Matrix d d ℝ) (hT : RealSymmetric T) + (hTbetween : RealLoewnerBetweenZeroAndOne T) : + matrixToEuclidean T ∈ + closedConvexHull ℝ (realRankOneCubeEuclideanSet d) := by + classical + by_contra hnot + rcases geometric_hahn_banach_point_closed + (convex_closedConvexHull (𝕜 := ℝ) (s := realRankOneCubeEuclideanSet d)) + (isClosed_closedConvexHull (𝕜 := ℝ) (s := realRankOneCubeEuclideanSet d)) + hnot with ⟨f, u, hTf, hsep⟩ + let y : EuclideanSpace ℝ (d × d) := + (InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (d × d))).symm f + let Aflat : EuclideanSpace ℝ (d × d) := -y + let A : Matrix d d ℝ := euclideanToMatrix Aflat + rcases supportInequality_from_cfc_posPart_card (realSymmPart A) + (realSymmetric_realSymmPart A) with ⟨q, hq, hsupport⟩ + have htrace := hsupport T hT hTbetween + have hflatA : matrixToEuclidean A = Aflat := + matrixToEuclidean_euclideanToMatrix Aflat + have hinnerT_trace : + inner ℝ Aflat (matrixToEuclidean T) = + (realSymmPart A * T).trace := by + rw [← hflatA] + rw [inner_matrixToEuclidean_eq_trace_transpose_mul] + exact trace_transpose_mul_eq_trace_realSymmPart_mul_of_realSymmetric A T hT + have hinnerQ_trace : + inner ℝ Aflat (matrixToEuclidean (realRankOne q)) = + realQuadraticForm (realSymmPart A) q := by + rw [← hflatA] + rw [inner_matrixToEuclidean_realRankOne_eq_realQuadraticForm] + exact (realQuadraticForm_realSymmPart A q).symm + have hinner : + inner ℝ Aflat (matrixToEuclidean T) ≤ + inner ℝ Aflat (matrixToEuclidean (realRankOne q)) := by + simpa [hinnerT_trace, hinnerQ_trace] using htrace + have hA_T : + inner ℝ Aflat (matrixToEuclidean T) = -f (matrixToEuclidean T) := by + simp [Aflat, y, InnerProductSpace.toDual_symm_apply] + have hA_q : + inner ℝ Aflat (matrixToEuclidean (realRankOne q)) = + -f (matrixToEuclidean (realRankOne q)) := by + simp [Aflat, y, InnerProductSpace.toDual_symm_apply] + have hf_le : + f (matrixToEuclidean (realRankOne q)) ≤ f (matrixToEuclidean T) := by + rw [hA_T, hA_q] at hinner + linarith + have hqclosed : + matrixToEuclidean (realRankOne q) ∈ + closedConvexHull ℝ (realRankOneCubeEuclideanSet d) := by + exact subset_closedConvexHull ⟨realRankOne q, ⟨q, hq, rfl⟩, rfl⟩ + have hsepq : + u < f (matrixToEuclidean (realRankOne q)) := + hsep (matrixToEuclidean (realRankOne q)) hqclosed + linarith + +/-- +For the compact rank-one cube image, the closed-convex-hull membership from +separation is ordinary convex-hull membership. +-/ +theorem matrixToEuclidean_mem_convexHull_rankOneCube_of_loewner + {d : Type*} [Fintype d] [DecidableEq d] + (T : Matrix d d ℝ) (hT : RealSymmetric T) + (hTbetween : RealLoewnerBetweenZeroAndOne T) : + matrixToEuclidean T ∈ convexHull ℝ (realRankOneCubeEuclideanSet d) := by + have hclosed := + matrixToEuclidean_mem_closedConvexHull_rankOneCube_of_loewner T hT hTbetween + rwa [closedConvexHull_eq_convexHull_of_isCompact + (isCompact_realRankOneCubeEuclideanSet (d := d))] at hclosed + +/-- +Real convex decomposition of every symmetric matrix satisfying `0 ≤ T ≤ I`. + +This is the finite-dimensional convex-hull extraction step in the paper: +membership of `T` in the convex hull of the rank-one cube matrices is unpacked +into explicit weights and cube vectors. +-/ +theorem hasRealConvexDecomposition + (d : Type*) [Fintype d] [DecidableEq d] : + HasRealConvexDecomposition d := by + classical + intro T hT hTbetween + have hconv := + matrixToEuclidean_mem_convexHull_rankOneCube_of_loewner T hT hTbetween + rw [mem_convexHull_iff_exists_fintype] at hconv + rcases hconv with ⟨ι, hι, w, z, hw, hsum, hz, hcenter⟩ + let : Fintype ι := hι + let m := Fintype.card ι + have hm : 0 < m := by + by_contra hnot + have hzero : Fintype.card ι = 0 := Nat.eq_zero_of_not_pos hnot + have : IsEmpty ι := Fintype.card_eq_zero_iff.mp hzero + simp at hsum + let e : ι ≃ Fin m := Fintype.equivFin ι + let p : Fin m → ℝ := fun r => w (e.symm r) + have hz_rank : + ∀ r : Fin m, ∃ q : d → ℝ, + InRealUnitCube q ∧ z (e.symm r) = matrixToEuclidean (realRankOne q) := by + intro r + rcases hz (e.symm r) with ⟨R, ⟨q, hq, hR⟩, hzR⟩ + exact ⟨q, hq, by rw [← hzR, hR]⟩ + let q : Fin m → d → ℝ := fun r => Classical.choose (hz_rank r) + have hqcube : ∀ r, InRealUnitCube (q r) := + fun r => (Classical.choose_spec (hz_rank r)).1 + have hz_eq : ∀ r, z (e.symm r) = matrixToEuclidean (realRankOne (q r)) := + fun r => (Classical.choose_spec (hz_rank r)).2 + have hp : ∀ r, 0 ≤ p r := fun r => hw (e.symm r) + have hpsum : ∑ r, p r = 1 := by + rw [← hsum] + symm + simpa [p] using Equiv.sum_comp e + (fun r : Fin m => w (e.symm r)) + have hcenter_fin : + ∑ r : Fin m, p r • z (e.symm r) = matrixToEuclidean T := by + rw [← hcenter] + symm + simpa [p] using Equiv.sum_comp e + (fun r : Fin m => w (e.symm r) • z (e.symm r)) + have hvec : + ∑ r : Fin m, p r • matrixToEuclidean (realRankOne (q r)) = + matrixToEuclidean T := by + simpa [hz_eq] using hcenter_fin + refine ⟨m, hm, p, q, hp, hpsum, hqcube, ?_⟩ + intro a b + have hcoord := congrArg (fun v : EuclideanSpace ℝ (d × d) => v (a, b)) hvec + simpa [matrixToEuclidean, realRankOne, smul_eq_mul, mul_assoc, mul_left_comm, + mul_comm] using hcoord.symm + +/-- +If the CFC positive part has zero trace, the support inequality is witnessed by +the zero cube vector. +-/ +theorem supportInequality_of_cfc_posPart_trace_zero + {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ) (hSym : RealSymmetric A) + (htrace0 : (A⁺).trace = 0) : + ∃ x : Fin N → ℝ, + InRealUnitCube x ∧ + ∀ G : Matrix (Fin N) (Fin N) ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ realQuadraticForm A x := by + exact supportInequality_of_cfc_posPart_trace_zero_card A hSym htrace0 + +/-- +Ball--Prodromou in matrix form for a positive semidefinite real symmetric matrix +whose eigenvalues are indexed in decreasing order. +-/ +theorem cubeQuadraticMaximum_of_realPSD_fin + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) (hPSD : RealPSD A) + (hantiEig : Antitone (realSymmetric_isHermitian A hSym).eigenvalues) : + ∃ x : Fin (m + 1) → ℝ, + InRealUnitCube x ∧ A.trace ≤ realQuadraticForm A x := + cubeQuadraticMaximum_from_eigenCoordinateData A A.trace + (hasPositiveEigenCoordinateData_of_realPSD_fin A hSym hPSD hantiEig) + +/-- +Ball--Prodromou cube quadratic maximum from Mathlib's sorted Euclidean spectral +data, with the remaining trace-identification hypothesis explicit. +-/ +theorem cubeQuadraticMaximum_of_realPSD_fin_sorted_of_trace + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) (hPSD : RealPSD A) + (htraceSorted : + let hT := Matrix.isSymmetric_toEuclideanLin_iff.mpr + (realSymmetric_isHermitian A hSym) + let hn : Module.finrank ℝ (EuclideanSpace ℝ (Fin (m + 1))) = m + 1 := + finrank_euclideanSpace_fin + A.trace = ∑ i, hT.eigenvalues hn i) : + ∃ x : Fin (m + 1) → ℝ, + InRealUnitCube x ∧ A.trace ≤ realQuadraticForm A x := + cubeQuadraticMaximum_from_eigenCoordinateData A A.trace + (hasPositiveEigenCoordinateData_of_realPSD_fin_sorted_of_trace + A hSym hPSD htraceSorted) + +/-- +Ball--Prodromou in matrix form for a positive semidefinite real symmetric matrix, +using Mathlib's sorted Euclidean spectral data directly. +-/ +theorem cubeQuadraticMaximum_of_realPSD_fin_sorted + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) (hPSD : RealPSD A) : + ∃ x : Fin (m + 1) → ℝ, + InRealUnitCube x ∧ A.trace ≤ realQuadraticForm A x := + cubeQuadraticMaximum_from_eigenCoordinateData A A.trace + (hasPositiveEigenCoordinateData_of_realPSD_fin_sorted A hSym hPSD) + +/-- +For a positive semidefinite real symmetric test matrix, Ball--Prodromou gives a +single cube vector whose quadratic value dominates all trace pairings +`tr(AG)` with `0 ≤ G ≤ I`. +-/ +theorem supportInequality_of_realPSD_fin_sorted + {m : ℕ} (A : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) + (hSym : RealSymmetric A) (hPSD : RealPSD A) : + ∃ x : Fin (m + 1) → ℝ, + InRealUnitCube x ∧ + ∀ G : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ realQuadraticForm A x := by + rcases cubeQuadraticMaximum_of_realPSD_fin_sorted A hSym hPSD with + ⟨x, hcube, hx⟩ + refine ⟨x, hcube, ?_⟩ + intro G hGsym hGbetween + exact ((hasPositivePartSupportFunction_of_realPSD A hSym hPSD).1 + G hGsym hGbetween).trans hx + +end OlevskiiGram diff --git a/LeanPool/GrothendieckBessel/ComplexReduction.lean b/LeanPool/GrothendieckBessel/ComplexReduction.lean new file mode 100644 index 0000000000..f20e8190f2 --- /dev/null +++ b/LeanPool/GrothendieckBessel/ComplexReduction.lean @@ -0,0 +1,243 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import LeanPool.GrothendieckBessel.RealConvex +public import Mathlib.Analysis.InnerProductSpace.GramMatrix + +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.Ring + +/-! +# Real block reduction of complex Gram matrices +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + +noncomputable section + +open scoped BigOperators ComplexConjugate ComplexOrder + +namespace OlevskiiGram + +private lemma complexRe_ite_one_zero (p : Prop) [Decidable p] : + Complex.re (if p then (1 : ℂ) else 0) = (if p then (1 : ℝ) else 0) := by + by_cases hp : p <;> simp [hp] + +private lemma complexIm_ite_one_zero (p : Prop) [Decidable p] : + Complex.im (if p then (1 : ℂ) else 0) = 0 := by + by_cases hp : p <;> simp [hp] + +private lemma scaled_complex_norm_le_one (a b : ℝ) (ha : |a| ≤ 1) (hb : |b| ≤ 1) : + ‖(((a : ℂ) + (b : ℂ) * Complex.I) / (Real.sqrt 2 : ℂ))‖ ≤ 1 := by + let z : ℂ := (((a : ℂ) + (b : ℂ) * Complex.I) / (Real.sqrt 2 : ℂ)) + have hnormsq : Complex.normSq z ≤ 1 := by + dsimp [z] + rw [Complex.normSq_div, Complex.normSq_add_mul_I, Complex.normSq_ofReal] + have hsqrt_sq : Real.sqrt 2 * Real.sqrt 2 = (2 : ℝ) := by + rw [← sq] + exact Real.sq_sqrt (by norm_num) + have ha2 : a ^ 2 ≤ 1 := by + rwa [sq_le_one_iff_abs_le_one] + have hb2 : b ^ 2 ≤ 1 := by + rwa [sq_le_one_iff_abs_le_one] + rw [hsqrt_sq] + nlinarith + have hsq : ‖z‖ ^ 2 ≤ 1 := by + simpa [Complex.sq_norm] using hnormsq + exact (sq_le_one_iff₀ (norm_nonneg z)).mp hsq + +theorem realBlock_quadraticForm + {n : Type*} [Fintype n] + (G : Matrix n n ℂ) (x : Sum n n → ℝ) : + realQuadraticForm (realBlockMatrix (complexReMatrix G) (complexImMatrix G)) x = + complexQuadraticFormRe G + (fun i : n => (x (Sum.inl i) : ℂ) + Complex.I * (x (Sum.inr i) : ℂ)) := by + simp [realQuadraticForm, complexQuadraticFormRe, realBlockMatrix, + complexReMatrix, complexImMatrix, Finset.sum_add_distrib, add_comm] + ring_nf + +theorem realBlock_one_sub_quadraticForm + {n : Type*} [Fintype n] [DecidableEq n] + (G : Matrix n n ℂ) (x : Sum n n → ℝ) : + realQuadraticForm (1 - realBlockMatrix (complexReMatrix G) (complexImMatrix G)) x = + complexQuadraticFormRe (1 - G) + (fun i : n => (x (Sum.inl i) : ℂ) + Complex.I * (x (Sum.inr i) : ℂ)) := by + simp [realQuadraticForm, complexQuadraticFormRe, realBlockMatrix, + complexReMatrix, complexImMatrix, Matrix.one_apply, Finset.sum_add_distrib, + add_comm, sub_eq_add_neg, complexRe_ite_one_zero, complexIm_ite_one_zero] + +/-- Bridge from Mathlib's complex matrix PSD predicate to the quadratic-form predicate. -/ +theorem complexPSD_of_posSemidef + {n : Type*} [Fintype n] (A : Matrix n n ℂ) : + A.PosSemidef → ComplexPSD A := by + intro hA x + have hx := hA.dotProduct_mulVec_nonneg x + have hxre := (RCLike.nonneg_iff.mp hx).1 + simpa [complexQuadraticFormRe, Matrix.dotProduct_mulVec, dotProduct, Matrix.mulVec] using hxre + +/-- The complex quadratic form is the real part of the Euclidean operator form. -/ +theorem complexQuadraticFormRe_eq_operator_inner + {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (x : Fin N → ℂ) : + complexQuadraticFormRe A x = + Complex.re (inner ℂ (WithLp.toLp 2 x) + (matrixL2Operator A (WithLp.toLp 2 x))) := by + simp [complexQuadraticFormRe, matrixL2Operator, EuclideanSpace.inner_toLp_toLp, + dotProduct, Matrix.mulVec, mul_comm] + +theorem matrixL2Operator_one_sub_apply + {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (x : Fin N → ℂ) : + matrixL2Operator (1 - A) (WithLp.toLp 2 x) = + WithLp.toLp 2 x - matrixL2Operator A (WithLp.toLp 2 x) := by + simp [matrixL2Operator, sub_eq_add_neg] + +theorem complexPSD_one_sub_of_operatorNorm + {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) : + matrixL2OperatorNormLE A 1 → ComplexPSD (1 - A) := by + intro hA x + rw [complexQuadraticFormRe_eq_operator_inner] + rw [matrixL2Operator_one_sub_apply] + let v : EuclideanSpace ℂ (Fin N) := WithLp.toLp 2 x + let T := matrixL2Operator A + have hinner : Complex.re (inner ℂ v (T v)) ≤ ‖v‖ * ‖T v‖ := by + exact re_inner_le_norm (𝕜 := ℂ) v (T v) + have happly : ‖T v‖ ≤ ‖v‖ := by + simpa using T.le_of_opNorm_le hA v + have hbound : Complex.re (inner ℂ v (T v)) ≤ ‖v‖ ^ 2 := by + calc + Complex.re (inner ℂ v (T v)) ≤ ‖v‖ * ‖T v‖ := hinner + _ ≤ ‖v‖ * ‖v‖ := mul_le_mul_of_nonneg_left happly (norm_nonneg v) + _ = ‖v‖ ^ 2 := by ring + have hnonneg : 0 ≤ ‖v‖ ^ 2 - Complex.re (inner ℂ v (T v)) := sub_nonneg.mpr hbound + convert hnonneg using 1 + simp [v, T, inner_sub_right, inner_self_eq_norm_sq_to_K, Complex.sub_re, sq] + +/-- +The Gram matrix with operator norm at most one satisfies the Hermitian and +Loewner-order hypotheses needed for the decomposition. +-/ +theorem gramMatrix_psd_le_one + {N : ℕ} {H : Type*} + [NormedAddCommGroup H] [InnerProductSpace ℂ H] + (z : Fin N → H) : + matrixL2OperatorNormLE (gramMatrix z) 1 → + ComplexHermitian (gramMatrix z) ∧ + ComplexLoewnerBetweenZeroAndOne (gramMatrix z) := by + intro hG + constructor + · intro i j + simp [gramMatrix] + · constructor + · have hgram : gramMatrix z = (Matrix.gram ℂ z).transpose := by + ext i j + simp [gramMatrix, Matrix.gram] + have hpos : (gramMatrix z).PosSemidef := by + rw [hgram] + exact (Matrix.posSemidef_gram ℂ z).transpose + exact complexPSD_of_posSemidef _ hpos + · exact complexPSD_one_sub_of_operatorNorm (gramMatrix z) hG + +/-- +The real block matrix of a Hermitian complex matrix `0 ≤ G ≤ I` also satisfies +`0 ≤ G_real ≤ I`. +-/ +theorem realBlock_psd_le_one + {n : Type*} [Fintype n] [DecidableEq n] + (G : Matrix n n ℂ) : + ComplexHermitian G → ComplexLoewnerBetweenZeroAndOne G → + let Gtilde := realBlockMatrix (complexReMatrix G) (complexImMatrix G) + RealSymmetric Gtilde ∧ RealLoewnerBetweenZeroAndOne Gtilde := by + intro hHerm hLoewner + dsimp + constructor + · intro a b + cases a with + | inl i => + cases b with + | inl j => + dsimp [realBlockMatrix, complexReMatrix] + have h := congrArg Complex.re (hHerm j i) + simpa using h + | inr j => + dsimp [realBlockMatrix, complexImMatrix] + have h := congrArg Complex.im (hHerm i j) + simpa using h.symm + | inr i => + cases b with + | inl j => + dsimp [realBlockMatrix, complexImMatrix] + have h := congrArg Complex.im (hHerm j i) + simpa using h + | inr j => + dsimp [realBlockMatrix, complexReMatrix] + have h := congrArg Complex.re (hHerm j i) + simpa using h + · constructor + · intro x + rw [realBlock_quadraticForm] + exact hLoewner.1 _ + · intro x + rw [realBlock_one_sub_quadraticForm] + exact hLoewner.2 _ + +/-- +Finite complex rank-one decomposition of a Hermitian matrix `0 ≤ G ≤ I` by +vectors with coordinatewise norm at most one. +-/ +theorem finiteComplexDecomposition + {n : Type*} [Fintype n] [DecidableEq n] + (G : Matrix n n ℂ) : + HasRealConvexDecomposition (Sum n n) → + ComplexHermitian G → ComplexLoewnerBetweenZeroAndOne G → + ∃ (m : ℕ) (_hm : 0 < m) (p : Fin m → ℝ) (ζ : Fin m → n → ℂ), + (∀ r, 0 ≤ p r) ∧ + (∑ r, p r = 1) ∧ + (∀ r j, ‖ζ r j‖ ≤ 1) ∧ + ∀ j k, G j k = ∑ r, (p r : ℂ) * ζ r j * star (ζ r k) := by + intro hdecomp hHerm hLoewner + rcases realBlock_psd_le_one G hHerm hLoewner with ⟨hSym, hBetween⟩ + rcases hdecomp (realBlockMatrix (complexReMatrix G) (complexImMatrix G)) + hSym hBetween with + ⟨m, hm, p, q, hp, hpsum, hcube, hentry⟩ + let ζ : Fin m → n → ℂ := fun r j => + ((q r (Sum.inl j) : ℂ) + (q r (Sum.inr j) : ℂ) * Complex.I) / (Real.sqrt 2 : ℂ) + refine ⟨m, hm, p, ζ, hp, hpsum, ?_, ?_⟩ + · intro r j + exact scaled_complex_norm_le_one _ _ (hcube r (Sum.inl j)) (hcube r (Sum.inr j)) + · intro j k + apply Complex.ext + · have hLL := hentry (Sum.inl j) (Sum.inl k) + have hRR := hentry (Sum.inr j) (Sum.inr k) + dsimp [realBlockMatrix, complexReMatrix] at hLL hRR + simp [ζ] + have hsqrt_inv_sq : (Real.sqrt 2)⁻¹ ^ 2 = (1 / 2 : ℝ) := by + rw [inv_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)] + norm_num + ring_nf + rw [hsqrt_inv_sq] + ring_nf at hLL hRR ⊢ + rw [← Finset.sum_mul, ← Finset.sum_mul] + rw [← hLL, ← hRR] + ring + · have hIL := hentry (Sum.inr j) (Sum.inl k) + have hLI := hentry (Sum.inl j) (Sum.inr k) + dsimp [realBlockMatrix, complexImMatrix] at hIL hLI + simp [ζ] + have hsqrt_inv_sq : (Real.sqrt 2)⁻¹ ^ 2 = (1 / 2 : ℝ) := by + rw [inv_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)] + norm_num + ring_nf + rw [hsqrt_inv_sq] + ring_nf at hIL hLI ⊢ + rw [Finset.sum_add_distrib] + rw [← Finset.sum_mul, ← Finset.sum_mul] + rw [← hLI, ← hIL] + ring + +end OlevskiiGram diff --git a/LeanPool/GrothendieckBessel/Conventions.lean b/LeanPool/GrothendieckBessel/Conventions.lean new file mode 100644 index 0000000000..0300aeead7 --- /dev/null +++ b/LeanPool/GrothendieckBessel/Conventions.lean @@ -0,0 +1,66 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import Mathlib.Analysis.InnerProductSpace.Basic +public import Mathlib.MeasureTheory.Integral.Bochner.Set +public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic + +/-! +# Countable Gram-kernel conventions +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + + +noncomputable section + +open MeasureTheory +open scoped BigOperators ComplexConjugate ENNReal + +namespace GrothendieckBessel + +/-- The unit interval `[0,1]`. -/ +def unitInterval : Set ℝ := + Set.Icc (0 : ℝ) 1 + +/-- Lebesgue measure restricted to `[0,1]`. -/ +abbrev μ : Measure ℝ := + volume.restrict unitInterval + +/-- +A Bessel sequence in a complex Hilbert space with bound `1`, expressed by +the standard inequality for all finitely supported coefficient families. +-/ +def BesselSequenceBoundOne + {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] + (x : ℕ → H) : Prop := + ∀ (F : Finset ℕ) (c : ℕ → ℂ), + ‖∑ j ∈ F, c j • x j‖ ^ 2 ≤ ∑ j ∈ F, ‖c j‖ ^ 2 + +/-- Lebesgue measure restricted to a measurable set. -/ +abbrev μOn (S : Set ℝ) : Measure ℝ := + volume.restrict S + +/-- The linear-in-the-first `L²` correlation on a measurable set. -/ +def l2InnerOn (S : Set ℝ) (f g : ℝ → ℂ) : ℂ := + ∫ t, f t * star (g t) ∂μOn S + +/-- +Every finite quadratic form of the kernel is nonnegative and bounded above by +the coefficient `ℓ²` norm. This is the finite positive-contraction condition +used in the compactness argument. +-/ +def FiniteHermitianPositiveContraction {J : Type*} (h : J → J → ℂ) : Prop := + (∀ j k, h k j = star (h j k)) ∧ + ∀ F : Finset J, ∀ c : J → ℂ, + 0 ≤ (F.sum (fun j => F.sum (fun k => c j * star (c k) * h j k))).re ∧ + (F.sum (fun j => F.sum (fun k => c j * star (c k) * h j k))).re ≤ + F.sum (fun j => ‖c j‖ ^ 2) + +end GrothendieckBessel diff --git a/LeanPool/GrothendieckBessel/Definitions.lean b/LeanPool/GrothendieckBessel/Definitions.lean new file mode 100644 index 0000000000..b203e96d63 --- /dev/null +++ b/LeanPool/GrothendieckBessel/Definitions.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import LeanPool.GrothendieckBessel.FiniteAPI + +/-! +# Real and complex matrix quadratic forms +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + +noncomputable section + +open MeasureTheory +open scoped BigOperators ComplexConjugate + +namespace OlevskiiGram + +/-- Dot product on a finite real coordinate space. -/ +def realDot {ι : Type*} [Fintype ι] (x y : ι → ℝ) : ℝ := + ∑ i, x i * y i + +/-- Quadratic form associated to a real matrix. -/ +def realQuadraticForm {ι : Type*} [Fintype ι] (A : Matrix ι ι ℝ) (x : ι → ℝ) : ℝ := + ∑ i, x i * ∑ j, A i j * x j + +/-- Real symmetry for a matrix. -/ +def RealSymmetric {ι : Type*} (A : Matrix ι ι ℝ) : Prop := + ∀ i j, A i j = A j i + +/-- Positive semidefiniteness in quadratic-form language. -/ +def RealPSD {ι : Type*} [Fintype ι] (A : Matrix ι ι ℝ) : Prop := + ∀ x : ι → ℝ, 0 ≤ realQuadraticForm A x + +/-- Loewner order for real matrices, expressed by positive semidefinite difference. -/ +def RealLoewnerLE {ι : Type*} [Fintype ι] (A B : Matrix ι ι ℝ) : Prop := + RealPSD (B - A) + +/-- The real matrix inequality `0 ≤ A ≤ I`. -/ +def RealLoewnerBetweenZeroAndOne {ι : Type*} [Fintype ι] [DecidableEq ι] + (A : Matrix ι ι ℝ) : Prop := + RealPSD A ∧ RealLoewnerLE A 1 + +/-- Coordinatewise membership in the real cube `[-1,1]^ι`. -/ +def InRealUnitCube {ι : Type*} (x : ι → ℝ) : Prop := + ∀ i, |x i| ≤ 1 + +/-- Rank-one real matrix `q qᵀ`. -/ +def realRankOne {ι : Type*} (q : ι → ℝ) : Matrix ι ι ℝ := + fun i j => q i * q j + +/-- Complex Hermitian symmetry, in entrywise form. -/ +def ComplexHermitian {ι : Type*} (A : Matrix ι ι ℂ) : Prop := + ∀ i j, A j i = star (A i j) + +/-- Real part of a complex matrix. -/ +def complexReMatrix {ι : Type*} (A : Matrix ι ι ℂ) : Matrix ι ι ℝ := + fun i j => (A i j).re + +/-- Imaginary part of a complex matrix. -/ +def complexImMatrix {ι : Type*} (A : Matrix ι ι ℂ) : Matrix ι ι ℝ := + fun i j => (A i j).im + +/-- Real part of the complex quadratic form `x* A x`. -/ +def complexQuadraticFormRe {ι : Type*} [Fintype ι] (A : Matrix ι ι ℂ) (x : ι → ℂ) : ℝ := + Complex.re (∑ i, star (x i) * ∑ j, A i j * x j) + +/-- Positive semidefiniteness for complex matrices, stated through quadratic forms. -/ +def ComplexPSD {ι : Type*} [Fintype ι] (A : Matrix ι ι ℂ) : Prop := + ∀ x : ι → ℂ, 0 ≤ complexQuadraticFormRe A x + +/-- The complex matrix inequality `0 ≤ A ≤ I`. -/ +def ComplexLoewnerBetweenZeroAndOne {ι : Type*} [Fintype ι] [DecidableEq ι] + (A : Matrix ι ι ℂ) : Prop := + ComplexPSD A ∧ ComplexPSD (1 - A) + +/-- The real block matrix associated to `A + iB`. -/ +def realBlockMatrix {ι : Type*} (A B : Matrix ι ι ℝ) : + Matrix (Sum ι ι) (Sum ι ι) ℝ + | Sum.inl i, Sum.inl j => A i j + | Sum.inl i, Sum.inr j => -B i j + | Sum.inr i, Sum.inl j => B i j + | Sum.inr i, Sum.inr j => A i j + +end OlevskiiGram diff --git a/LeanPool/GrothendieckBessel/FiniteAPI.lean b/LeanPool/GrothendieckBessel/FiniteAPI.lean new file mode 100644 index 0000000000..391c4be024 --- /dev/null +++ b/LeanPool/GrothendieckBessel/FiniteAPI.lean @@ -0,0 +1,64 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import Mathlib.Analysis.InnerProductSpace.PiL2 +public import Mathlib.MeasureTheory.Function.LpSeminorm.Basic +public import Mathlib.MeasureTheory.Integral.Bochner.Set +public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic + +/-! +# Internal finite Gram API + +Finite Gram matrices, their Euclidean operators, and bounded-function predicates +used by the finite decomposition and realization theorems. +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + + +noncomputable section + +open MeasureTheory +open scoped BigOperators ComplexConjugate + +namespace OlevskiiGram + +/-- Lebesgue measure restricted to the open unit interval. -/ +abbrev μ01 : Measure ℝ := + volume.restrict (Set.Ioo (0 : ℝ) 1) + +/-- The finite Gram matrix, using the paper's inner-product convention. -/ +def gramMatrix {N : ℕ} {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] + (z : Fin N → H) : Matrix (Fin N) (Fin N) ℂ := + fun j k => inner ℂ (z k) (z j) + +/-- The continuous Euclidean operator associated to a finite complex matrix. -/ +def matrixL2Operator {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) : + EuclideanSpace ℂ (Fin N) →L[ℂ] EuclideanSpace ℂ (Fin N) := + LinearMap.toContinuousLinearMap + ((Matrix.toEuclideanLin (𝕜 := ℂ) (m := Fin N) (n := Fin N)) A) + +/-- An upper bound on the Euclidean operator norm of a finite complex matrix. -/ +def matrixL2OperatorNormLE {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (C : ℝ) : Prop := + ‖matrixL2Operator A‖ ≤ C + +/-- An essential supremum bound relative to the open-unit-interval measure. -/ +def LInfNormLe (C : ℝ) (f : ℝ → ℂ) : Prop := + eLpNormEssSup f μ01 ≤ ENNReal.ofReal C + +/-- Bounded functions whose unit-interval correlations represent a finite Gram matrix. -/ +def RepresentsGramMatrixWithBound {N : ℕ} {H : Type*} + [NormedAddCommGroup H] [InnerProductSpace ℂ H] + (C : ℝ) (z : Fin N → H) (f : Fin N → ℝ → ℂ) : Prop := + (∀ j, LInfNormLe C (f j)) ∧ + ∀ j k, + (∫ t in Set.Ioo (0 : ℝ) (1 : ℝ), (f j) t * star ((f k) t)) = + inner ℂ (z k) (z j) + +end OlevskiiGram diff --git a/LeanPool/GrothendieckBessel/FiniteRealization.lean b/LeanPool/GrothendieckBessel/FiniteRealization.lean new file mode 100644 index 0000000000..ef90cbdbc3 --- /dev/null +++ b/LeanPool/GrothendieckBessel/FiniteRealization.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import LeanPool.GrothendieckBessel.Conventions +public import LeanPool.GrothendieckBessel.BallProdromou +public import LeanPool.GrothendieckBessel.ComplexReduction +public import LeanPool.GrothendieckBessel.StepFunctions + +import Mathlib.Tactic.Ring + +/-! +# Finite complex Olevskii realization + +This connects the finite quadratic-form condition to the real and complex +convex decompositions and their bounded measurable step-function realization. +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + + +noncomputable section + +open MeasureTheory +open scoped BigOperators ComplexConjugate ENNReal + +namespace GrothendieckBessel + +private theorem complexQuadraticFormRe_eq_kernelSum + {F : Type*} [Fintype F] + (h : Matrix F F ℂ) (x : F → ℂ) : + OlevskiiGram.complexQuadraticFormRe h x = + (∑ j, ∑ k, star (x j) * star (star (x k)) * h j k).re := by + unfold OlevskiiGram.complexQuadraticFormRe + apply congrArg Complex.re + simp only [Finset.mul_sum] + apply Finset.sum_congr rfl + intro j _hj + apply Finset.sum_congr rfl + intro k _hk + simp only [star_star] + ring + +private theorem complexQuadraticFormRe_one + {F : Type*} [Fintype F] [DecidableEq F] + (x : F → ℂ) : + OlevskiiGram.complexQuadraticFormRe (1 : Matrix F F ℂ) x = + ∑ j, ‖x j‖ ^ 2 := by + rw [complexQuadraticFormRe_eq_kernelSum] + simp only [RCLike.star_def, RingHomCompTriple.comp_apply, RingHom.id_apply, + mul_comm, Matrix.one_apply, + ite_mul, one_mul, zero_mul, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, Complex.mul_conj, + Complex.normSq_eq_norm_sq, Complex.ofReal_pow, Complex.re_sum] + apply Finset.sum_congr rfl + intro j _hj + norm_cast + +private theorem complexQuadraticFormRe_sub + {F : Type*} [Fintype F] + (A B : Matrix F F ℂ) (x : F → ℂ) : + OlevskiiGram.complexQuadraticFormRe (A - B) x = + OlevskiiGram.complexQuadraticFormRe A x - + OlevskiiGram.complexQuadraticFormRe B x := by + unfold OlevskiiGram.complexQuadraticFormRe + rw [← Complex.sub_re] + apply congrArg Complex.re + simp only [Matrix.sub_apply, sub_mul, Finset.sum_sub_distrib, mul_sub] + +/-- The finite-sum positive-contraction condition implies matrix Loewner bounds. -/ +theorem FiniteHermitianPositiveContraction.toComplexLoewner + {F : Type*} [Fintype F] [DecidableEq F] + {h : Matrix F F ℂ} (hh : FiniteHermitianPositiveContraction h) : + OlevskiiGram.ComplexLoewnerBetweenZeroAndOne h := by + constructor + · intro x + have hq := (hh.2 Finset.univ (fun j => star (x j))).1 + rw [complexQuadraticFormRe_eq_kernelSum h x] + simpa [mul_assoc] using hq + · intro x + have hq := (hh.2 Finset.univ (fun j => star (x j))).2 + have hupper : + OlevskiiGram.complexQuadraticFormRe h x ≤ ∑ j, ‖x j‖ ^ 2 := by + rw [complexQuadraticFormRe_eq_kernelSum h x] + simpa [mul_assoc] using hq + rw [complexQuadraticFormRe_sub, complexQuadraticFormRe_one] + exact sub_nonneg.mpr hupper + +/-- +Finite complex Olevskii Gram realization on `[0,1]`, proved from the finite +convex-decomposition development rather than assumed as an axiom. +-/ +theorem finite_complex_olevskii_gram_realization + {F : Type*} [Finite F] + (h : Matrix F F ℂ) + (hh : FiniteHermitianPositiveContraction h) : + ∃ a : F → ℝ → ℂ, + (∀ j, AEStronglyMeasurable (a j) (μOn unitInterval)) ∧ + (∀ j t, t ∈ unitInterval → ‖a j t‖ ≤ 1) ∧ + (∀ j k, l2InnerOn unitInterval (a j) (a k) = h j k) := by + classical + let : Fintype F := Fintype.ofFinite F + have hHerm : OlevskiiGram.ComplexHermitian h := hh.1 + have hLoewner : OlevskiiGram.ComplexLoewnerBetweenZeroAndOne h := + hh.toComplexLoewner + rcases OlevskiiGram.finiteComplexDecomposition h + (OlevskiiGram.hasRealConvexDecomposition (Sum F F)) hHerm hLoewner with + ⟨m, _hm, p, ζ, hp, hpsum, hζ, hentry⟩ + rcases OlevskiiGram.stepFunctionRealizationOnUnitInterval p ζ hp hpsum hζ with + ⟨a, haMeas, haBound, haMoment⟩ + refine ⟨a, haMeas, ?_, ?_⟩ + · intro j t _ht + exact haBound j t + · intro j k + unfold l2InnerOn μOn + change (∫ t in Set.Icc (0 : ℝ) 1, a j t * star (a k t)) = h j k + rw [haMoment j k] + exact (hentry j k).symm + +end GrothendieckBessel diff --git a/LeanPool/GrothendieckBessel/Imports.lean b/LeanPool/GrothendieckBessel/Imports.lean new file mode 100644 index 0000000000..96703d857b --- /dev/null +++ b/LeanPool/GrothendieckBessel/Imports.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ +module -- shake: keep-all --deprecated_module: ignore + +-- Generated project imports; run `lake exe mk_all`. +public import LeanPool.GrothendieckBessel +public import LeanPool.GrothendieckBessel.AbstractBessel +public import LeanPool.GrothendieckBessel.BallProdromou +public import LeanPool.GrothendieckBessel.ComplexReduction +public import LeanPool.GrothendieckBessel.Conventions +public import LeanPool.GrothendieckBessel.Definitions +public import LeanPool.GrothendieckBessel.FiniteAPI +public import LeanPool.GrothendieckBessel.FiniteRealization +public import LeanPool.GrothendieckBessel.MainTheorem +public import LeanPool.GrothendieckBessel.ProbabilityMoments +public import LeanPool.GrothendieckBessel.RealConvex +public import LeanPool.GrothendieckBessel.StepFunctions +public import LeanPool.GrothendieckBessel.UnitIntervalRealization diff --git a/LeanPool/GrothendieckBessel/MainTheorem.lean b/LeanPool/GrothendieckBessel/MainTheorem.lean new file mode 100644 index 0000000000..8b5037090d --- /dev/null +++ b/LeanPool/GrothendieckBessel/MainTheorem.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import LeanPool.GrothendieckBessel.AbstractBessel +public import LeanPool.GrothendieckBessel.UnitIntervalRealization + +/-! +# Countable Grothendieck--Bessel Gram theorem +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + + +noncomputable section + +open MeasureTheory +open scoped BigOperators ComplexConjugate InnerProductSpace + +namespace GrothendieckBessel + +/-- Proof implementation for the single TeX-shaped public theorem. -/ +theorem main_proof + (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] + (x : ℕ → H) (hx : BesselSequenceBoundOne x) : + ∃ f : ℕ → ℝ → ℂ, + (∀ j, AEStronglyMeasurable (f j) μ) ∧ + (∀ j t, t ∈ unitInterval → ‖f j t‖ ≤ 1) ∧ + ∀ j k, + ⟪x k, x j⟫_ℂ = + ∫ t in unitInterval, f j t * star (f k t) := by + have hgram : FiniteHermitianPositiveContraction (besselGram x) := + besselGram_finite_positive_contraction x hx + rcases countable_unit_interval_realization (besselGram x) hgram with + ⟨f, hfMeas, hfBound, hfMoment⟩ + refine ⟨f, hfMeas, hfBound, ?_⟩ + intro j k + have h := hfMoment j k + simpa [besselGram, l2InnerOn, μOn] using h.symm + +end GrothendieckBessel diff --git a/LeanPool/GrothendieckBessel/ProbabilityMoments.lean b/LeanPool/GrothendieckBessel/ProbabilityMoments.lean new file mode 100644 index 0000000000..6a323b4df9 --- /dev/null +++ b/LeanPool/GrothendieckBessel/ProbabilityMoments.lean @@ -0,0 +1,411 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import LeanPool.GrothendieckBessel.FiniteRealization +public import Mathlib.Analysis.InnerProductSpace.EuclideanDist +public import Mathlib.MeasureTheory.Integral.Pi +public import Mathlib.MeasureTheory.Measure.FiniteMeasurePi +public import Mathlib.MeasureTheory.Measure.Prokhorov + +/-! +# Countable moment measures +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + + +noncomputable section + +open MeasureTheory Set Filter Topology +open scoped BigOperators ComplexConjugate ENNReal BoundedContinuousFunction + +namespace GrothendieckBessel + +/-- The closed unit disk in `ℂ`, as a compact measurable subtype. -/ +abbrev ClosedComplexUnitDisk : Type := + Metric.closedBall (0 : ℂ) 1 + +/-- Countable products of the closed complex unit disk. -/ +abbrev ClosedComplexUnitDiskProduct (J : Type*) : Type _ := + J → ClosedComplexUnitDisk + +instance closedComplexUnitDisk_compactSpace : CompactSpace ClosedComplexUnitDisk := + isCompact_iff_compactSpace.mp (isCompact_closedBall (0 : ℂ) 1) + +instance closedComplexUnitDisk_standardBorelSpace : + StandardBorelSpace ClosedComplexUnitDisk := + MeasurableSet.standardBorel Metric.isClosed_closedBall.measurableSet + +instance closedComplexUnitDisk_nonempty : Nonempty ClosedComplexUnitDisk := + ⟨⟨0, by simp⟩⟩ + +/-- Coercions from the closed unit disk have norm at most one. -/ +theorem ClosedComplexUnitDisk.norm_coe_le_one (z : ClosedComplexUnitDisk) : + ‖(z : ℂ)‖ ≤ 1 := by + simpa using (mem_closedBall_zero_iff.mp z.2) + +/-- Package a complex number whose norm is at most one as a point of the closed unit disk. -/ +def Complex.toClosedUnitDisk (z : ℂ) (hz : ‖z‖ ≤ 1) : ClosedComplexUnitDisk := + ⟨z, by simpa [ClosedComplexUnitDisk] using (mem_closedBall_zero_iff.mpr hz)⟩ + +/-- The zero point of the closed complex unit disk. -/ +def zeroClosedComplexUnitDisk : ClosedComplexUnitDisk := + Complex.toClosedUnitDisk 0 (by simp) + +/-- Compact standard Borel structure for the product `closedDisk^J`. -/ +theorem compact_standard_borel_product + (J : Type*) [Countable J] : + CompactSpace (ClosedComplexUnitDiskProduct J) ∧ + StandardBorelSpace (ClosedComplexUnitDiskProduct J) := by + constructor <;> infer_instance + +/-- Compactness of probability measures on a +compact metrizable space. -/ +theorem probability_measures_compact + (X : Type*) [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] + [T2Space X] [BorelSpace X] : + CompactSpace (ProbabilityMeasure X) := by + infer_instance + +/-- The bounded continuous test function for the `(j,k)` moment. -/ +def diskMomentBCF {J : Type*} (j k : J) : + ClosedComplexUnitDiskProduct J →ᵇ ℂ := + BoundedContinuousFunction.mkOfCompact + { toFun := fun x : ClosedComplexUnitDiskProduct J => + ((x j : ClosedComplexUnitDisk) : ℂ) * + star (((x k : ClosedComplexUnitDisk) : ℂ)) + continuous_toFun := by + exact ((continuous_subtype_val.comp (continuous_apply j)).mul + (continuous_star.comp + (continuous_subtype_val.comp (continuous_apply k)))) } + +/-- Complex-valued weak-continuity of integration of a bounded continuous test function. -/ +theorem continuous_probability_integral_complex + {X : Type*} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] + (f : X →ᵇ ℂ) : + Continuous fun μ : ProbabilityMeasure X => ∫ x, f x ∂(μ : Measure X) := by + rw [continuous_iff_continuousAt] + intro μ + exact (ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto ℂ).1 + tendsto_id f + +/-- The map sending a probability measure to its `(j,k)` moment is continuous. -/ +theorem momentIntegral_continuous + {J : Type*} [Countable J] (j k : J) : + Continuous fun μ : ProbabilityMeasure (ClosedComplexUnitDiskProduct J) => + ∫ x, diskMomentBCF j k x ∂(μ : Measure (ClosedComplexUnitDiskProduct J)) := by + exact continuous_probability_integral_complex (diskMomentBCF j k) + +/-- The closed set of probability measures satisfying one prescribed moment. -/ +def momentConstraint + {J : Type*} (h : J → J → ℂ) (j k : J) : + Set (ProbabilityMeasure (ClosedComplexUnitDiskProduct J)) := + {μ | ∫ x, diskMomentBCF j k x ∂(μ : Measure (ClosedComplexUnitDiskProduct J)) = + h j k} + +/-- Closedness of one moment constraint. -/ +theorem closed_moment_constraints + {J : Type*} [Countable J] + (h : J → J → ℂ) (j k : J) : + IsClosed (momentConstraint h j k) := by + exact isClosed_eq (momentIntegral_continuous j k) continuous_const + +/-- +Restriction of a positive-contraction kernel to a finite subtype. This is the +adapter needed before applying the finite Olevskii realization to finitely many +coordinates of a countable kernel. +-/ +theorem FiniteHermitianPositiveContraction.restrictSubtype + {J : Type*} {h : J → J → ℂ} + (hh : FiniteHermitianPositiveContraction h) (S : Finset J) : + FiniteHermitianPositiveContraction + (fun a b : {j // j ∈ S} => h a b) := by + classical + constructor + · intro j k + exact hh.1 j k + · intro F c + let emb : {j // j ∈ S} ↪ J := ⟨Subtype.val, Subtype.val_injective⟩ + let cJ : J → ℂ := fun j => if hj : j ∈ S then c ⟨j, hj⟩ else 0 + have hquad := hh.2 (F.map emb) cJ + have hsum_eq : + (F.map emb).sum + (fun j => (F.map emb).sum + (fun k => cJ j * star (cJ k) * h j k)) = + F.sum (fun j => F.sum + (fun k => c j * star (c k) * h j k)) := by + simp [Finset.sum_map, emb, cJ] + have hnorm_eq : + (F.map emb).sum (fun j => ‖cJ j‖ ^ 2) = + F.sum (fun j => ‖c j‖ ^ 2) := by + simp [Finset.sum_map, emb, cJ] + constructor + · change 0 ≤ + (F.sum (fun j => F.sum + (fun k => c j * star (c k) * h j k))).re + rw [← congrArg Complex.re hsum_eq] + exact hquad.1 + · change + (F.sum (fun j => F.sum + (fun k => c j * star (c k) * h j k))).re ≤ + F.sum (fun j => ‖c j‖ ^ 2) + rw [← congrArg Complex.re hsum_eq, ← hnorm_eq] + exact hquad.2 + +/-- Coordinates appearing in a finite set of requested moment pairs. -/ +def pairCoordinateFinset {J : Type*} [DecidableEq J] + (S : Finset (J × J)) : Finset J := + S.image Prod.fst ∪ S.image Prod.snd + +theorem pairCoordinateFinset_fst_mem + {J : Type*} [DecidableEq J] {S : Finset (J × J)} {p : J × J} + (hp : p ∈ S) : + p.1 ∈ pairCoordinateFinset S := by + exact Finset.mem_union_left _ (Finset.mem_image.mpr ⟨p, hp, rfl⟩) + +theorem pairCoordinateFinset_snd_mem + {J : Type*} [DecidableEq J] {S : Finset (J × J)} {p : J × J} + (hp : p ∈ S) : + p.2 ∈ pairCoordinateFinset S := by + exact Finset.mem_union_right _ (Finset.mem_image.mpr ⟨p, hp, rfl⟩) + +theorem pairCoordinateFinset_nonempty_of_nonempty + {J : Type*} [DecidableEq J] {S : Finset (J × J)} + (hS : S.Nonempty) : + (pairCoordinateFinset S).Nonempty := by + rcases hS with ⟨p, hp⟩ + exact ⟨p.1, pairCoordinateFinset_fst_mem hp⟩ + +/-- The restricted Lebesgue measure on the ambient `[0,1]` is a probability measure. -/ +theorem μOn_unitInterval_isProbabilityMeasure : + IsProbabilityMeasure (μOn unitInterval) := by + constructor + rw [μOn, Measure.restrict_apply_univ] + simp [unitInterval, Real.volume_Icc] + +/-- Build a disk-product sample from finitely many bounded coordinate functions. -/ +def diskProductSample + {J : Type*} [DecidableEq J] + (T : Finset J) + (a : {j // j ∈ T} → ℝ → ℂ) + (ha_bound : ∀ j t, t ∈ unitInterval → ‖a j t‖ ≤ 1) : + ℝ → ClosedComplexUnitDiskProduct J := by + classical + exact fun t j => + if hj : j ∈ T then + if ht : t ∈ unitInterval then + Complex.toClosedUnitDisk (a ⟨j, hj⟩ t) (ha_bound ⟨j, hj⟩ t ht) + else + zeroClosedComplexUnitDisk + else + zeroClosedComplexUnitDisk + +theorem diskProductSample_of_mem + {J : Type*} [DecidableEq J] + {T : Finset J} + {a : {j // j ∈ T} → ℝ → ℂ} + {ha_bound : ∀ j t, t ∈ unitInterval → ‖a j t‖ ≤ 1} + {j : J} (hj : j ∈ T) {t : ℝ} (ht : t ∈ unitInterval) : + ((diskProductSample T a ha_bound t j : ClosedComplexUnitDisk) : ℂ) = + a ⟨j, hj⟩ t := by + classical + simp [diskProductSample, hj, ht, Complex.toClosedUnitDisk] + +/-- The finite disk-product sample map is measurable for the restricted unit-interval measure. -/ +theorem diskProductSample_aemeasurable + {J : Type*} [Countable J] [DecidableEq J] + {T : Finset J} + {a : {j // j ∈ T} → ℝ → ℂ} + {ha_bound : ∀ j t, t ∈ unitInterval → ‖a j t‖ ≤ 1} + (ha_meas : ∀ j, AEStronglyMeasurable (a j) (μOn unitInterval)) : + AEMeasurable (diskProductSample T a ha_bound) (μOn unitInterval) := by + classical + refine AEMeasurable.of_eval ?_ + intro j + by_cases hj : j ∈ T + · have hraw : + AEMeasurable + (fun t => if ht : t ∈ unitInterval then a ⟨j, hj⟩ t else 0) + (μOn unitInterval) := by + refine (ha_meas ⟨j, hj⟩).aemeasurable.congr ?_ + filter_upwards [ae_restrict_mem measurableSet_Icc] with t ht + simp [ht] + have hsub : + AEMeasurable + (fun t => + Complex.toClosedUnitDisk + (if ht : t ∈ unitInterval then a ⟨j, hj⟩ t else 0) + (by + by_cases ht : t ∈ unitInterval + · simpa [ht] using ha_bound ⟨j, hj⟩ t ht + · simp [ht])) + (μOn unitInterval) := + AEMeasurable.subtype_mk hraw + refine hsub.congr ?_ + filter_upwards with t + by_cases ht : t ∈ unitInterval + · simp [diskProductSample, hj, ht, Complex.toClosedUnitDisk] + · simp [diskProductSample, hj, ht, zeroClosedComplexUnitDisk, + Complex.toClosedUnitDisk] + · have hconst : + AEMeasurable (fun _ : ℝ => zeroClosedComplexUnitDisk) + (μOn unitInterval) := + measurable_const.aemeasurable + refine hconst.congr ?_ + filter_upwards with t + simp [diskProductSample, hj] + +/-- Push the restricted unit-interval measure forward through a finite disk-product sample. -/ +def diskProductSampleMeasure + {J : Type*} [Countable J] [DecidableEq J] + (T : Finset J) + (a : {j // j ∈ T} → ℝ → ℂ) + (ha_bound : ∀ j t, t ∈ unitInterval → ‖a j t‖ ≤ 1) + (ha_meas : ∀ j, AEStronglyMeasurable (a j) (μOn unitInterval)) : + ProbabilityMeasure (ClosedComplexUnitDiskProduct J) := by + letI : IsProbabilityMeasure (μOn unitInterval) := + μOn_unitInterval_isProbabilityMeasure + exact + ⟨Measure.map (diskProductSample T a ha_bound) (μOn unitInterval), + (Measure.isProbabilityMeasure_map_iff + (diskProductSample_aemeasurable (T := T) (a := a) + (ha_bound := ha_bound) ha_meas)).mpr inferInstance⟩ + +/-- +Moments of the finite disk-product sample agree with the original finite +coordinate functions for coordinates in the finite coordinate set. +-/ +theorem diskProductSampleMeasure_moment_of_mem + {J : Type*} [Countable J] [DecidableEq J] + {T : Finset J} + {a : {j // j ∈ T} → ℝ → ℂ} + {ha_bound : ∀ j t, t ∈ unitInterval → ‖a j t‖ ≤ 1} + {ha_meas : ∀ j, AEStronglyMeasurable (a j) (μOn unitInterval)} + {j k : J} (hj : j ∈ T) (hk : k ∈ T) : + ∫ x, diskMomentBCF j k x + ∂((diskProductSampleMeasure T a ha_bound ha_meas : + ProbabilityMeasure (ClosedComplexUnitDiskProduct J)) : + Measure (ClosedComplexUnitDiskProduct J)) = + l2InnerOn unitInterval (a ⟨j, hj⟩) (a ⟨k, hk⟩) := by + change + ∫ x, diskMomentBCF j k x + ∂Measure.map (diskProductSample T a ha_bound) (μOn unitInterval) = + ∫ x, a ⟨j, hj⟩ x * star (a ⟨k, hk⟩ x) ∂μOn unitInterval + rw [MeasureTheory.integral_map + (diskProductSample_aemeasurable (T := T) (a := a) + (ha_bound := ha_bound) ha_meas) + (by + exact (diskMomentBCF j k).continuous.measurable.aestronglyMeasurable)] + apply integral_congr_ae + filter_upwards [ae_restrict_mem measurableSet_Icc] with t ht + simp [diskMomentBCF, diskProductSample_of_mem (T := T) (a := a) + (ha_bound := ha_bound) hj ht, + diskProductSample_of_mem (T := T) (a := a) (ha_bound := ha_bound) hk ht] + +/-- +Finite satisfiability of moment constraints, obtained by applying the finite +Olevskii realization theorem to the coordinates appearing in the finite set of pairs and +pushing the restricted unit-interval measure forward to the full disk product. +-/ +theorem finite_moment_constraints_nonempty + {J : Type*} [Countable J] + (h : J → J → ℂ) + (hh : FiniteHermitianPositiveContraction h) + (S : Finset (J × J)) : + (⋂ p ∈ S, momentConstraint h p.1 p.2).Nonempty := by + classical + by_cases hS_empty : S = ∅ + · subst S + let ν : ProbabilityMeasure (ClosedComplexUnitDiskProduct J) := + ⟨Measure.dirac (fun _ => zeroClosedComplexUnitDisk), + Measure.dirac.isProbabilityMeasure⟩ + exact ⟨ν, by simp⟩ + · let T : Finset J := pairCoordinateFinset S + have hhT : + FiniteHermitianPositiveContraction + (fun a b : {j // j ∈ T} => h a b) := + hh.restrictSubtype T + rcases finite_complex_olevskii_gram_realization + (fun a b : {j // j ∈ T} => h a b) hhT with + ⟨a, ha_meas, ha_bound, ha_inner⟩ + let μ : ProbabilityMeasure (ClosedComplexUnitDiskProduct J) := + diskProductSampleMeasure T a ha_bound ha_meas + refine ⟨μ, ?_⟩ + refine mem_iInter.2 ?_ + intro p + refine mem_iInter.2 ?_ + intro hp + have hp_fst : p.1 ∈ T := by + exact pairCoordinateFinset_fst_mem (S := S) hp + have hp_snd : p.2 ∈ T := by + exact pairCoordinateFinset_snd_mem (S := S) hp + change + ∫ x, diskMomentBCF p.1 p.2 x + ∂(μ : Measure (ClosedComplexUnitDiskProduct J)) = + h p.1 p.2 + rw [diskProductSampleMeasure_moment_of_mem + (T := T) (a := a) (ha_bound := ha_bound) (ha_meas := ha_meas) + hp_fst hp_snd] + exact ha_inner ⟨p.1, hp_fst⟩ ⟨p.2, hp_snd⟩ + +/-- Finite intersection property in the compact space of disk-product probability measures. -/ +theorem moment_constraints_all_nonempty_of_finite + {J : Type*} [Countable J] + (h : J → J → ℂ) + (hfinite : ∀ S : Finset (J × J), + (⋂ p ∈ S, momentConstraint h p.1 p.2).Nonempty) : + (⋂ p : J × J, momentConstraint h p.1 p.2).Nonempty := by + exact CompactSpace.iInter_nonempty + (fun p => closed_moment_constraints h p.1 p.2) + (by + intro S + simpa using hfinite S) + +/-- +If every finite family of moment constraints is satisfiable, then there is one +probability measure satisfying all countably many constraints. +-/ +theorem countable_moment_measure_of_finite_satisfiable + {J : Type*} [Countable J] + (h : J → J → ℂ) + (hfinite : ∀ S : Finset (J × J), + (⋂ p ∈ S, momentConstraint h p.1 p.2).Nonempty) : + ∃ μ : ProbabilityMeasure (ClosedComplexUnitDiskProduct J), + ∀ j k, + ∫ x, diskMomentBCF j k x ∂(μ : Measure (ClosedComplexUnitDiskProduct J)) = + h j k := by + rcases moment_constraints_all_nonempty_of_finite h hfinite with ⟨μ, hμ⟩ + refine ⟨μ, ?_⟩ + intro j k + exact show μ ∈ momentConstraint h j k from (mem_iInter.mp hμ (j, k)) + +/-- Finite-intersection step for finitely many moment constraints. -/ +theorem finite_intersection_step + {J : Type*} [Countable J] + (h : J → J → ℂ) + (hh : FiniteHermitianPositiveContraction h) + (S : Finset (J × J)) : + (⋂ p ∈ S, momentConstraint h p.1 p.2).Nonempty := by + classical + exact finite_moment_constraints_nonempty h hh S + +/-- Countable moment measure obtained from finite satisfiability and compactness. -/ +theorem countable_moment_measure + {J : Type*} [Countable J] + (h : J → J → ℂ) + (hh : FiniteHermitianPositiveContraction h) : + ∃ μ : ProbabilityMeasure (ClosedComplexUnitDiskProduct J), + ∀ j k, + ∫ x, diskMomentBCF j k x ∂(μ : Measure (ClosedComplexUnitDiskProduct J)) = + h j k := by + classical + exact countable_moment_measure_of_finite_satisfiable h + (fun S => finite_moment_constraints_nonempty h hh S) + +end GrothendieckBessel diff --git a/LeanPool/GrothendieckBessel/RealConvex.lean b/LeanPool/GrothendieckBessel/RealConvex.lean new file mode 100644 index 0000000000..115c2ba78a --- /dev/null +++ b/LeanPool/GrothendieckBessel/RealConvex.lean @@ -0,0 +1,1648 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import LeanPool.GrothendieckBessel.Definitions +public import Mathlib.Algebra.BigOperators.Pi +public import Mathlib.Analysis.Convex.Caratheodory +public import Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart +public import Mathlib.Analysis.InnerProductSpace.PiL2 +public import Mathlib.Analysis.InnerProductSpace.Projection.Minimal +public import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus +public import Mathlib.Analysis.Matrix.Order +public import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional +public import Mathlib.LinearAlgebra.Basis.VectorSpace + +import Mathlib.Tactic.FunProp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring +import Mathlib.Tactic.Positivity + +/-! +# Constraint polytopes and finite convex decompositions +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + +noncomputable section + +open scoped BigOperators MatrixOrder + +namespace OlevskiiGram + +/-- The constraint polytope cut out by the inequalities `|⟪x,a_j⟫| ≤ 1`. -/ +def constraintPolytope {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) : Set (n → ℝ) := + {x | ∀ j, |realDot x (a j)| ≤ 1} + +/-- The vectors whose constraints are active at `x`. -/ +def activeConstraintVectors {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) (x : n → ℝ) : Set (n → ℝ) := + {v | ∃ j, v = a j ∧ |realDot x (a j)| = 1} + +/-- The span of the active constraint vectors at `x`. -/ +def activeConstraintSpan {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) (x : n → ℝ) : Submodule ℝ (n → ℝ) := + Submodule.span ℝ (activeConstraintVectors a x) + +/-- The finite set of indices whose constraints are active at `x`. -/ +def activeConstraintIndexSet {n ι : Type*} [Fintype n] [Fintype ι] + (a : ι → n → ℝ) (x : n → ℝ) : Finset ι := by + classical + exact Finset.univ.filter fun j => |realDot x (a j)| = 1 + +/-- The number of active constraints at `x`. -/ +def activeConstraintCount {n ι : Type*} [Fintype n] [Fintype ι] + (a : ι → n → ℝ) (x : n → ℝ) : ℕ := + (activeConstraintIndexSet a x).card + +/-- Membership in the finite active-index set is exactly activity of the constraint. -/ +theorem mem_activeConstraintIndexSet_iff + {n ι : Type*} [Fintype n] [Fintype ι] + (a : ι → n → ℝ) (x : n → ℝ) (j : ι) : + j ∈ activeConstraintIndexSet a x ↔ |realDot x (a j)| = 1 := by + classical + simp [activeConstraintIndexSet] + +/-- Adding one genuinely new active index strictly increases the active count. -/ +theorem activeConstraintCount_lt_of_subset_and_new + {n ι : Type*} [Fintype n] [Fintype ι] + (a : ι → n → ℝ) (x y : n → ℝ) + (hsubset : activeConstraintIndexSet a x ⊆ activeConstraintIndexSet a y) + {jNew : ι} + (hjOld : jNew ∉ activeConstraintIndexSet a x) + (hjNew : jNew ∈ activeConstraintIndexSet a y) : + activeConstraintCount a x < activeConstraintCount a y := by + classical + have hne : activeConstraintIndexSet a x ≠ activeConstraintIndexSet a y := by + intro hxy + exact hjOld (by simpa [hxy] using hjNew) + have hssub : + activeConstraintIndexSet a x ⊂ activeConstraintIndexSet a y := + Finset.ssubset_iff_subset_ne.mpr ⟨hsubset, hne⟩ + simpa [activeConstraintCount] using Finset.card_lt_card hssub + +/-- +If all old active constraints remain active and one inactive constraint becomes +active, then the active count strictly increases. +-/ +theorem activeConstraintCount_lt_of_old_active_and_new + {n ι : Type*} [Fintype n] [Fintype ι] + (a : ι → n → ℝ) (x y : n → ℝ) {jNew : ι} + (hold : ∀ j, |realDot x (a j)| = 1 → |realDot y (a j)| = 1) + (hjOldInactive : |realDot x (a jNew)| ≠ 1) + (hjNewActive : |realDot y (a jNew)| = 1) : + activeConstraintCount a x < activeConstraintCount a y := by + classical + apply activeConstraintCount_lt_of_subset_and_new a x y + · intro j hj + rw [mem_activeConstraintIndexSet_iff] at hj ⊢ + exact hold j hj + · rw [mem_activeConstraintIndexSet_iff] + exact hjOldInactive + · rw [mem_activeConstraintIndexSet_iff] + exact hjNewActive + +/-- Predicate for a point maximizing `Φ` on the constraint polytope. -/ +def IsConstraintPolytopeMaximizer {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) (x : n → ℝ) : Prop := + x ∈ constraintPolytope a ∧ + ∀ y : n → ℝ, y ∈ constraintPolytope a → Φ y ≤ Φ x + +/-- Linearity of the finite real dot product in its first argument. -/ +theorem realDot_add {ι : Type*} [Fintype ι] (x y z : ι → ℝ) : + realDot (x + y) z = realDot x z + realDot y z := by + simp [realDot, add_mul, Finset.sum_add_distrib] + +/-- Homogeneity of the finite real dot product in its first argument. -/ +theorem realDot_smul {ι : Type*} [Fintype ι] (c : ℝ) (x y : ι → ℝ) : + realDot (c • x) y = c * realDot x y := by + simp [realDot, Finset.mul_sum, mul_assoc] + +/-- Linearity of the finite real dot product in its second argument. -/ +theorem realDot_add_right {ι : Type*} [Fintype ι] (x y z : ι → ℝ) : + realDot x (y + z) = realDot x y + realDot x z := by + simp [realDot, mul_add, Finset.sum_add_distrib] + +/-- Homogeneity of the finite real dot product in its second argument. -/ +theorem realDot_smul_right {ι : Type*} [Fintype ι] (c : ℝ) (x y : ι → ℝ) : + realDot x (c • y) = c * realDot x y := by + simp [realDot, Finset.mul_sum, mul_left_comm] + +/-- The dot product with a fixed first argument, as a linear functional. -/ +def realDotLinearFunctional {ι : Type*} [Fintype ι] (x : ι → ℝ) : + (ι → ℝ) →ₗ[ℝ] ℝ where + toFun y := realDot x y + map_add' y z := realDot_add_right x y z + map_smul' c y := realDot_smul_right c x y + +/-- A vector with zero dot product against itself is zero. -/ +theorem realDot_self_eq_zero {ι : Type*} [Fintype ι] {x : ι → ℝ} : + realDot x x = 0 ↔ x = 0 := by + constructor + · intro hx + funext i + exact (Finset.sum_mul_self_eq_zero_iff Finset.univ x).mp + (by simpa [realDot] using hx) i (Finset.mem_univ i) + · intro hx + simp [hx, realDot] + +/-- The coordinate vector representing a linear functional via `realDot`. -/ +def dualRepresenter {ι : Type*} + (φ : (ι → ℝ) →ₗ[ℝ] ℝ) : ι → ℝ := by + classical + exact fun i => φ (Pi.single i (1 : ℝ)) + +/-- Every linear functional on a finite coordinate space is represented by `realDot`. -/ +theorem realDot_dualRepresenter {ι : Type*} [Fintype ι] + (φ : (ι → ℝ) →ₗ[ℝ] ℝ) (x : ι → ℝ) : + realDot (dualRepresenter φ) x = φ x := by + classical + calc + realDot (dualRepresenter φ) x + = ∑ i, x i * φ (Pi.single i (1 : ℝ)) := by + simp [realDot, dualRepresenter, mul_comm] + _ = φ (∑ i, x i • Pi.single (M := fun _ => ℝ) i (1 : ℝ)) := by + simp [map_sum] + _ = φ x := by + rw [← pi_eq_sum_univ' x] + +/-- A nonzero functional has a nonzero `realDot` representer. -/ +theorem dualRepresenter_ne_zero {ι : Type*} [Finite ι] + {φ : (ι → ℝ) →ₗ[ℝ] ℝ} : + φ ≠ 0 → dualRepresenter φ ≠ 0 := by + let : Fintype ι := Fintype.ofFinite ι + intro hφ hrep + apply hφ + ext x + have hx := (realDot_dualRepresenter φ x).symm + simpa [hrep, realDot] using hx + +/-- Continuity of the finite real dot product as a function of its first argument. -/ +theorem continuous_realDot_left {ι : Type*} [Fintype ι] (y : ι → ℝ) : + Continuous fun x : ι → ℝ => realDot x y := by + unfold realDot + fun_prop + +/-- The linear map collecting all constraint functionals. -/ +def constraintLinearMap {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) : (n → ℝ) →ₗ[ℝ] (ι → ℝ) where + toFun x j := realDot x (a j) + map_add' x y := by + ext j + exact realDot_add x y (a j) + map_smul' c x := by + ext j + exact realDot_smul c x (a j) + +/-- If the constraint vectors span, then the constraint map is injective. -/ +theorem constraintLinearMap_injective_of_span + {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) : + Function.Injective (constraintLinearMap a) := by + intro x y hxy + suffices x - y = 0 by + exact sub_eq_zero.mp this + apply realDot_self_eq_zero.mp + let φ : (n → ℝ) →ₗ[ℝ] ℝ := realDotLinearFunctional (x - y) + have hmap : constraintLinearMap a (x - y) = 0 := by + rw [map_sub, hxy, sub_self] + have hrange : Set.range a ⊆ φ.ker := by + rintro v ⟨j, rfl⟩ + have hcoord := congrFun hmap j + change realDot (x - y) (a j) = 0 + simpa [constraintLinearMap] using hcoord + have hspan_le : Submodule.span ℝ (Set.range a) ≤ φ.ker := + (Submodule.span_le).2 hrange + have hxmem : x - y ∈ φ.ker := by + have htop_le : (⊤ : Submodule ℝ (n → ℝ)) ≤ φ.ker := by + simpa [hspan] using hspan_le + exact htop_le trivial + exact hxmem + +/-- +If the active span is proper, there is a nonzero direction annihilating every +active constraint vector under `realDot`. +-/ +theorem exists_nonzero_annihilating_activeSpan + {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) (x : n → ℝ) + (hproper : activeConstraintSpan a x ≠ ⊤) : + ∃ h : n → ℝ, + h ≠ 0 ∧ ∀ j, |realDot x (a j)| = 1 → realDot h (a j) = 0 := by + classical + have hlt : activeConstraintSpan a x < ⊤ := lt_top_iff_ne_top.mpr hproper + rcases Submodule.exists_le_ker_of_lt_top (activeConstraintSpan a x) hlt with + ⟨φ, hφne, hleker⟩ + refine ⟨dualRepresenter φ, dualRepresenter_ne_zero hφne, ?_⟩ + intro j hj + have haj_mem : a j ∈ activeConstraintSpan a x := by + exact Submodule.subset_span ⟨j, rfl, hj⟩ + have hφaj : φ (a j) = 0 := hleker haj_mem + simpa [hφaj] using realDot_dualRepresenter φ (a j) + +/-- Active constraints remain active along a direction annihilating them. -/ +theorem activeConstraint_stays_active_along_annihilating_direction + {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) (x h : n → ℝ) + (hh : ∀ j, |realDot x (a j)| = 1 → realDot h (a j) = 0) + {j : ι} (hj : |realDot x (a j)| = 1) (t : ℝ) : + |realDot (x + t • h) (a j)| = 1 := by + have hdot : realDot (x + t • h) (a j) = realDot x (a j) := by + rw [realDot_add, realDot_smul, hh j hj] + ring + rw [hdot, hj] + +/-- A strict scalar inequality has a positive interval of perturbative room. -/ +theorem abs_add_mul_le_one_of_abs_lt_one {u v : ℝ} (hu : |u| < 1) : + ∃ δ : ℝ, 0 < δ ∧ ∀ t : ℝ, |t| ≤ δ → |u + t * v| ≤ 1 := by + let δ : ℝ := (1 - |u|) / (|v| + 1) + have hnum : 0 < 1 - |u| := by linarith + have hden : 0 < |v| + 1 := by positivity + refine ⟨δ, div_pos hnum hden, ?_⟩ + intro t ht + have hvfrac : δ * |v| ≤ 1 - |u| := by + dsimp [δ] + have hle : |v| / (|v| + 1) ≤ 1 := by + rw [div_le_one hden] + linarith [abs_nonneg v] + have hnum_nonneg : 0 ≤ 1 - |u| := le_of_lt hnum + calc + (1 - |u|) / (|v| + 1) * |v| + = (1 - |u|) * (|v| / (|v| + 1)) := by ring + _ ≤ (1 - |u|) * 1 := by + exact mul_le_mul_of_nonneg_left hle hnum_nonneg + _ = 1 - |u| := by ring + calc + |u + t * v| ≤ |u| + |t * v| := abs_add_le _ _ + _ = |u| + |t| * |v| := by rw [abs_mul] + _ ≤ |u| + δ * |v| := by + exact add_le_add le_rfl (mul_le_mul_of_nonneg_right ht (abs_nonneg v)) + _ ≤ |u| + (1 - |u|) := by + exact add_le_add le_rfl hvfrac + _ = 1 := by ring + +/-- A single inactive constraint has a positive interval of allowed motion. -/ +theorem inactiveConstraint_has_room + {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) (x h : n → ℝ) {j : ι} + (hj : |realDot x (a j)| < 1) : + ∃ δ : ℝ, 0 < δ ∧ + ∀ t : ℝ, |t| ≤ δ → |realDot (x + t • h) (a j)| ≤ 1 := by + rcases abs_add_mul_le_one_of_abs_lt_one + (u := realDot x (a j)) (v := realDot h (a j)) hj with + ⟨δ, hδpos, hδ⟩ + refine ⟨δ, hδpos, ?_⟩ + intro t ht + have hdot : + realDot (x + t • h) (a j) = + realDot x (a j) + t * realDot h (a j) := by + rw [realDot_add, realDot_smul] + rw [hdot] + exact hδ t ht + +/-- +If a direction annihilates every active constraint, then a small whole segment +around the base point remains in the constraint polytope. +-/ +theorem constraintPolytope_has_local_line_segment + {n ι : Type*} [Fintype n] [Finite ι] + (a : ι → n → ℝ) (x h : n → ℝ) + (hx : x ∈ constraintPolytope a) + (hh : ∀ j, |realDot x (a j)| = 1 → realDot h (a j) = 0) : + ∃ δ : ℝ, 0 < δ ∧ + ∀ t : ℝ, |t| ≤ δ → x + t • h ∈ constraintPolytope a := by + classical + let : Fintype ι := Fintype.ofFinite ι + have room : + ∀ j : ι, ∃ δ : ℝ, 0 < δ ∧ + ∀ t : ℝ, |t| ≤ δ → |realDot (x + t • h) (a j)| ≤ 1 := by + intro j + by_cases hactive : |realDot x (a j)| = 1 + · refine ⟨1, zero_lt_one, ?_⟩ + intro t _ht + exact le_of_eq + (activeConstraint_stays_active_along_annihilating_direction a x h hh hactive t) + · have hinactive : |realDot x (a j)| < 1 := + lt_of_le_of_ne (hx j) hactive + exact inactiveConstraint_has_room a x h (j := j) hinactive + by_cases huniv : (Finset.univ : Finset ι).Nonempty + · let δOf : ι → ℝ := fun j => Classical.choose (room j) + obtain ⟨j₀, _hj₀mem, hj₀min⟩ := + Finset.exists_min_image (Finset.univ : Finset ι) δOf huniv + refine ⟨δOf j₀, ?_, ?_⟩ + · exact (Classical.choose_spec (room j₀)).1 + · intro t ht j + have hle : |t| ≤ δOf j := by + exact ht.trans (hj₀min j (Finset.mem_univ j)) + exact (Classical.choose_spec (room j)).2 t hle + · refine ⟨1, zero_lt_one, ?_⟩ + intro _t _ht j + exact False.elim (huniv ⟨j, Finset.mem_univ j⟩) + +/-- The constraint polytope always contains the origin. -/ +theorem constraintPolytope_zero_mem {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) : + (0 : n → ℝ) ∈ constraintPolytope a := by + intro j + simp [realDot] + +/-- The constraint polytope is closed. -/ +theorem constraintPolytope_isClosed {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) : + IsClosed (constraintPolytope a) := by + rw [constraintPolytope, Set.ofPred_forall] + exact isClosed_iInter fun j => + isClosed_le ((continuous_realDot_left (a j)).abs) + (continuous_const : Continuous fun _ : n → ℝ => (1 : ℝ)) + +/-- Under the spanning hypothesis, the constraint polytope is bounded. -/ +theorem constraintPolytope_isBounded + {n ι : Type*} [Fintype n] [Finite ι] + (a : ι → n → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) : + Bornology.IsBounded (constraintPolytope a) := by + let : Fintype ι := Fintype.ofFinite ι + rcases (constraintLinearMap a).injective_iff_antilipschitz.mp + (constraintLinearMap_injective_of_span a hspan) with + ⟨K, _hKpos, hanti⟩ + refine isBounded_iff_forall_norm_le.2 ⟨(K : ℝ), ?_⟩ + intro x hx + have hMx : ‖constraintLinearMap a x‖ ≤ (1 : ℝ) := by + rw [pi_norm_le_iff_of_nonneg zero_le_one] + intro j + simpa [constraintLinearMap, Real.norm_eq_abs] using hx j + calc + ‖x‖ ≤ (K : ℝ) * ‖constraintLinearMap a x‖ := by + simpa using hanti.le_mul_norm (map_zero (constraintLinearMap a)) x + _ ≤ (K : ℝ) * 1 := by + exact mul_le_mul_of_nonneg_left hMx K.coe_nonneg + _ = (K : ℝ) := by + rw [mul_one] + +/-- Under the spanning hypothesis, the constraint polytope is compact. -/ +theorem constraintPolytope_isCompact + {n ι : Type*} [Fintype n] [Finite ι] + (a : ι → n → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) : + IsCompact (constraintPolytope a) := + Metric.isCompact_of_isClosed_isBounded + (constraintPolytope_isClosed a) + (constraintPolytope_isBounded a hspan) + +/-- A continuous function on the constraint polytope attains its maximum. -/ +theorem exists_constraintPolytope_maximizer + {n ι : Type*} [Fintype n] [Finite ι] + (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) + (hcont : Continuous Φ) : + ∃ x₀ : n → ℝ, + x₀ ∈ constraintPolytope a ∧ + ∀ x : n → ℝ, x ∈ constraintPolytope a → Φ x ≤ Φ x₀ := by + rcases (constraintPolytope_isCompact a hspan).exists_isMaxOn + ⟨0, constraintPolytope_zero_mem a⟩ hcont.continuousOn with + ⟨x₀, hx₀, hmax⟩ + exact ⟨x₀, hx₀, fun x hx => hmax hx⟩ + +/-- The number of active constraints is bounded by the total number of constraints. -/ +theorem activeConstraintCount_le_card + {n ι : Type*} [Fintype n] [Fintype ι] + (a : ι → n → ℝ) (x : n → ℝ) : + activeConstraintCount a x ≤ Fintype.card ι := by + classical + calc + activeConstraintCount a x + = ((Finset.univ : Finset ι).filter + (fun j => |realDot x (a j)| = 1)).card := by + simp [activeConstraintCount, activeConstraintIndexSet] + _ ≤ (Finset.univ : Finset ι).card := Finset.card_filter_le _ _ + _ = Fintype.card ι := Finset.card_univ + +/-- There is a maximizer whose number of active constraints is maximal. -/ +theorem exists_constraintPolytope_maximizer_max_active + {n ι : Type*} [Fintype n] [Fintype ι] + (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) + (hcont : Continuous Φ) : + ∃ x₀ : n → ℝ, + IsConstraintPolytopeMaximizer a Φ x₀ ∧ + ∀ x : n → ℝ, + IsConstraintPolytopeMaximizer a Φ x → + activeConstraintCount a x ≤ activeConstraintCount a x₀ := by + classical + rcases exists_constraintPolytope_maximizer a Φ hspan hcont with + ⟨x, hxmem, hxmax⟩ + let P : ℕ → Prop := fun k => + ∃ x : n → ℝ, IsConstraintPolytopeMaximizer a Φ x ∧ activeConstraintCount a x = k + have hP : P (activeConstraintCount a x) := + ⟨x, ⟨hxmem, hxmax⟩, rfl⟩ + have hbound : activeConstraintCount a x ≤ Fintype.card ι := + activeConstraintCount_le_card a x + let k₀ := Nat.findGreatest P (Fintype.card ι) + have hk₀P : P k₀ := Nat.findGreatest_spec (P := P) hbound hP + rcases hk₀P with ⟨x₀, hx₀max, hx₀card⟩ + refine ⟨x₀, hx₀max, ?_⟩ + intro y hymax + have hyP : P (activeConstraintCount a y) := ⟨y, hymax, rfl⟩ + have hybound : activeConstraintCount a y ≤ Fintype.card ι := + activeConstraintCount_le_card a y + have hle : activeConstraintCount a y ≤ k₀ := + Nat.le_findGreatest (P := P) hybound hyP + rwa [hx₀card] + +/-- The constraint polytope is convex. -/ +theorem constraintPolytope_convex {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) : + Convex ℝ (constraintPolytope a) := by + rw [convex_iff_add_mem] + intro x hx y hy c d hc hd hcd j + have hxj : |realDot x (a j)| ≤ 1 := hx j + have hyj : |realDot y (a j)| ≤ 1 := hy j + have hlin : + realDot (c • x + d • y) (a j) = + c * realDot x (a j) + d * realDot y (a j) := by + rw [realDot_add, realDot_smul, realDot_smul] + calc + |realDot (c • x + d • y) (a j)| + = |c * realDot x (a j) + d * realDot y (a j)| := by rw [hlin] + _ ≤ |c * realDot x (a j)| + |d * realDot y (a j)| := abs_add_le _ _ + _ = c * |realDot x (a j)| + d * |realDot y (a j)| := by + rw [abs_mul, abs_mul, abs_of_nonneg hc, abs_of_nonneg hd] + _ ≤ c * 1 + d * 1 := by + exact add_le_add + (mul_le_mul_of_nonneg_left hxj hc) + (mul_le_mul_of_nonneg_left hyj hd) + _ = 1 := by + nlinarith + +/-- +If a maximizer is a genuine convex combination of two feasible endpoints, then +both endpoints are maximizers. +-/ +theorem endpoints_are_maximizers_of_convex_combination + {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) + {x₀ xPlus xMinus : n → ℝ} {c d : ℝ} + (hconv : ConvexOn ℝ (constraintPolytope a) Φ) + (hx₀max : IsConstraintPolytopeMaximizer a Φ x₀) + (hxPlus : xPlus ∈ constraintPolytope a) + (hxMinus : xMinus ∈ constraintPolytope a) + (hc : 0 < c) (hd : 0 < d) (hcd : c + d = 1) + (hcomb : x₀ = c • xPlus + d • xMinus) : + IsConstraintPolytopeMaximizer a Φ xPlus ∧ + IsConstraintPolytopeMaximizer a Φ xMinus := by + have hxMinus_le_combo : Φ xMinus ≤ Φ (c • xPlus + d • xMinus) := by + rw [← hcomb] + exact hx₀max.2 xMinus hxMinus + have hx₀_le_xPlus : Φ x₀ ≤ Φ xPlus := by + rw [hcomb] + exact hconv.le_left_of_right_le' hxPlus hxMinus hc hd.le hcd hxMinus_le_combo + have hxPlus_le_combo : Φ xPlus ≤ Φ (c • xPlus + d • xMinus) := by + rw [← hcomb] + exact hx₀max.2 xPlus hxPlus + have hx₀_le_xMinus : Φ x₀ ≤ Φ xMinus := by + rw [hcomb] + exact hconv.le_right_of_left_le' hxPlus hxMinus hc.le hd hcd hxPlus_le_combo + constructor + · exact ⟨hxPlus, fun y hy => (hx₀max.2 y hy).trans hx₀_le_xPlus⟩ + · exact ⟨hxMinus, fun y hy => (hx₀max.2 y hy).trans hx₀_le_xMinus⟩ + +/-- Some spanning constraint has nonzero pairing with every nonzero direction. -/ +theorem exists_constraint_not_annihilated_of_span + {n ι : Type*} [Fintype n] + (a : ι → n → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) + {h : n → ℝ} (hhne : h ≠ 0) : + ∃ j : ι, realDot h (a j) ≠ 0 := by + by_contra hnone + have hall : ∀ j : ι, realDot h (a j) = 0 := by + intro j + by_contra hj + exact hnone ⟨j, hj⟩ + let φ : (n → ℝ) →ₗ[ℝ] ℝ := realDotLinearFunctional h + have hrange : Set.range a ⊆ φ.ker := by + rintro v ⟨j, rfl⟩ + exact hall j + have hspan_le : Submodule.span ℝ (Set.range a) ≤ φ.ker := + (Submodule.span_le).2 hrange + have hhker : h ∈ φ.ker := by + have htop_le : (⊤ : Submodule ℝ (n → ℝ)) ≤ φ.ker := by + simpa [hspan] using hspan_le + exact htop_le trivial + have hself : realDot h h = 0 := by + simpa [φ, realDotLinearFunctional] using hhker + exact hhne (realDot_self_eq_zero.mp hself) + +/-- The positive endpoint time for the scalar inequality `|u + t v| ≤ 1`. -/ +def endpointTimeBound (u v : ℝ) : ℝ := + if 0 < v then (1 - u) / v else (-1 - u) / v + +/-- +For a strictly inactive scalar constraint with nonzero derivative, the endpoint +time is positive. +-/ +theorem endpointTimeBound_pos {u v : ℝ} + (hu : |u| < 1) (hv : v ≠ 0) : + 0 < endpointTimeBound u v := by + by_cases hvpos : 0 < v + · have hnum : 0 < 1 - u := by + have hright := (abs_lt.mp hu).2 + linarith + simp [endpointTimeBound, hvpos, div_pos hnum hvpos] + · have hvneg : v < 0 := lt_of_le_of_ne (le_of_not_gt hvpos) hv + have hnum : -1 - u < 0 := by + have hleft := (abs_lt.mp hu).1 + linarith + simp [endpointTimeBound, hvpos, div_pos_of_neg_of_neg hnum hvneg] + +/-- +If `0 ≤ t` is below the scalar endpoint time, then the corresponding scalar +constraint remains feasible. +-/ +theorem abs_add_mul_le_one_of_le_endpointTimeBound {u v t : ℝ} + (hu : |u| ≤ 1) (htnonneg : 0 ≤ t) + (htle : t ≤ endpointTimeBound u v) : + |u + t * v| ≤ 1 := by + have hu_bounds := abs_le.mp hu + by_cases hvpos : 0 < v + · have hvnonneg : 0 ≤ v := le_of_lt hvpos + have ht_v_le : t * v ≤ 1 - u := by + have hmul := mul_le_mul_of_nonneg_right htle hvnonneg + have hvne : v ≠ 0 := ne_of_gt hvpos + simpa [endpointTimeBound, hvpos, div_mul_cancel₀ (1 - u) hvne] using hmul + have hlower : -1 ≤ u + t * v := by + have htv_nonneg : 0 ≤ t * v := mul_nonneg htnonneg hvnonneg + linarith + have hupper : u + t * v ≤ 1 := by + linarith + exact abs_le.mpr ⟨hlower, hupper⟩ + · by_cases hvzero : v = 0 + · simpa [hvzero] using hu + · have hvneg : v < 0 := lt_of_le_of_ne (le_of_not_gt hvpos) hvzero + have hvnonpos : v ≤ 0 := le_of_lt hvneg + have hbound_v_le : -1 - u ≤ t * v := by + have hmul := mul_le_mul_of_nonpos_right htle hvnonpos + rw [endpointTimeBound, ite_eq_right hvpos] at hmul + rw [div_mul_cancel₀ (-1 - u) hvzero] at hmul + exact hmul + have hlower : -1 ≤ u + t * v := by + linarith + have htv_nonpos : t * v ≤ 0 := mul_nonpos_of_nonneg_of_nonpos htnonneg hvnonpos + have hupper : u + t * v ≤ 1 := by + linarith + exact abs_le.mpr ⟨hlower, hupper⟩ + +/-- At the scalar endpoint time, the scalar constraint is active. -/ +theorem abs_add_endpointTimeBound_mul_eq_one {u v : ℝ} (hv : v ≠ 0) : + |u + endpointTimeBound u v * v| = 1 := by + by_cases hvpos : 0 < v + · have hvne : v ≠ 0 := ne_of_gt hvpos + simp [endpointTimeBound, hvpos, div_mul_cancel₀ (1 - u) hvne] + · have hvneg : v < 0 := lt_of_le_of_ne (le_of_not_gt hvpos) hv + have hvne : v ≠ 0 := ne_of_lt hvneg + simp [endpointTimeBound, hvpos, div_mul_cancel₀ (-1 - u) hvne] + +/-- +Endpoint construction in the active-constraint +maximizer lemma. + +All compactness, local-motion, and convexity/maximizer consequences have been +separated out. This lemma proves the remaining endpoint/geometric part: from +a nonzero feasible perturbation direction, one can find feasible +endpoints whose convex combination is the base point, all old active +constraints remain active at one endpoint, and one genuinely new constraint +becomes active there. +-/ +theorem activeEndpointWithNewActiveConstraint + {n ι : Type*} [Fintype n] [Finite ι] + (a : ι → n → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) + (x₀ : n → ℝ) : + (h : n → ℝ) → + h ≠ 0 → + (∀ j, |realDot x₀ (a j)| = 1 → realDot h (a j) = 0) → + (δ : ℝ) → + 0 < δ → + (∀ t : ℝ, |t| ≤ δ → x₀ + t • h ∈ constraintPolytope a) → + ∃ (xPlus xMinus : n → ℝ) (c d : ℝ) (jNew : ι), + xPlus ∈ constraintPolytope a ∧ + xMinus ∈ constraintPolytope a ∧ + 0 < c ∧ + 0 < d ∧ + c + d = 1 ∧ + x₀ = c • xPlus + d • xMinus ∧ + (∀ j, |realDot x₀ (a j)| = 1 → |realDot xPlus (a j)| = 1) ∧ + |realDot x₀ (a jNew)| ≠ 1 ∧ + |realDot xPlus (a jNew)| = 1 := by + classical + let : Fintype ι := Fintype.ofFinite ι + intro h hhne hhortho δ hδpos hlocal + have hx₀ : x₀ ∈ constraintPolytope a := by + simpa using hlocal 0 (by simpa using le_of_lt hδpos) + let activeDerivativeSet : Finset ι := + (Finset.univ : Finset ι).filter fun j => realDot h (a j) ≠ 0 + have hactiveDerivativeSet_nonempty : activeDerivativeSet.Nonempty := by + rcases exists_constraint_not_annihilated_of_span a hspan hhne with ⟨j, hj⟩ + exact ⟨j, by simp [activeDerivativeSet, hj]⟩ + let u : ι → ℝ := fun j => realDot x₀ (a j) + let v : ι → ℝ := fun j => realDot h (a j) + let scalarBound : ι → ℝ := fun j => endpointTimeBound (u j) (v j) + rcases Finset.exists_min_image activeDerivativeSet scalarBound + hactiveDerivativeSet_nonempty with + ⟨jNew, hjNew_mem, hjNew_min⟩ + have hjNew_v_ne : v jNew ≠ 0 := by + simpa [activeDerivativeSet, v] using hjNew_mem + have inactive_of_mem_activeDerivativeSet : + ∀ {j : ι}, j ∈ activeDerivativeSet → |realDot x₀ (a j)| ≠ 1 := by + intro j hjmem hjactive + have hvne : realDot h (a j) ≠ 0 := by + simpa [activeDerivativeSet] using hjmem + exact hvne (hhortho j hjactive) + have hjNew_inactive : |realDot x₀ (a jNew)| ≠ 1 := + inactive_of_mem_activeDerivativeSet hjNew_mem + have strict_of_mem_activeDerivativeSet : + ∀ {j : ι}, j ∈ activeDerivativeSet → |u j| < 1 := by + intro j hjmem + exact lt_of_le_of_ne (by simpa [u] using hx₀ j) + (by simpa [u] using inactive_of_mem_activeDerivativeSet hjmem) + let τ : ℝ := scalarBound jNew + have hτpos : 0 < τ := by + exact endpointTimeBound_pos + (strict_of_mem_activeDerivativeSet hjNew_mem) hjNew_v_ne + let σ : ℝ := δ / 2 + have hσpos : 0 < σ := by + positivity + let xPlus : n → ℝ := x₀ + τ • h + let xMinus : n → ℝ := x₀ + (-σ) • h + have hxPlus : xPlus ∈ constraintPolytope a := by + intro j + by_cases hvj : v j = 0 + · have hdot : realDot xPlus (a j) = realDot x₀ (a j) := by + simp [xPlus, v, realDot_add, realDot_smul, hvj] + simpa [hdot] using hx₀ j + · have hjmem : j ∈ activeDerivativeSet := by + simp [activeDerivativeSet, v, hvj] + have hτle : τ ≤ scalarBound j := hjNew_min j hjmem + have huj : |u j| ≤ 1 := by + simpa [u] using hx₀ j + have hscalar : + |u j + τ * v j| ≤ 1 := + abs_add_mul_le_one_of_le_endpointTimeBound huj hτpos.le hτle + have hdot : + realDot xPlus (a j) = u j + τ * v j := by + simp [xPlus, u, v, realDot_add, realDot_smul] + simpa [hdot] using hscalar + have hσ_le : |-σ| ≤ δ := by + have hσnonneg : 0 ≤ σ := le_of_lt hσpos + rw [abs_of_nonpos (neg_nonpos.mpr hσnonneg)] + dsimp [σ] + linarith + have hxMinus : xMinus ∈ constraintPolytope a := by + simpa [xMinus, σ] using hlocal (-σ) hσ_le + let c : ℝ := σ / (τ + σ) + let d : ℝ := τ / (τ + σ) + have hsumpos : 0 < τ + σ := add_pos hτpos hσpos + have hcpos : 0 < c := div_pos hσpos hsumpos + have hdpos : 0 < d := div_pos hτpos hsumpos + have hcd : c + d = 1 := by + change σ / (τ + σ) + τ / (τ + σ) = 1 + field_simp [ne_of_gt hsumpos] + ring + have hcomb : x₀ = c • xPlus + d • xMinus := by + ext i + change x₀ i = + σ / (τ + σ) * (x₀ i + τ * h i) + + τ / (τ + σ) * (x₀ i + -σ * h i) + field_simp [ne_of_gt hsumpos] + ring + have hold : ∀ j, |realDot x₀ (a j)| = 1 → |realDot xPlus (a j)| = 1 := by + intro j hj + simpa [xPlus] using + activeConstraint_stays_active_along_annihilating_direction a x₀ h hhortho hj τ + have hjNew_active : |realDot xPlus (a jNew)| = 1 := by + have hdot : + realDot xPlus (a jNew) = u jNew + τ * v jNew := by + simp [xPlus, u, v, realDot_add, realDot_smul] + simpa [hdot, τ, scalarBound] using + abs_add_endpointTimeBound_mul_eq_one hjNew_v_ne + exact ⟨xPlus, xMinus, c, d, jNew, hxPlus, hxMinus, hcpos, hdpos, hcd, + hcomb, hold, hjNew_inactive, hjNew_active⟩ + +/-- The endpoint construction implies the active-count increase used downstream. -/ +theorem activeEndpointWithMoreActiveConstraints + {n ι : Type*} [Fintype n] [Fintype ι] + (a : ι → n → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) + (x₀ : n → ℝ) : + (h : n → ℝ) → + h ≠ 0 → + (∀ j, |realDot x₀ (a j)| = 1 → realDot h (a j) = 0) → + (δ : ℝ) → + 0 < δ → + (∀ t : ℝ, |t| ≤ δ → x₀ + t • h ∈ constraintPolytope a) → + ∃ (xPlus xMinus : n → ℝ) (c d : ℝ), + xPlus ∈ constraintPolytope a ∧ + xMinus ∈ constraintPolytope a ∧ + 0 < c ∧ + 0 < d ∧ + c + d = 1 ∧ + x₀ = c • xPlus + d • xMinus ∧ + activeConstraintCount a x₀ < activeConstraintCount a xPlus := by + intro h hhne hhortho δ hδpos hlocal + rcases activeEndpointWithNewActiveConstraint a hspan x₀ + h hhne hhortho δ hδpos hlocal with + ⟨xPlus, xMinus, c, d, jNew, hxPlus, hxMinus, hc, hd, hcd, hcomb, + hold, hjOldInactive, hjNewActive⟩ + exact ⟨xPlus, xMinus, c, d, hxPlus, hxMinus, hc, hd, hcd, hcomb, + activeConstraintCount_lt_of_old_active_and_new a x₀ xPlus + hold hjOldInactive hjNewActive⟩ + +/-- +Endpoint contradiction after proving the endpoint maximizer fact from convexity. +-/ +theorem activeEndpointContradiction + {n ι : Type*} [Fintype n] [Fintype ι] + (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) + (hconv : ConvexOn ℝ (constraintPolytope a) Φ) + (x₀ : n → ℝ) : + IsConstraintPolytopeMaximizer a Φ x₀ → + (∀ x : n → ℝ, + IsConstraintPolytopeMaximizer a Φ x → + activeConstraintCount a x ≤ activeConstraintCount a x₀) → + (h : n → ℝ) → + h ≠ 0 → + (∀ j, |realDot x₀ (a j)| = 1 → realDot h (a j) = 0) → + (δ : ℝ) → + 0 < δ → + (∀ t : ℝ, |t| ≤ δ → x₀ + t • h ∈ constraintPolytope a) → + False := by + intro hx₀max hx₀card h hhne hhortho δ hδpos hlocal + rcases activeEndpointWithMoreActiveConstraints a hspan x₀ + h hhne hhortho δ hδpos hlocal with + ⟨xPlus, xMinus, c, d, hxPlus, hxMinus, hc, hd, hcd, hcomb, hcount_lt⟩ + have hxPlusMax : + IsConstraintPolytopeMaximizer a Φ xPlus := + (endpoints_are_maximizers_of_convex_combination a Φ hconv hx₀max + hxPlus hxMinus hc hd hcd hcomb).1 + exact (not_lt_of_ge (hx₀card xPlus hxPlusMax)) hcount_lt + +/-- +The perturbation contradiction, reduced to the endpoint part after proving +there is positive room to move inside the polytope. +-/ +theorem activePerturbationContradiction + {n ι : Type*} [Fintype n] [Fintype ι] + (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) + (hconv : ConvexOn ℝ (constraintPolytope a) Φ) + (x₀ : n → ℝ) : + IsConstraintPolytopeMaximizer a Φ x₀ → + (∀ x : n → ℝ, + IsConstraintPolytopeMaximizer a Φ x → + activeConstraintCount a x ≤ activeConstraintCount a x₀) → + (h : n → ℝ) → + h ≠ 0 → + (∀ j, |realDot x₀ (a j)| = 1 → realDot h (a j) = 0) → + False := by + intro hx₀max hx₀card h hhne hhortho + rcases constraintPolytope_has_local_line_segment a x₀ h hx₀max.1 hhortho with + ⟨δ, hδpos, hlocal⟩ + exact activeEndpointContradiction a Φ hspan hconv x₀ + hx₀max hx₀card h hhne hhortho δ hδpos hlocal + +/-- +A maximal-active-cardinality maximizer has full active span via the endpoint +perturbation argument. +-/ +theorem activeSpanTopOfMaximalActiveMaximizer + {n ι : Type*} [Fintype n] [Fintype ι] + (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) + (hconv : ConvexOn ℝ (constraintPolytope a) Φ) + (x₀ : n → ℝ) : + IsConstraintPolytopeMaximizer a Φ x₀ → + (∀ x : n → ℝ, + IsConstraintPolytopeMaximizer a Φ x → + activeConstraintCount a x ≤ activeConstraintCount a x₀) → + activeConstraintSpan a x₀ = ⊤ := by + intro hx₀max hx₀card + by_contra hproper + rcases exists_nonzero_annihilating_activeSpan a x₀ hproper with + ⟨h, hhne, hhortho⟩ + exact activePerturbationContradiction a Φ hspan hconv x₀ + hx₀max hx₀card h hhne hhortho + +/-- +The active-constraint maximizer lemma, proved using the perturbation argument. +-/ +theorem activeConstraintMaximizer + {n ι : Type*} [Fintype n] [Finite ι] + (a : ι → n → ℝ) (Φ : (n → ℝ) → ℝ) + (hspan : Submodule.span ℝ (Set.range a) = ⊤) + (hcont : Continuous Φ) + (hconv : ConvexOn ℝ (constraintPolytope a) Φ) : + ∃ x₀ : n → ℝ, + x₀ ∈ constraintPolytope a ∧ + (∀ x : n → ℝ, x ∈ constraintPolytope a → Φ x ≤ Φ x₀) ∧ + activeConstraintSpan a x₀ = ⊤ := by + let : Fintype ι := Fintype.ofFinite ι + rcases exists_constraintPolytope_maximizer_max_active a Φ hspan hcont with + ⟨x₀, hx₀max, hx₀card⟩ + exact ⟨x₀, hx₀max.1, hx₀max.2, + activeSpanTopOfMaximalActiveMaximizer a Φ hspan hconv x₀ hx₀max hx₀card⟩ + +/-- A compact set lies in a nonempty compact convex set when its support function +is smaller. -/ +theorem supportFunctionSeparation + {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] + (K L : Set V) + (hKcpt : IsCompact K) (hLcpt : IsCompact L) + (hLconv : Convex ℝ L) (hLnonempty : L.Nonempty) + (hsupport : + ∀ a : V, + sSup ((fun x : V => inner ℝ a x) '' K) ≤ + sSup ((fun y : V => inner ℝ a y) '' L)) : + K ⊆ L := by + intro x hxK + by_contra hxL + rcases exists_norm_eq_iInf_of_complete_convex hLnonempty hLcpt.isComplete hLconv x with + ⟨y₀, hy₀L, hy₀min⟩ + let a : V := x - y₀ + have hvariational : ∀ y ∈ L, inner ℝ a (y - y₀) ≤ 0 := by + simpa [a] using (norm_eq_iInf_iff_real_inner_le_zero hLconv hy₀L).mp hy₀min + have hLupper : + ∀ b ∈ ((fun y : V => inner ℝ a y) '' L), b ≤ inner ℝ a y₀ := by + rintro b ⟨y, hyL, rfl⟩ + have hy := hvariational y hyL + have hy' : inner ℝ a y - inner ℝ a y₀ ≤ 0 := by + simpa [inner_sub_right] using hy + linarith + have hLsup_le : + sSup ((fun y : V => inner ℝ a y) '' L) ≤ inner ℝ a y₀ := by + exact csSup_le ⟨inner ℝ a y₀, ⟨y₀, hy₀L, rfl⟩⟩ hLupper + have hKbdd : BddAbove ((fun x : V => inner ℝ a x) '' K) := by + exact hKcpt.bddAbove_image (by fun_prop) + have hx_le_Ksup : inner ℝ a x ≤ sSup ((fun x : V => inner ℝ a x) '' K) := by + exact le_csSup hKbdd ⟨x, hxK, rfl⟩ + have hx_le_y₀ : inner ℝ a x ≤ inner ℝ a y₀ := + hx_le_Ksup.trans ((hsupport a).trans hLsup_le) + have hx_ne_y₀ : x ≠ y₀ := by + intro hxy + apply hxL + simpa [hxy] using hy₀L + have hstrict : inner ℝ a y₀ < inner ℝ a x := by + have hpos : 0 < inner ℝ a x - inner ℝ a y₀ := by + have hdiff : inner ℝ a x - inner ℝ a y₀ = inner ℝ a a := by + rw [← inner_sub_right] + rw [hdiff, real_inner_self_eq_norm_sq] + exact sq_pos_of_ne_zero (norm_ne_zero_iff.mpr (sub_ne_zero.mpr hx_ne_y₀)) + linarith + linarith + +/-- Over the real numbers, matrix star is just transpose. -/ +theorem realMatrix_star_eq_transpose + {n : Type*} (A : Matrix n n ℝ) : + star A = A.transpose := by + ext i j + simp [Matrix.star_apply] + +/-- +For the matrix inner product induced by the identity positive matrix, the +Frobenius pairing is the trace pairing against the transpose. +-/ +theorem matrixInner_eq_trace_transpose_mul + {n : Type*} [Fintype n] [DecidableEq n] + (A G : Matrix n n ℝ) : + letI := Matrix.toMatrixInnerProductSpace + (1 : Matrix n n ℝ) Matrix.PosSemidef.one + inner ℝ A G = (A.transpose * G).trace := by + change (G * (1 : Matrix n n ℝ) * star A).trace = (A.transpose * G).trace + rw [realMatrix_star_eq_transpose A] + rw [Matrix.trace_mul_cycle] + simp + +/-- +The Frobenius support value of a rank-one cube matrix is the associated +quadratic form. +-/ +theorem matrixInner_realRankOne_eq_realQuadraticForm + {n : Type*} [Fintype n] [DecidableEq n] + (A : Matrix n n ℝ) (q : n → ℝ) : + letI := Matrix.toMatrixInnerProductSpace + (1 : Matrix n n ℝ) Matrix.PosSemidef.one + inner ℝ A (realRankOne q) = realQuadraticForm A q := by + change (realRankOne q * (1 : Matrix n n ℝ) * star A).trace = + realQuadraticForm A q + rw [realMatrix_star_eq_transpose A] + rw [Matrix.trace_mul_cycle] + simp only [Matrix.trace, mul_one, Matrix.diag_apply, Matrix.mul_apply, Matrix.transpose_apply, + realRankOne, + realQuadraticForm, Finset.mul_sum] + rw [Finset.sum_comm] + apply Finset.sum_congr rfl + intro i _hi + apply Finset.sum_congr rfl + intro j _hj + ring + +/-- The symmetric part of a real square matrix. -/ +def realSymmPart {d : Type*} (A : Matrix d d ℝ) : Matrix d d ℝ := + fun i j => (A i j + A j i) / 2 + +/-- Rank-one cube matrices, as a subset of the ambient real matrix space. -/ +def realRankOneCubeSet (d : Type*) : Set (Matrix d d ℝ) := + {R | ∃ q : d → ℝ, InRealUnitCube q ∧ R = realRankOne q} + +/-- Flatten a matrix into the Euclidean coordinate space indexed by pairs. -/ +def matrixToEuclidean {d : Type*} (A : Matrix d d ℝ) : + EuclideanSpace ℝ (d × d) := + WithLp.toLp 2 (fun ij : d × d => A (Prod.fst ij) (Prod.snd ij)) + +/-- Unflatten a Euclidean vector indexed by pairs into a matrix. -/ +def euclideanToMatrix {d : Type*} (v : EuclideanSpace ℝ (d × d)) : + Matrix d d ℝ := + fun i j => v (i, j) + +/-- Rank-one cube matrices, flattened into Euclidean space. -/ +def realRankOneCubeEuclideanSet (d : Type*) : + Set (EuclideanSpace ℝ (d × d)) := + Set.image (fun A : Matrix d d ℝ => matrixToEuclidean A) + (realRankOneCubeSet d) + +/-- The coordinate cube `[-1,1]^d` is compact. -/ +theorem isCompact_realUnitCube + {d : Type*} : + IsCompact {q : d → ℝ | InRealUnitCube q} := by + have h : IsCompact {q : d → ℝ | ∀ i, q i ∈ Set.Icc (-1 : ℝ) 1} := by + exact isCompact_pi_infinite (fun _ => isCompact_Icc) + convert h using 1 + ext q + simp [InRealUnitCube, abs_le] + +/-- The rank-one flattening map is continuous on the real cube ambient space. -/ +theorem continuous_matrixToEuclidean_realRankOne + {d : Type*} : + Continuous (fun q : d → ℝ => matrixToEuclidean (realRankOne q)) := by + unfold matrixToEuclidean realRankOne + apply (PiLp.continuous_toLp 2 (fun _ : d × d => ℝ)).comp + apply continuous_pi + intro ij + exact (continuous_apply (Prod.fst ij)).mul + (continuous_apply (Prod.snd ij)) + +/-- The flattened rank-one cube image is compact. -/ +theorem isCompact_realRankOneCubeEuclideanSet + {d : Type*} : + IsCompact (realRankOneCubeEuclideanSet d) := by + have himage : + Set.image (fun q : d → ℝ => matrixToEuclidean (realRankOne q)) + {q : d → ℝ | InRealUnitCube q} = + realRankOneCubeEuclideanSet d := by + ext v + constructor + · rintro ⟨q, hq, rfl⟩ + exact ⟨realRankOne q, ⟨q, hq, rfl⟩, rfl⟩ + · rintro ⟨R, ⟨q, hq, hR⟩, hv⟩ + refine ⟨q, hq, ?_⟩ + rw [← hv, hR] + rw [← himage] + exact isCompact_realUnitCube.image continuous_matrixToEuclidean_realRankOne + +/-- +The set of barycentres of `k` points of `s`, with weights in the standard +simplex. +-/ +def barycentricImageSet {E : Type*} [AddCommMonoid E] [Module ℝ E] + (s : Set E) (k : ℕ) : Set E := + {x | ∃ (w : Fin k → ℝ) (z : Fin k → E), + w ∈ Set.range (fun t : Convexity.StdSimplex ℝ (Fin k) => + (t.weights : Fin k → ℝ)) ∧ (∀ i, z i ∈ s) ∧ ∑ i, w i • z i = x} + +/-- +A finite-dimensional Caratheodory-sized union of barycentric images. +-/ +def finiteBarycentricHull {E : Type*} [AddCommGroup E] [Module ℝ E] + (s : Set E) : Set E := + ⋃ k : Fin (Module.finrank ℝ E + 2), barycentricImageSet s k.1 + +/-- Barycentric images of compact sets are compact. -/ +theorem isCompact_barycentricImageSet + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + {s : Set E} (hs : IsCompact s) (k : ℕ) : + IsCompact (barycentricImageSet s k) := by + let D : Set ((Fin k → ℝ) × (Fin k → E)) := + {x | x.1 ∈ Set.range (fun t : Convexity.StdSimplex ℝ (Fin k) => + (t.weights : Fin k → ℝ)) ∧ ∀ i, x.2 i ∈ s} + have hD : IsCompact D := by + have hw : IsCompact (Set.range (fun t : Convexity.StdSimplex ℝ (Fin k) => + (t.weights : Fin k → ℝ))) := + isCompact_range (Convexity.StdSimplex.isEmbedding_toFun_comp_weights ℝ (Fin k)).continuous + have hz : IsCompact {z : Fin k → E | ∀ i, z i ∈ s} := + isCompact_pi_infinite (fun _ => hs) + have hprod := hw.prod hz + convert hprod using 1 + ext x + rfl + let F : ((Fin k → ℝ) × (Fin k → E)) → E := fun x => ∑ i, x.1 i • x.2 i + have hF : Continuous F := by + dsimp [F] + fun_prop + have himage : F '' D = barycentricImageSet s k := by + ext x + constructor + · rintro ⟨y, hy, rfl⟩ + exact ⟨y.1, y.2, hy.1, hy.2, rfl⟩ + · rintro ⟨w, z, hw, hz, hx⟩ + exact ⟨(w, z), ⟨hw, hz⟩, hx⟩ + rw [← himage] + exact hD.image hF + +/-- +Membership in the convex hull of a finite subset gives an explicit barycentric +image point. +-/ +theorem mem_barycentricImageSet_of_finset_convexHull + {E : Type*} [AddCommGroup E] [Module ℝ E] + {s : Set E} {t : Finset E} {x : E} + (hts : (t : Set E) ⊆ s) (hx : x ∈ convexHull ℝ (t : Set E)) : + x ∈ barycentricImageSet s (Fintype.card t) := by + classical + rw [Finset.convexHull_eq] at hx + rcases hx with ⟨w, hw_nonneg, hsum, hcenter⟩ + let e : t ≃ Fin (Fintype.card t) := Fintype.equivFin t + refine ⟨fun r => w ((e.symm r : t) : E), fun r => ((e.symm r : t) : E), ?_, ?_, ?_⟩ + · simp only [Convexity.StdSimplex.range_toFun_comp_weights, Set.mem_inter_iff, + Set.mem_iInter, Set.mem_ofPred_eq] + have hsum_subtype : ∑ y : t, w (y : E) = 1 := by + rw [← Finset.sum_attach t w] at hsum + simpa using hsum + constructor + · intro r + exact hw_nonneg ((e.symm r : t) : E) (e.symm r).property + · rw [← hsum_subtype] + symm + simpa using Equiv.sum_comp e + (fun r : Fin (Fintype.card t) => w ((e.symm r : t) : E)) + · intro r + exact hts (e.symm r).property + · have hcenter_sum : ∑ y : t, w (y : E) • (y : E) = x := by + rw [Finset.centerMass_eq_of_sum_1 t id hsum] at hcenter + rw [← Finset.sum_attach t (fun y => w y • id y)] at hcenter + simpa using hcenter + rw [← hcenter_sum] + symm + simpa using Equiv.sum_comp e + (fun r : Fin (Fintype.card t) => w ((e.symm r : t) : E) • ((e.symm r : t) : E)) + +/-- In finite dimension, the convex hull is the Caratheodory-sized barycentric union. -/ +theorem convexHull_eq_finiteBarycentricHull + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + [FiniteDimensional ℝ E] (s : Set E) : + convexHull ℝ s = finiteBarycentricHull s := by + classical + ext x + constructor + · intro hx + rw [convexHull_eq_union] at hx + simp only [exists_prop, Set.mem_iUnion] at hx + rcases hx with ⟨t, hts, hAI, hxt⟩ + have hcard : Fintype.card t ≤ Module.finrank ℝ E + 1 := + (hAI.card_le_finrank_succ).trans + (Nat.succ_le_succ (Submodule.finrank_le _)) + refine Set.mem_iUnion.mpr ⟨⟨Fintype.card t, Nat.lt_succ_iff.mpr hcard⟩, ?_⟩ + exact mem_barycentricImageSet_of_finset_convexHull hts hxt + · intro hx + rw [finiteBarycentricHull] at hx + rcases Set.mem_iUnion.mp hx with ⟨k, hk⟩ + rcases hk with ⟨w, z, hw, hz, hsum⟩ + have hw' : (∀ i, 0 ≤ w i) ∧ ∑ i, w i = 1 := by + simpa only [Convexity.StdSimplex.range_toFun_comp_weights, Set.mem_inter_iff, + Set.mem_iInter, Set.mem_ofPred_eq] using hw + exact mem_convexHull_of_exists_fintype w z hw'.1 hw'.2 hz hsum + +/-- The convex hull of a compact set in finite-dimensional real space is compact. -/ +theorem isCompact_convexHull_of_isCompact + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + [FiniteDimensional ℝ E] {s : Set E} (hs : IsCompact s) : + IsCompact (convexHull ℝ s) := by + rw [convexHull_eq_finiteBarycentricHull] + rw [finiteBarycentricHull] + exact isCompact_iUnion fun k => isCompact_barycentricImageSet hs k.1 + +/-- The convex hull of a compact set in finite-dimensional real space is closed. -/ +theorem isClosed_convexHull_of_isCompact + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + [FiniteDimensional ℝ E] {s : Set E} (hs : IsCompact s) : + IsClosed (convexHull ℝ s) := + (isCompact_convexHull_of_isCompact hs).isClosed + +/-- For compact sets in finite dimension, closed convex hull equals convex hull. -/ +theorem closedConvexHull_eq_convexHull_of_isCompact + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + [FiniteDimensional ℝ E] {s : Set E} (hs : IsCompact s) : + closedConvexHull ℝ s = convexHull ℝ s := by + rw [closedConvexHull_eq_closure_convexHull] + exact closure_eq_iff_isClosed.mpr (isClosed_convexHull_of_isCompact hs) + +/-- Flattening and then unflattening a matrix gives the original matrix. -/ +theorem euclideanToMatrix_matrixToEuclidean + {d : Type*} (A : Matrix d d ℝ) : + euclideanToMatrix (matrixToEuclidean A) = A := by + ext i j + simp [euclideanToMatrix, matrixToEuclidean] + +/-- Unflattening and then flattening a Euclidean matrix-vector gives the original vector. -/ +theorem matrixToEuclidean_euclideanToMatrix + {d : Type*} (v : EuclideanSpace ℝ (d × d)) : + matrixToEuclidean (euclideanToMatrix v) = v := by + ext ij + simp [euclideanToMatrix, matrixToEuclidean] + +/-- The symmetric part is symmetric. -/ +theorem realSymmetric_realSymmPart + {d : Type*} (A : Matrix d d ℝ) : + RealSymmetric (realSymmPart A) := by + intro i j + simp [realSymmPart, add_comm] + +/-- Rank-one real matrices are symmetric. -/ +theorem realSymmetric_realRankOne + {d : Type*} (q : d → ℝ) : + RealSymmetric (realRankOne q) := by + intro i j + simp [realRankOne, mul_comm] + +/-- Against a symmetric right factor, `A` and `Aᵀ` have the same trace pairing. -/ +theorem trace_mul_eq_trace_transpose_mul_of_realSymmetric_right + {d : Type*} [Fintype d] + (A T : Matrix d d ℝ) (hT : RealSymmetric T) : + (A * T).trace = (A.transpose * T).trace := by + simp only [Matrix.trace, Matrix.diag_apply, Matrix.mul_apply, Matrix.transpose_apply] + rw [Finset.sum_comm] + apply Finset.sum_congr rfl + intro i _hi + apply Finset.sum_congr rfl + intro j _hj + rw [hT j i] + +/-- The trace pairing with the symmetric part is the average of the two trace pairings. -/ +theorem trace_realSymmPart_mul_eq_average + {d : Type*} [Fintype d] + (A T : Matrix d d ℝ) : + (realSymmPart A * T).trace = + ((A * T).trace + (A.transpose * T).trace) / 2 := by + simp [Matrix.trace, Matrix.mul_apply, realSymmPart, add_mul, div_eq_mul_inv, + Finset.sum_add_distrib, Finset.sum_mul] + ring_nf + +/-- A symmetric right factor only sees the symmetric part of the left factor. -/ +theorem trace_transpose_mul_eq_trace_realSymmPart_mul_of_realSymmetric + {d : Type*} [Fintype d] + (A T : Matrix d d ℝ) (hT : RealSymmetric T) : + (A.transpose * T).trace = (realSymmPart A * T).trace := by + rw [trace_realSymmPart_mul_eq_average] + rw [trace_mul_eq_trace_transpose_mul_of_realSymmetric_right A T hT] + ring + +/-- The quadratic form of a transpose agrees with the original quadratic form. -/ +theorem realQuadraticForm_transpose + {d : Type*} [Fintype d] + (A : Matrix d d ℝ) (q : d → ℝ) : + realQuadraticForm A.transpose q = realQuadraticForm A q := by + simp only [realQuadraticForm, Matrix.transpose_apply, Finset.mul_sum] + rw [Finset.sum_comm] + apply Finset.sum_congr rfl + intro i _hi + apply Finset.sum_congr rfl + intro j _hj + ring + +/-- The quadratic form of the symmetric part is the average of the two transpose forms. -/ +theorem realQuadraticForm_realSymmPart_eq_average + {d : Type*} [Fintype d] + (A : Matrix d d ℝ) (q : d → ℝ) : + realQuadraticForm (realSymmPart A) q = + (realQuadraticForm A q + realQuadraticForm A.transpose q) / 2 := by + simp [realQuadraticForm, realSymmPart, add_mul, mul_add, div_eq_mul_inv, + Finset.sum_add_distrib, Finset.sum_mul, Finset.mul_sum] + ring_nf + +/-- Quadratic forms only see the symmetric part of a real matrix. -/ +theorem realQuadraticForm_realSymmPart + {d : Type*} [Fintype d] + (A : Matrix d d ℝ) (q : d → ℝ) : + realQuadraticForm (realSymmPart A) q = realQuadraticForm A q := by + rw [realQuadraticForm_realSymmPart_eq_average] + rw [realQuadraticForm_transpose] + ring + +/-- The Euclidean inner product of flattened matrices is the trace pairing. -/ +theorem inner_matrixToEuclidean_eq_trace_transpose_mul + {d : Type*} [Fintype d] + (A T : Matrix d d ℝ) : + inner ℝ (matrixToEuclidean A) (matrixToEuclidean T) = + (A.transpose * T).trace := by + classical + simp only [matrixToEuclidean, PiLp.inner_apply, RCLike.inner_apply, conj_trivial, Matrix.trace, + Matrix.diag_apply, Matrix.mul_apply, Matrix.transpose_apply] + rw [Fintype.sum_prod_type] + rw [Finset.sum_comm] + apply Finset.sum_congr rfl + intro i _hi + apply Finset.sum_congr rfl + intro j _hj + ring + +/-- The flattened support value of a rank-one matrix is the quadratic form. -/ +theorem inner_matrixToEuclidean_realRankOne_eq_realQuadraticForm + {d : Type*} [Fintype d] + (A : Matrix d d ℝ) (q : d → ℝ) : + inner ℝ (matrixToEuclidean A) (matrixToEuclidean (realRankOne q)) = + realQuadraticForm A q := by + classical + rw [inner_matrixToEuclidean_eq_trace_transpose_mul] + simp only [Matrix.trace, Matrix.diag_apply, Matrix.mul_apply, Matrix.transpose_apply, + realRankOne, + realQuadraticForm, Finset.mul_sum] + rw [Finset.sum_comm] + apply Finset.sum_congr rfl + intro i _hi + apply Finset.sum_congr rfl + intro j _hj + ring + +/-- A real symmetric matrix is Hermitian in Mathlib's matrix sense. -/ +theorem realSymmetric_isHermitian + {n : Type*} (A : Matrix n n ℝ) : + RealSymmetric A → A.IsHermitian := by + intro hA + rw [Matrix.IsHermitian] + ext i j + exact hA j i + +/-- A real Hermitian matrix is symmetric in entrywise real coordinates. -/ +theorem realSymmetric_of_isHermitian + {n : Type*} (A : Matrix n n ℝ) : + A.IsHermitian → RealSymmetric A := by + intro hA i j + rw [Matrix.IsHermitian] at hA + have hij := congrFun (congrFun hA i) j + simpa using hij.symm + +/-- The explicit Hermitian matrix functional calculus preserves real symmetry. -/ +theorem realSymmetric_cfc + {n : Type*} [Fintype n] [DecidableEq n] + (A : Matrix n n ℝ) (hSym : RealSymmetric A) (f : ℝ → ℝ) : + RealSymmetric ((realSymmetric_isHermitian A hSym).cfc f) := by + apply realSymmetric_of_isHermitian + rw [← Matrix.IsHermitian.cfc_eq] + exact cfc_predicate f A + +/-- The real quadratic-form PSD predicate implies Mathlib's matrix PSD predicate. -/ +theorem realPSD_posSemidef + {n : Type*} [Fintype n] + (A : Matrix n n ℝ) : + RealSymmetric A → RealPSD A → A.PosSemidef := by + intro hSym hPSD + refine Matrix.PosSemidef.of_dotProduct_mulVec_nonneg (realSymmetric_isHermitian A hSym) ?_ + intro x + have hx := hPSD x + simpa [realQuadraticForm, dotProduct, Matrix.vecMul, Matrix.mulVec, + Finset.mul_sum, Finset.sum_mul, mul_assoc, mul_comm, mul_left_comm] using hx + +/-- Mathlib's matrix PSD predicate implies nonnegativity of the real quadratic form. -/ +theorem realPSD_of_posSemidef + {n : Type*} [Fintype n] + (A : Matrix n n ℝ) : + A.PosSemidef → RealPSD A := by + intro hA x + have hx := hA.dotProduct_mulVec_nonneg x + simpa [realQuadraticForm, dotProduct, Matrix.mulVec, + Finset.mul_sum, Finset.sum_mul, mul_assoc, mul_comm, mul_left_comm] using hx + +/-- +If a real function is nonnegative on the spectrum, its Hermitian matrix +functional calculus is positive semidefinite in the project's quadratic-form +sense. +-/ +theorem realPSD_cfc_of_nonneg_spectrum + {n : Type*} [Fintype n] [DecidableEq n] + (A : Matrix n n ℝ) (hSym : RealSymmetric A) (f : ℝ → ℝ) + (hf : ∀ x ∈ spectrum ℝ A, 0 ≤ f x) : + RealPSD ((realSymmetric_isHermitian A hSym).cfc f) := by + rw [← Matrix.IsHermitian.cfc_eq] + exact realPSD_of_posSemidef (cfc f A) + (Matrix.nonneg_iff_posSemidef.mp + (cfc_nonneg (A := Matrix n n ℝ) hf)) + +/-- Trace of the explicit Hermitian matrix functional calculus. -/ +theorem trace_cfc_eq_sum_eigenvalues + {n : Type*} [Fintype n] [DecidableEq n] + (A : Matrix n n ℝ) (hA : A.IsHermitian) (f : ℝ → ℝ) : + (hA.cfc f).trace = ∑ i, f (hA.eigenvalues i) := by + rw [Matrix.IsHermitian.cfc] + rw [Unitary.conjStarAlgAut_apply] + rw [Matrix.trace_mul_cycle] + simp [Matrix.trace_diagonal] + +/-- Mathlib's CFC positive part agrees with the explicit Hermitian matrix `cfc`. -/ +theorem posPart_eq_cfc_posPart + {n : Type*} [Fintype n] [DecidableEq n] + (A : Matrix n n ℝ) (hA : A.IsHermitian) : + A⁺ = hA.cfc (fun x : ℝ => x⁺) := by + rw [CFC.posPart_def] + rw [cfcₙ_eq_cfc] + rw [Matrix.IsHermitian.cfc_eq] + +/-- Trace of the CFC positive part as the sum of positive eigenvalue parts. -/ +theorem trace_posPart_eq_sum_posPart_eigenvalues + {n : Type*} [Fintype n] [DecidableEq n] + (A : Matrix n n ℝ) (hA : A.IsHermitian) : + (A⁺).trace = ∑ i, (hA.eigenvalues i)⁺ := by + rw [posPart_eq_cfc_posPart A hA] + exact trace_cfc_eq_sum_eigenvalues A hA (fun x : ℝ => x⁺) + +/-- +Trace of the CFC positive part, indexed by Mathlib's canonical sorted +eigenvalue list. +-/ +theorem trace_posPart_eq_sum_eigenvalues₀ + {n : Type*} [Fintype n] [DecidableEq n] + (A : Matrix n n ℝ) (hSym : RealSymmetric A) : + (A⁺).trace = + ∑ i : Fin (Fintype.card n), + ((realSymmetric_isHermitian A hSym).eigenvalues₀ i)⁺ := by + have hHerm : A.IsHermitian := realSymmetric_isHermitian A hSym + calc + (A⁺).trace = ∑ i : n, (hHerm.eigenvalues i)⁺ := + trace_posPart_eq_sum_posPart_eigenvalues A hHerm + _ = ∑ i : Fin (Fintype.card n), (hHerm.eigenvalues₀ i)⁺ := by + unfold Matrix.IsHermitian.eigenvalues + exact Equiv.sum_comp + ((Fintype.equivOfCardEq (Fintype.card_fin (Fintype.card n))).symm) + (fun i : Fin (Fintype.card n) => (hHerm.eigenvalues₀ i)⁺) + +/-- The identity matrix is real symmetric. -/ +theorem realSymmetric_one + {n : Type*} [DecidableEq n] : + RealSymmetric (1 : Matrix n n ℝ) := by + intro i j + by_cases hij : i = j + · subst j + simp + · have hji : j ≠ i := fun h => hij h.symm + simp [hij, hji] + +/-- Symmetry is preserved by subtracting from the identity. -/ +theorem realSymmetric_one_sub + {n : Type*} [DecidableEq n] (G : Matrix n n ℝ) : + RealSymmetric G → RealSymmetric (1 - G) := by + intro hG i j + by_cases hij : i = j + · subst j + simp + · have hji : j ≠ i := fun h => hij h.symm + simp [hij, hji, hG i j] + +/-- The zero matrix is real positive semidefinite. -/ +theorem realPSD_zero + {n : Type*} [Fintype n] : + RealPSD (0 : Matrix n n ℝ) := by + intro x + simp [realQuadraticForm] + +/-- The identity matrix is real positive semidefinite. -/ +theorem realPSD_one + {n : Type*} [Fintype n] [DecidableEq n] : + RealPSD (1 : Matrix n n ℝ) := by + intro x + calc + 0 ≤ ∑ i, x i * x i := by + exact Finset.sum_nonneg fun i _ => mul_self_nonneg (x i) + _ = realQuadraticForm (1 : Matrix n n ℝ) x := by + unfold realQuadraticForm + apply Finset.sum_congr rfl + intro i _hi + rw [show (∑ j, (1 : Matrix n n ℝ) i j * x j) = x i by + simp [Matrix.one_apply]] + +/-- The identity matrix satisfies `0 ≤ I ≤ I`. -/ +theorem realLoewnerBetweenZeroAndOne_one + {n : Type*} [Fintype n] [DecidableEq n] : + RealLoewnerBetweenZeroAndOne (1 : Matrix n n ℝ) := by + exact ⟨realPSD_one, by + simpa [RealLoewnerLE] using (realPSD_zero : RealPSD (0 : Matrix n n ℝ))⟩ + +/-- The trace of a product of two real PSD matrices is nonnegative. -/ +theorem positiveSemidefinite_trace_mul_nonneg + {n : Type*} [Fintype n] + (B C : Matrix n n ℝ) : + RealSymmetric B → RealSymmetric C → RealPSD B → RealPSD C → + 0 ≤ (B * C).trace := by + classical + intro hBsym hCsym hBpsd hCpsd + have hBpos : B.PosSemidef := realPSD_posSemidef B hBsym hBpsd + have hCpos : C.PosSemidef := realPSD_posSemidef C hCsym hCpsd + obtain ⟨S, hS⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hCpos.nonneg + rw [hS] + calc + 0 ≤ (S * B * star S).trace := (hBpos.mul_mul_conjTranspose_same S).trace_nonneg + _ = (B * (star S * S)).trace := by + rw [← Matrix.trace_mul_cycle B (star S) S] + rw [Matrix.mul_assoc] + +/-- Trace pairing with a finite convex combination of rank-one matrices. -/ +theorem trace_mul_realConvexCombination + {n : Type*} [Fintype n] + {m : ℕ} (A G : Matrix n n ℝ) (p : Fin m → ℝ) (q : Fin m → n → ℝ) + (hentry : ∀ a b, G a b = ∑ r, p r * q r a * q r b) : + (A * G).trace = ∑ r, p r * realQuadraticForm A (q r) := by + calc + (A * G).trace = ∑ i, ∑ j, A i j * G j i := by + simp [Matrix.trace, Matrix.mul_apply] + _ = ∑ i, ∑ j, A i j * (∑ r, p r * q r j * q r i) := by + simp [hentry] + _ = ∑ i, ∑ j, ∑ r, A i j * (p r * q r j * q r i) := by + simp [Finset.mul_sum] + _ = ∑ r, ∑ i, ∑ j, A i j * (p r * q r j * q r i) := by + rw [show (∑ i, ∑ j, ∑ r, A i j * (p r * q r j * q r i)) = + ∑ i, ∑ r, ∑ j, A i j * (p r * q r j * q r i) by + apply Finset.sum_congr rfl + intro i _hi + rw [Finset.sum_comm]] + rw [Finset.sum_comm] + _ = ∑ r, p r * realQuadraticForm A (q r) := by + simp [realQuadraticForm, Finset.mul_sum, mul_comm, mul_left_comm] + +/-- +The support-function property expected from the positive spectral part of `A`. + +For the paper proof, `Apos` is instantiated as the positive spectral part of +`A`; this predicate packages the required support-function property. +-/ +def HasPositivePartSupportFunction + {n : Type*} [Fintype n] [DecidableEq n] + (A Apos : Matrix n n ℝ) : Prop := + (∀ G : Matrix n n ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ Apos.trace) ∧ + ∃ G : Matrix n n ℝ, + RealSymmetric G ∧ RealLoewnerBetweenZeroAndOne G ∧ + (A * G).trace = Apos.trace + +/-- +For a positive semidefinite test matrix, the support function over `0 ≤ G ≤ I` +is attained at `G = I`. +-/ +theorem hasPositivePartSupportFunction_of_realPSD + {n : Type*} [Fintype n] [DecidableEq n] + (A : Matrix n n ℝ) : + RealSymmetric A → RealPSD A → HasPositivePartSupportFunction A A := by + intro hAsym hApsd + constructor + · intro G hGsym hGbetween + have hnonneg := positiveSemidefinite_trace_mul_nonneg A (1 - G) + hAsym (realSymmetric_one_sub G hGsym) hApsd hGbetween.2 + have htrace : 0 ≤ A.trace - (A * G).trace := by + simpa [Matrix.mul_sub] using hnonneg + linarith + · exact ⟨1, realSymmetric_one, realLoewnerBetweenZeroAndOne_one, by simp⟩ + +/-- +Upper-bound half of the positive/negative spectral-part support-function +argument. This is enough for the convex-hull separation proof once +Ball--Prodromou supplies a cube vector with quadratic value at least +`Apos.trace`. +-/ +theorem supportUpperBound_of_posNegDecomposition + {n : Type*} [Fintype n] [DecidableEq n] + (A Apos Aneg : Matrix n n ℝ) + (hAeq : A = Apos - Aneg) + (hAposSym : RealSymmetric Apos) (hAnegSym : RealSymmetric Aneg) + (hAposPSD : RealPSD Apos) (hAnegPSD : RealPSD Aneg) : + ∀ G : Matrix n n ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ Apos.trace := by + intro G hGsym hGbetween + have hposUpper : (Apos * G).trace ≤ Apos.trace := + (hasPositivePartSupportFunction_of_realPSD Apos hAposSym hAposPSD).1 + G hGsym hGbetween + have hnegNonneg : 0 ≤ (Aneg * G).trace := + positiveSemidefinite_trace_mul_nonneg Aneg G + hAnegSym hGsym hAnegPSD hGbetween.1 + have hsplit : (A * G).trace = (Apos * G).trace - (Aneg * G).trace := by + rw [hAeq] + simp [Matrix.sub_mul] + rw [hsplit] + linarith + +/-- +For a real symmetric matrix, Mathlib's CFC positive part gives the support +upper bound over the Loewner interval `0 ≤ G ≤ I`. +-/ +theorem supportUpperBound_cfc_posPart + {n : Type*} [Fintype n] [DecidableEq n] + (A : Matrix n n ℝ) (hSym : RealSymmetric A) : + ∀ G : Matrix n n ℝ, + RealSymmetric G → RealLoewnerBetweenZeroAndOne G → + (A * G).trace ≤ (A⁺).trace := + supportUpperBound_of_posNegDecomposition A A⁺ A⁻ + (by simpa using (CFC.posPart_sub_negPart A + (realSymmetric_isHermitian A hSym)).symm) + (by + apply realSymmetric_of_isHermitian + exact (CFC.posPart_nonneg A).isSelfAdjoint) + (by + apply realSymmetric_of_isHermitian + exact (CFC.negPart_nonneg A).isSelfAdjoint) + (realPSD_of_posSemidef A⁺ + (Matrix.nonneg_iff_posSemidef.mp (CFC.posPart_nonneg A))) + (realPSD_of_posSemidef A⁻ + (Matrix.nonneg_iff_posSemidef.mp (CFC.negPart_nonneg A))) + +/-- +Abstract positive/negative spectral-part criterion for the support-function +property. The remaining spectral task is to provide `Apos`, `Aneg`, and +`Ppos` satisfying these hypotheses for a real symmetric matrix `A`. +-/ +theorem hasPositivePartSupportFunction_of_posNegProjection + {n : Type*} [Fintype n] [DecidableEq n] + (A Apos Aneg Ppos : Matrix n n ℝ) + (hAeq : A = Apos - Aneg) + (hAposSym : RealSymmetric Apos) (hAnegSym : RealSymmetric Aneg) + (hAposPSD : RealPSD Apos) (hAnegPSD : RealPSD Aneg) + (hPposSym : RealSymmetric Ppos) + (hPposBetween : RealLoewnerBetweenZeroAndOne Ppos) + (hApos_mul_Ppos : Apos * Ppos = Apos) + (hAneg_mul_Ppos : Aneg * Ppos = 0) : + HasPositivePartSupportFunction A Apos := by + constructor + · exact supportUpperBound_of_posNegDecomposition A Apos Aneg hAeq + hAposSym hAnegSym hAposPSD hAnegPSD + · refine ⟨Ppos, hPposSym, hPposBetween, ?_⟩ + rw [hAeq] + simp [Matrix.sub_mul, hApos_mul_Ppos, hAneg_mul_Ppos] + +/-- +The real convex-decomposition theorem as an explicit property. + +This packages the substantial mathematical statement that every real +symmetric matrix with `0 ≤ T ≤ I` should be a finite convex combination of +rank-one matrices `q qᵀ` with `q ∈ [-1,1]^d`. It is established below by +`hasRealConvexDecomposition`. +-/ +def HasRealConvexDecomposition + (d : Type*) [Fintype d] [DecidableEq d] : Prop := + ∀ T : Matrix d d ℝ, + RealSymmetric T → RealLoewnerBetweenZeroAndOne T → + ∃ (m : ℕ) (_hm : 0 < m) (p : Fin m → ℝ) (q : Fin m → d → ℝ), + (∀ r, 0 ≤ p r) ∧ + (∑ r, p r = 1) ∧ + (∀ r, InRealUnitCube (q r)) ∧ + ∀ a b, T a b = ∑ r, p r * q r a * q r b + +/-- +The cube quadratic maximum follows from the support-function maximizer and the +real convex decomposition. +-/ +theorem cubeQuadraticMaximum + {n : Type*} [Fintype n] [DecidableEq n] + (A Apos : Matrix n n ℝ) : + HasRealConvexDecomposition n → + HasPositivePartSupportFunction A Apos → + ∃ x : n → ℝ, + InRealUnitCube x ∧ Apos.trace ≤ realQuadraticForm A x := by + classical + intro hdecomp hsupport + rcases hsupport with ⟨_, hmax⟩ + rcases hmax with ⟨G, hGsym, hGbetween, htrace⟩ + rcases hdecomp G hGsym hGbetween with + ⟨m, hm, p, q, hp, hpsum, hcube, hentry⟩ + have htrace_sum : Apos.trace = ∑ r, p r * realQuadraticForm A (q r) := by + rw [← htrace] + exact trace_mul_realConvexCombination A G p q hentry + have hnonempty : (Finset.univ : Finset (Fin m)).Nonempty := by + exact Finset.univ_nonempty_iff.mpr (Fin.pos_iff_nonempty.mp hm) + rcases Finset.exists_max_image (Finset.univ : Finset (Fin m)) + (fun r => realQuadraticForm A (q r)) hnonempty with + ⟨r₀, _hr₀mem, hr₀max⟩ + refine ⟨q r₀, hcube r₀, ?_⟩ + rw [htrace_sum] + calc + ∑ r, p r * realQuadraticForm A (q r) + ≤ ∑ r, p r * realQuadraticForm A (q r₀) := by + exact Finset.sum_le_sum fun r _hr => + mul_le_mul_of_nonneg_left (hr₀max r (Finset.mem_univ r)) (hp r) + _ = (∑ r, p r) * realQuadraticForm A (q r₀) := by + rw [Finset.sum_mul] + _ = realQuadraticForm A (q r₀) := by + rw [hpsum, one_mul] + +end OlevskiiGram diff --git a/LeanPool/GrothendieckBessel/StepFunctions.lean b/LeanPool/GrothendieckBessel/StepFunctions.lean new file mode 100644 index 0000000000..a0ae8d691e --- /dev/null +++ b/LeanPool/GrothendieckBessel/StepFunctions.lean @@ -0,0 +1,286 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import LeanPool.GrothendieckBessel.Definitions + +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum + +/-! +# Bounded step-function realizations of finite Gram matrices +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + +noncomputable section + +open MeasureTheory +open scoped BigOperators ComplexConjugate + +namespace OlevskiiGram + +private def partialWeight {m : ℕ} (p : Fin m → ℝ) (k : ℕ) : ℝ := + ∑ i ∈ Finset.range k, if h : i < m then p ⟨i, h⟩ else 0 + +private lemma partialWeight_succ {m : ℕ} (p : Fin m → ℝ) {k : ℕ} (hk : k < m) : + partialWeight p (k + 1) = partialWeight p k + p ⟨k, hk⟩ := by + simp [partialWeight, Finset.sum_range_succ, hk] + +private lemma partialWeight_nonneg {m : ℕ} (p : Fin m → ℝ) (hp : ∀ r, 0 ≤ p r) : + ∀ k, 0 ≤ partialWeight p k := by + intro k + dsimp [partialWeight] + exact Finset.sum_nonneg fun i _hi => by + by_cases h : i < m + · simpa [h] using hp ⟨i, h⟩ + · simp [h] + +private lemma partialWeight_mono_succ {m : ℕ} (p : Fin m → ℝ) (hp : ∀ r, 0 ≤ p r) : + ∀ k, partialWeight p k ≤ partialWeight p (k + 1) := by + intro k + by_cases hk : k < m + · rw [partialWeight_succ p hk] + exact le_add_of_nonneg_right (hp ⟨k, hk⟩) + · have hk' : ¬ k < m := hk + rw [partialWeight] + rw [partialWeight] + simp [Finset.sum_range_succ, hk'] + +private lemma partialWeight_mono {m : ℕ} (p : Fin m → ℝ) (hp : ∀ r, 0 ≤ p r) : + Monotone (partialWeight p) := by + intro a b hab + induction b, hab using Nat.le_induction with + | base => rfl + | succ b _ ih => exact ih.trans (partialWeight_mono_succ p hp b) + +private lemma partialWeight_total {m : ℕ} (p : Fin m → ℝ) : + partialWeight p m = ∑ r, p r := by + rw [partialWeight] + rw [Finset.sum_fin_eq_sum_range] + +private def stepInterval {m : ℕ} (p : Fin m → ℝ) (r : Fin m) : Set ℝ := + Set.Ioc (partialWeight p r.1) (partialWeight p (r.1 + 1)) + +private lemma measurableSet_stepInterval {m : ℕ} (p : Fin m → ℝ) (r : Fin m) : + MeasurableSet (stepInterval p r) := by + exact measurableSet_Ioc + +private lemma stepInterval_measureReal {m : ℕ} (p : Fin m → ℝ) + (hp : ∀ r, 0 ≤ p r) (r : Fin m) : + volume.real (stepInterval p r) = p r := by + have hle : partialWeight p r.1 ≤ partialWeight p (r.1 + 1) := + partialWeight_mono_succ p hp r.1 + rw [stepInterval, Real.volume_real_Ioc_of_le hle] + rw [partialWeight_succ p r.2] + ring + +private lemma stepInterval_subset_Ioc {m : ℕ} (p : Fin m → ℝ) + (hp : ∀ r, 0 ≤ p r) (hpsum : ∑ r, p r = 1) (r : Fin m) : + stepInterval p r ⊆ Set.Ioc (0 : ℝ) 1 := by + intro x hx + rcases hx with ⟨hlx, hxu⟩ + constructor + · exact lt_of_le_of_lt (partialWeight_nonneg p hp r.1) hlx + · have hle_total : partialWeight p (r.1 + 1) ≤ partialWeight p m := + partialWeight_mono p hp (Nat.succ_le_of_lt r.2) + rw [partialWeight_total p, hpsum] at hle_total + exact hxu.trans hle_total + +private lemma disjoint_stepInterval {m : ℕ} (p : Fin m → ℝ) (hp : ∀ r, 0 ≤ p r) + {r s : Fin m} (hrs : r ≠ s) : + Disjoint (stepInterval p r) (stepInterval p s) := by + rw [Set.disjoint_left] + intro x hxr hxs + have hval_ne : r.1 ≠ s.1 := by + intro hval + exact hrs (Fin.ext hval) + rcases lt_or_gt_of_ne hval_ne with hlt | hgt + · have hle_rs : r.1 + 1 ≤ s.1 := by omega + have hmono : partialWeight p (r.1 + 1) ≤ partialWeight p s.1 := + partialWeight_mono p hp hle_rs + rcases hxr with ⟨_, hxru⟩ + rcases hxs with ⟨hsl, _⟩ + linarith + · have hle_sr : s.1 + 1 ≤ r.1 := by omega + have hmono : partialWeight p (s.1 + 1) ≤ partialWeight p r.1 := + partialWeight_mono p hp hle_sr + rcases hxs with ⟨_, hxsu⟩ + rcases hxr with ⟨hrl, _⟩ + linarith + +private def finiteStep {m : ℕ} {n : Type*} (p : Fin m → ℝ) (ζ : Fin m → n → ℂ) + (j : n) : ℝ → ℂ := + ∑ r, (stepInterval p r).indicator (fun _ : ℝ => ζ r j) + +private lemma finiteStep_eq_of_mem {m : ℕ} {n : Type*} + (p : Fin m → ℝ) (ζ : Fin m → n → ℂ) (hp : ∀ r, 0 ≤ p r) + {r : Fin m} {t : ℝ} (hr : t ∈ stepInterval p r) (j : n) : + finiteStep p ζ j t = ζ r j := by + classical + rw [finiteStep] + simp only [Finset.sum_apply] + rw [Finset.sum_eq_single (a := r) + (f := fun s => (stepInterval p s).indicator (fun _ : ℝ => ζ s j) t)] + · simp [Set.indicator_of_mem hr] + · intro s _hs hsr + have hnot : t ∉ stepInterval p s := by + intro hts + exact (Set.disjoint_left.mp (disjoint_stepInterval p hp hsr) hts hr) + simp [Set.indicator_of_notMem hnot] + · intro hrmem + simp at hrmem + +private lemma finiteStep_eq_zero_of_notMem {m : ℕ} {n : Type*} + (p : Fin m → ℝ) (ζ : Fin m → n → ℂ) {t : ℝ} + (hnot : ∀ r, t ∉ stepInterval p r) (j : n) : + finiteStep p ζ j t = 0 := by + rw [finiteStep] + simp only [Finset.sum_apply] + refine Finset.sum_eq_zero fun r _hr => ?_ + simp [Set.indicator_of_notMem (hnot r)] + +private lemma finiteStep_norm_le {m : ℕ} {n : Type*} + (p : Fin m → ℝ) (ζ : Fin m → n → ℂ) + (hp : ∀ r, 0 ≤ p r) (hζ : ∀ r j, ‖ζ r j‖ ≤ 1) (j : n) (t : ℝ) : + ‖finiteStep p ζ j t‖ ≤ 1 := by + classical + by_cases hhit : ∃ r, t ∈ stepInterval p r + · rcases hhit with ⟨r, hr⟩ + rw [finiteStep_eq_of_mem p ζ hp hr j] + exact hζ r j + · have hnot : ∀ r, t ∉ stepInterval p r := by + intro r htr + exact hhit ⟨r, htr⟩ + rw [finiteStep_eq_zero_of_notMem p ζ hnot j] + norm_num + +private lemma finiteStep_LInfNormLe {m : ℕ} {n : Type*} + (p : Fin m → ℝ) (ζ : Fin m → n → ℂ) + (hp : ∀ r, 0 ≤ p r) (hζ : ∀ r j, ‖ζ r j‖ ≤ 1) (j : n) : + LInfNormLe 1 (finiteStep p ζ j) := by + unfold LInfNormLe + exact eLpNormEssSup_le_of_ae_bound + (ae_of_all _ fun t => finiteStep_norm_le p ζ hp hζ j t) + +private lemma finiteStep_mul_star_eq {m : ℕ} {n : Type*} + (p : Fin m → ℝ) (ζ : Fin m → n → ℂ) (hp : ∀ r, 0 ≤ p r) (j k : n) (t : ℝ) : + finiteStep p ζ j t * star (finiteStep p ζ k t) = + ∑ r, (stepInterval p r).indicator (fun _ : ℝ => ζ r j * star (ζ r k)) t := by + classical + by_cases hhit : ∃ r, t ∈ stepInterval p r + · rcases hhit with ⟨r, hr⟩ + rw [finiteStep_eq_of_mem p ζ hp hr j, finiteStep_eq_of_mem p ζ hp hr k] + rw [Finset.sum_eq_single (a := r) + (f := fun s => (stepInterval p s).indicator + (fun _ : ℝ => ζ s j * star (ζ s k)) t)] + · simp [Set.indicator_of_mem hr] + · intro s _hs hsr + have hnot : t ∉ stepInterval p s := by + intro hts + exact (Set.disjoint_left.mp (disjoint_stepInterval p hp hsr) hts hr) + simp [Set.indicator_of_notMem hnot] + · intro hrmem + simp at hrmem + · have hnot : ∀ r, t ∉ stepInterval p r := by + intro r htr + exact hhit ⟨r, htr⟩ + rw [finiteStep_eq_zero_of_notMem p ζ hnot j, finiteStep_eq_zero_of_notMem p ζ hnot k] + simp [hnot] + +private lemma finiteStep_integral {m : ℕ} {n : Type*} + (p : Fin m → ℝ) (ζ : Fin m → n → ℂ) + (hp : ∀ r, 0 ≤ p r) (hpsum : ∑ r, p r = 1) (j k : n) : + (∫ t in Set.Ioo (0 : ℝ) (1 : ℝ), finiteStep p ζ j t * star (finiteStep p ζ k t)) = + ∑ r, (p r : ℂ) * ζ r j * star (ζ r k) := by + classical + rw [← MeasureTheory.integral_Ioc_eq_integral_Ioo' (μ := volume) + (f := fun t => finiteStep p ζ j t * star (finiteStep p ζ k t)) + (x := (0 : ℝ)) (y := (1 : ℝ)) (by simp)] + have hfun : + (fun t => finiteStep p ζ j t * star (finiteStep p ζ k t)) = + fun t => ∑ r, (stepInterval p r).indicator + (fun _ : ℝ => ζ r j * star (ζ r k)) t := by + funext t + exact finiteStep_mul_star_eq p ζ hp j k t + rw [hfun] + rw [integral_finsetSum] + · apply Finset.sum_congr rfl + intro r _hr + rw [MeasureTheory.integral_indicator_const (μ := volume.restrict (Set.Ioc (0 : ℝ) 1)) + (e := ζ r j * star (ζ r k)) (s_meas := measurableSet_stepInterval p r)] + rw [measureReal_restrict_apply (μ := volume) (s := Set.Ioc (0 : ℝ) 1) + (t := stepInterval p r) (measurableSet_stepInterval p r)] + rw [Set.inter_eq_left.mpr (stepInterval_subset_Ioc p hp hpsum r)] + rw [stepInterval_measureReal p hp r] + simp [mul_assoc] + · intro r _hr + exact (integrable_const (μ := volume.restrict (Set.Ioc (0 : ℝ) 1)) + (ζ r j * star (ζ r k))).indicator (measurableSet_stepInterval p r) + +/-- +Realize a finite weighted complex Gram decomposition by piecewise constant +functions on `(0,1)`. +-/ +theorem stepFunctionRealization + {n : Type*} + {m : ℕ} + (p : Fin m → ℝ) (ζ : Fin m → n → ℂ) : + (∀ r, 0 ≤ p r) → + (∑ r, p r = 1) → + (∀ r j, ‖ζ r j‖ ≤ 1) → + ∃ f : n → ℝ → ℂ, + (∀ j, LInfNormLe 1 (f j)) ∧ + ∀ j k, + (∫ t in Set.Ioo (0 : ℝ) (1 : ℝ), f j t * star (f k t)) = + ∑ r, (p r : ℂ) * ζ r j * star (ζ r k) + := by + intro hp hpsum hζ + refine ⟨finiteStep p ζ, ?_, ?_⟩ + · intro j + exact finiteStep_LInfNormLe p ζ hp hζ j + · intro j k + exact finiteStep_integral p ζ hp hpsum j k + +/-- +The same finite realization with the concrete measurability and everywhere +pointwise bound needed by the countable compactness construction. The moment +identity is written on `[0,1]`; changing the endpoints does not change a +Lebesgue integral. +-/ +theorem stepFunctionRealizationOnUnitInterval + {n : Type*} + {m : ℕ} + (p : Fin m → ℝ) (ζ : Fin m → n → ℂ) : + (∀ r, 0 ≤ p r) → + (∑ r, p r = 1) → + (∀ r j, ‖ζ r j‖ ≤ 1) → + ∃ f : n → ℝ → ℂ, + (∀ j, AEStronglyMeasurable (f j) + (volume.restrict (Set.Icc (0 : ℝ) 1))) ∧ + (∀ j t, ‖f j t‖ ≤ 1) ∧ + ∀ j k, + (∫ t in Set.Icc (0 : ℝ) (1 : ℝ), f j t * star (f k t)) = + ∑ r, (p r : ℂ) * ζ r j * star (ζ r k) := by + intro hp hpsum hζ + refine ⟨finiteStep p ζ, ?_, ?_, ?_⟩ + · intro j + have hstrong : StronglyMeasurable (finiteStep p ζ j) := by + unfold finiteStep + exact Finset.stronglyMeasurable_sum Finset.univ fun r _ => + (stronglyMeasurable_const : + StronglyMeasurable (fun _ : ℝ => ζ r j)).indicator + (measurableSet_stepInterval p r) + exact hstrong.aestronglyMeasurable + · intro j t + exact finiteStep_norm_le p ζ hp hζ j t + · intro j k + rw [MeasureTheory.integral_Icc_eq_integral_Ioo] + exact finiteStep_integral p ζ hp hpsum j k + +end OlevskiiGram diff --git a/LeanPool/GrothendieckBessel/UnitIntervalRealization.lean b/LeanPool/GrothendieckBessel/UnitIntervalRealization.lean new file mode 100644 index 0000000000..d6c307ae86 --- /dev/null +++ b/LeanPool/GrothendieckBessel/UnitIntervalRealization.lean @@ -0,0 +1,140 @@ +/- +Copyright (c) 2026 Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu +-/ +module + +public import LeanPool.GrothendieckBessel.ProbabilityMoments +public import Mathlib.Probability.Kernel.Representation +import Mathlib.Tactic.Measurability + +/-! +# Realization on the unit interval +Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, +Mathlib API, and compilation changes. +-/ + +@[expose] public section + + +noncomputable section + +open MeasureTheory +open scoped BigOperators ComplexConjugate ENNReal unitInterval + +namespace GrothendieckBessel + +/-- Standard Borel realization of a probability measure by a map from +Mathlib's canonical measured unit interval. -/ +theorem realization_on_unit_interval + (X : Type*) [MeasurableSpace X] [StandardBorelSpace X] + (_nonemptyX : Nonempty X) + (μ : Measure X) [IsProbabilityMeasure μ] : + ∃ f : I → X, Measurable f ∧ Measure.map f volume = μ := by + let := _nonemptyX + exact Measure.exists_measurable_map_eq μ + +/-- Extend one coordinate of a disk-product random variable on Mathlib's +canonical unit interval to an ambient representative on `ℝ`. -/ +def unitIntervalRealizedCoordinate + {J : Type*} + (g : I → ClosedComplexUnitDiskProduct J) (j : J) : ℝ → ℂ := + Function.extend ((↑) : I → ℝ) + (fun x : I => ((g x j : ClosedComplexUnitDisk) : ℂ)) + (fun _ : ℝ => 0) + +theorem unitIntervalRealizedCoordinate_apply + {J : Type*} + (g : I → ClosedComplexUnitDiskProduct J) (j : J) (x : I) : + unitIntervalRealizedCoordinate g j (x : ℝ) = + ((g x j : ClosedComplexUnitDisk) : ℂ) := by + simp [unitIntervalRealizedCoordinate] + +theorem unitIntervalRealizedCoordinate_aestronglyMeasurable + {J : Type*} + {g : I → ClosedComplexUnitDiskProduct J} + (hg_meas : Measurable g) (j : J) : + AEStronglyMeasurable (unitIntervalRealizedCoordinate g j) (μOn unitInterval) := by + have hcoord : Measurable fun x : I => ((g x j : ClosedComplexUnitDisk) : ℂ) := by + measurability + have hext : Measurable (unitIntervalRealizedCoordinate g j) := by + exact unitInterval.measurableEmbedding_coe.measurable_extend hcoord measurable_const + exact hext.aestronglyMeasurable + +theorem unitIntervalRealizedCoordinate_bound + {J : Type*} + (g : I → ClosedComplexUnitDiskProduct J) (j : J) {t : ℝ} + (ht : t ∈ unitInterval) : + ‖unitIntervalRealizedCoordinate g j t‖ ≤ 1 := by + let x : I := ⟨t, by simpa [unitInterval] using ht⟩ + have hx : (x : ℝ) = t := rfl + rw [← hx, unitIntervalRealizedCoordinate_apply] + exact ClosedComplexUnitDisk.norm_coe_le_one (g x j) + +theorem unitIntervalRealizedCoordinate_moment + {J : Type*} [Countable J] + {ν : ProbabilityMeasure (ClosedComplexUnitDiskProduct J)} + {g : I → ClosedComplexUnitDiskProduct J} + (hg_meas : Measurable g) + (hg_map : Measure.map g volume = + (ν : Measure (ClosedComplexUnitDiskProduct J))) + (j k : J) : + l2InnerOn unitInterval (unitIntervalRealizedCoordinate g j) + (unitIntervalRealizedCoordinate g k) = + ∫ x, diskMomentBCF j k x + ∂(ν : Measure (ClosedComplexUnitDiskProduct J)) := by + have hcoe := unitInterval.measurePreserving_coe.integral_comp + unitInterval.measurableEmbedding_coe + (fun t : ℝ => unitIntervalRealizedCoordinate g j t * + star (unitIntervalRealizedCoordinate g k t)) + unfold l2InnerOn + change ∫ t : ℝ, unitIntervalRealizedCoordinate g j t * + star (unitIntervalRealizedCoordinate g k t) ∂μOn unitInterval = + ∫ x, diskMomentBCF j k x ∂(ν : Measure (ClosedComplexUnitDiskProduct J)) + rw [μOn] + change ∫ t : ℝ, unitIntervalRealizedCoordinate g j t * + star (unitIntervalRealizedCoordinate g k t) ∂volume.restrict unitInterval = + ∫ x, diskMomentBCF j k x ∂(ν : Measure (ClosedComplexUnitDiskProduct J)) + have hcoe_unit : + ∫ x : I, unitIntervalRealizedCoordinate g j (x : ℝ) * + star (unitIntervalRealizedCoordinate g k (x : ℝ)) ∂volume = + ∫ t : ℝ, unitIntervalRealizedCoordinate g j t * + star (unitIntervalRealizedCoordinate g k t) ∂volume.restrict unitInterval := by + simpa [unitInterval] using hcoe + rw [← hcoe_unit] + rw [← hg_map] + rw [MeasureTheory.integral_map hg_meas.aemeasurable + (by exact (diskMomentBCF j k).continuous.measurable.aestronglyMeasurable)] + apply integral_congr_ae + filter_upwards with x + simp [diskMomentBCF, unitIntervalRealizedCoordinate_apply] + +/-- +Countable bounded realization of a positive-contraction moment family on the +unit interval. +-/ +theorem countable_unit_interval_realization + {J : Type*} [Countable J] + (h : J → J → ℂ) + (hh : FiniteHermitianPositiveContraction h) : + ∃ f : J → ℝ → ℂ, + (∀ j, AEStronglyMeasurable (f j) (μOn unitInterval)) ∧ + (∀ j t, t ∈ unitInterval → ‖f j t‖ ≤ 1) ∧ + (∀ j k, l2InnerOn unitInterval (f j) (f k) = h j k) := by + rcases countable_moment_measure h hh with ⟨ν, hν⟩ + rcases realization_on_unit_interval + (ClosedComplexUnitDiskProduct J) + (by infer_instance) + (ν : Measure (ClosedComplexUnitDiskProduct J)) with + ⟨g, hg_meas, hg_map⟩ + refine ⟨fun j => unitIntervalRealizedCoordinate g j, ?_, ?_, ?_⟩ + · intro j + exact unitIntervalRealizedCoordinate_aestronglyMeasurable hg_meas j + · intro j t ht + exact unitIntervalRealizedCoordinate_bound g j ht + · intro j k + rw [unitIntervalRealizedCoordinate_moment hg_meas hg_map j k] + exact hν j k + +end GrothendieckBessel diff --git a/LeanPool/projects/grothendieck-bessel.yaml b/LeanPool/projects/grothendieck-bessel.yaml new file mode 100644 index 0000000000..1b5577d43a --- /dev/null +++ b/LeanPool/projects/grothendieck-bessel.yaml @@ -0,0 +1,47 @@ +slug: grothendieck-bessel +title: Grothendieck's theorem for Bessel sequences +summary: Every Bessel sequence with bound one in a complex Hilbert space has its Gram kernel + represented by correlations of measurable functions bounded by one on the unit interval. + The proof includes real and complex finite matrix decompositions, a Ball--Prodromou argument, + and a countable moment-measure construction followed by standard Borel realization. +branch: functional analysis +entry_module: LeanPool.GrothendieckBessel +authors: +- Lukas Liehr +- Mitchell A. Taylor +- Peiyang Yu +source: + title: Grothendieck's theorem for Bessel sequences + authors: + - Lukas Liehr + - Mitchell A. Taylor + - Peiyang Yu + arxiv: '2608.12280' + url: https://github.com/lukasliehr/GrothendieckBessel/tree/f1ad1c7680bce2b1ab4218a02bddd694fb57062a + github_repo: lukasliehr/GrothendieckBessel + commit: f1ad1c7680bce2b1ab4218a02bddd694fb57062a +license: Apache-2.0 +status: verified +provenance: AI +main_declarations: +- GrothendieckBessel.main +main_results: +- declaration: GrothendieckBessel.main + informal: Every countable Bessel sequence with bound one in a complex Hilbert space admits + measurable functions on the unit interval, pointwise bounded by one, whose Lebesgue correlations + equal its Gram kernel. +- declaration: GrothendieckBessel.countable_unit_interval_realization + informal: Every complex kernel on a countable index type whose finite quadratic forms are + Hermitian positive contractions has a bounded measurable realization on the unit interval + with exactly the prescribed correlations. +- declaration: OlevskiiGram.hasRealConvexDecomposition + informal: Every finite real symmetric matrix between zero and the identity is a finite convex + combination of rank-one matrices formed from vectors in the coordinate unit cube. +tags: +- functional-analysis +- bessel-sequences +- gram-matrices +msc: +- 46B15 +- 46B25 +- 46C05