EuclideanCertificateCoordinates.lean

1 import Mathlib.Analysis.InnerProductSpace.PiL2
2 import Mathlib.Analysis.Normed.Module.FiniteDimension
3 import Mathlib.Tactic.FinCases
4 import Mathlib.Tactic.Ring
5 
6 set_option autoImplicit false
7 
8 /-! Explicit Euclidean coordinates for generated exact polynomial certificates.
9 There is no change from the Euclidean norm to the coordinate maximum norm. -/
10 noncomputable section
11 namespace KomorebiSpace
12 namespace ExactCoordinates
13 abbrev Space (n : ℕ) := EuclideanSpace ℝ (Fin n)
14 
15 def linear (n : ℕ) (a : Fin n → Fin n → ℝ) : Space n →ₗ[ℝ] Space n where
16   toFun x := WithLp.toLp 2 (fun i => ∑ j, a i j*x j)
17   map_add' x y := by
18     ext i
19     change (∑ j, a i j * (x j+y j))=(∑ j,a i j*x j)+(∑ j,a i j*y j)
20     simp only [mul_add, Finset.sum_add_distrib]
21   map_smul' c x := by
22     ext i
23     change (∑ j, a i j*(c*x j))=c*(∑ j,a i j*x j)
24     rw [Finset.mul_sum]
25     congr 1
26     funext j
27     ring
28 
29 def operator (n : ℕ) (a : Fin n → Fin n → ℝ) : Space n →L[ℝ] Space n :=
30   (linear n a).toContinuousLinearMap
31 
32 @[simp] theorem operator_apply (n : ℕ) (a : Fin n → Fin n → ℝ)
33     (x : Space n) (i : Fin n) : operator n a x i=∑ j,a i j*x j := rfl
34 
35 theorem norm_squared (n : ℕ) (x : Space n) : ‖x‖^2=∑ i,(x i)^2 :=
36   EuclideanSpace.real_norm_sq_eq x
37 
38 theorem inner_coordinates (n : ℕ) (x y : Space n) :
39     inner ℝ x y=∑ i,x i*y i := by
40   simp [PiLp.inner_apply, mul_comm]
41 
42 end ExactCoordinates
43 end KomorebiSpace
44 end

Back to source controls