English
There exists a real-linear isometry rightAngleRotationAux₂ extending the auxiliary right-angle rotation, preserving norms: for all x, ∥o.rightAngleRotationAux₂ x∥ = ∥x∥.
Русский
Существует линейная изометрия rightAngleRotationAux₂, сохраняющая нормы: для всех x выполняется ∥o.rightAngleRotationAux₂ x∥ = ∥x∥.
LaTeX
$$$\\\\|o.rightAngleRotationAux₂ x\\\\| = \\\\|x\\\\| \\\\quad\\forall x \\\\, x \u2208 E$$$
Lean4
/-- Auxiliary construction for `Orientation.rightAngleRotation`, rotation by 90 degrees in an
oriented real inner product space of dimension 2. -/
def rightAngleRotationAux₂ : E →ₗᵢ[ℝ] E :=
{ o.rightAngleRotationAux₁ with
norm_map' := fun x => by
refine le_antisymm ?_ ?_
· rcases eq_or_lt_of_le (norm_nonneg (o.rightAngleRotationAux₁ x)) with h | h
· rw [← h]
positivity
refine le_of_mul_le_mul_right ?_ h
rw [← real_inner_self_eq_norm_mul_norm, o.inner_rightAngleRotationAux₁_left]
exact o.areaForm_le x (o.rightAngleRotationAux₁ x)
· let K : Submodule ℝ E := ℝ ∙ x
have : Nontrivial Kᗮ := by
apply nontrivial_of_finrank_pos (R := ℝ)
have : finrank ℝ K ≤ Finset.card { x } :=
by
rw [← Set.toFinset_singleton]
exact finrank_span_le_card ({ x } : Set E)
have : Finset.card { x } = 1 := Finset.card_singleton x
have : finrank ℝ K + finrank ℝ Kᗮ = finrank ℝ E := K.finrank_add_finrank_orthogonal
have : finrank ℝ E = 2 := Fact.out
omega
obtain ⟨w, hw₀⟩ : ∃ w : Kᗮ, w ≠ 0 := exists_ne 0
have hw' : ⟪x, (w : E)⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
have hw : (w : E) ≠ 0 := fun h => hw₀ (Submodule.coe_eq_zero.mp h)
refine le_of_mul_le_mul_right ?_ (by rwa [norm_pos_iff] : 0 < ‖(w : E)‖)
rw [← o.abs_areaForm_of_orthogonal hw']
rw [← o.inner_rightAngleRotationAux₁_left x w]
exact abs_real_inner_le_norm (o.rightAngleRotationAux₁ x) w }
