isometryEquivSumSquares — Mathlib

English

There exists an isometry between the weighted sum of squares with weights w′: ι → ℂ and the weighted sum of squares with 0-1 weights given by the indicator of being nonzero: w(i) = 0 if w′(i) = 0, else 1.

Русский

Существует изометрия между взвешенной суммой квадратов с весами w′ и взвешенной суммой квадратов с весами 0/1, задаваемыми индикатором не нуля.

LaTeX

$$$ IsometryEquiv\\ (weightedSumSquares\\ ℂ\\ w')\\ (weightedSumSquares\\ ℂ\\ (\\lambda i. if w'(i)=0 then 0 else 1)) $$$

Lean4

/-- The isometry between a weighted sum of squares on the complex numbers and the
sum of squares, i.e. `weightedSumSquares` with weights 1 or 0. -/
noncomputable def isometryEquivSumSquares (w' : ι → ℂ) :
    IsometryEquiv (weightedSumSquares ℂ w') (weightedSumSquares ℂ (fun i => if w' i = 0 then 0 else 1 : ι → ℂ)) :=
  by
  let w i := if h : w' i = 0 then (1 : Units ℂ) else Units.mk0 (w' i) h
  have hw' : ∀ i : ι, (w i : ℂ) ^ (-(1 / 2 : ℂ)) ≠ 0 :=
    by
    intro i hi
    exact (w i).ne_zero ((Complex.cpow_eq_zero_iff _ _).1 hi).1
  convert
    QuadraticMap.isometryEquivBasisRepr (weightedSumSquares ℂ w')
      ((Pi.basisFun ℂ ι).unitsSMul fun i => (isUnit_iff_ne_zero.2 <| hw' i).unit)
  ext1 v
  rw [basisRepr_apply, weightedSumSquares_apply, weightedSumSquares_apply]
  refine sum_congr rfl fun j hj => ?_
  have hsum :
    (∑ i : ι, v i • ((isUnit_iff_ne_zero.2 <| hw' i).unit : ℂ) • (Pi.basisFun ℂ ι) i) j = v j • w j ^ (-(1 / 2 : ℂ)) :=
    by
    classical
    rw [Finset.sum_apply, sum_eq_single j, Pi.basisFun_apply, IsUnit.unit_spec, Pi.smul_apply, Pi.smul_apply,
      Pi.single_eq_same, smul_eq_mul, smul_eq_mul, smul_eq_mul, mul_one]
    · intro i _ hij
      rw [Pi.basisFun_apply, Pi.smul_apply, Pi.smul_apply, Pi.single_eq_of_ne hij.symm, smul_eq_mul, smul_eq_mul,
        mul_zero, mul_zero]
    intro hj'; exact False.elim (hj' hj)
  simp_rw [Module.Basis.unitsSMul_apply]
  erw [hsum, smul_eq_mul]
  split_ifs with h
  · simp only [h, zero_smul, zero_mul]
  have hww' : w' j = w j := by simp only [w, dif_neg h, Units.val_mk0]
  simp -zeta only [one_mul, smul_eq_mul]
  rw [hww']
  suffices v j * v j = w j ^ (-(1 / 2 : ℂ)) * w j ^ (-(1 / 2 : ℂ)) * w j * v j * v j by rw [this]; ring
  rw [← Complex.cpow_add _ _ (w j).ne_zero, show -(1 / 2 : ℂ) + -(1 / 2) = -1 by simp [← two_mul], Complex.cpow_neg_one,
    inv_mul_cancel₀ (w j).ne_zero, one_mul]

Похожие утверждения