English
There is a canonical isometry between the weighted sum of squares with weights w on Real and the weighted sum with weights sign(w).
Русский
Существуют канонические изометрии между взвешенными суммаx квадратов с весами w и с весами sign(w).
LaTeX
$$$\\text{isometryEquivSignWeightedSumSquares}(w) : \\big(\\text{weightedSumSquares } \\mathbb{R} w\\big) \\cong \\big(\\text{weightedSumSquares } \\mathbb{R} (\\mathrm{sign} \\circ w)\\big)$$$
Lean4
/-- The isometry between a weighted sum of squares with weights `u` on the
(non-zero) real numbers and the weighted sum of squares with weights `sign ∘ u`. -/
noncomputable def isometryEquivSignWeightedSumSquares (w : ι → ℝ) :
IsometryEquiv (weightedSumSquares ℝ w) (weightedSumSquares ℝ (fun i ↦ (sign (w i) : ℝ))) :=
by
let u i := if h : w i = 0 then (1 : ℝˣ) else Units.mk0 (w i) h
have hu : ∀ i : ι, 1 / √|(u i : ℝ)| ≠ 0 := fun i ↦
have : (u i : ℝ) ≠ 0 := (u i).ne_zero
by positivity
have hwu : ∀ i, w i / |(u i : ℝ)| = sign (w i) := fun i ↦
by
by_cases hi : w i = 0
· simp [hi]
· simp only [hi, ↓reduceDIte, Units.val_mk0, u]; field_simp; simp
convert
QuadraticMap.isometryEquivBasisRepr (weightedSumSquares ℝ w) ((Pi.basisFun ℝ ι).unitsSMul fun i => .mk0 _ (hu i))
ext1 v
classical
suffices ∑ i, (w i / |(u i : ℝ)|) * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |(u i : ℝ)|⁻¹) by
simpa [basisRepr_apply, Basis.unitsSMul_apply, ← _root_.sq, mul_pow, ← hwu, Pi.single_apply]
exact sum_congr rfl fun j _ ↦ by ring
