Ball's determinant lemma in Lean: Cauchy–Binet weights + Jensen, count via t = 2 at one index

To prove ∏ tᵢ^cᵢ ≤ det(∑ cᵢtᵢ uᵢ⊗uᵢ) when ∑cᵢuᵢ⊗uᵢ = I (unit uᵢ), write toMatrix in an orthonormal basis as A*B with A j i = ⟪b j,uᵢ⟫ cᵢtᵢ and B i j = ⟪b j,uᵢ⟫. Unordered Cauchy–Binet then gives det = ∑_{p : Fin d → ι} w_p ∏ⱼ t(p j), where w_p = (∏ c(p j)) det(U.submatrix id p)² / d!. At t = 1 the map is id, so ∑ w_p = 1, and Jensen (strictConcaveOn_log_Ioi.concaveOn.le_map_sum) handles the log. The non-obvious step is showing ∑_p w_p #{j | p j = i} = cᵢ without derivatives. Plug in t = 2 at i and 1 elsewhere. The map becomes stretch uᵢ (1+cᵢ) 1, of determinant 1+cᵢ. Non-injective p have w_p = 0 (Matrix.det_zero_of_column_eq), so ∏ⱼ t(p j) = 1 + #{j | p j = i} for every p that matters (prod_eq_single / sum_eq_single). Comparing the two sides gives the count. Lean details: the submatrix-of-a-let-matrix ext goals close by rfl (simp leaves Matrix.submatrix (fun ..) id p j j'). Also, rw [← hI z] rewrites z everywhere, so use conv_rhs. if_true/if_false are deprecated, use ite_true/ite_false.