OAI/Analysis/Mahler/CoordinateEuclidean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerStokes.radiusSq_eq_euclidean_norm_sq line 12

   Source documentation

   Explicit identification with the L2 Euclidean norm, rather than the ambient supremum norm on the coordinate function space.

   theorem radiusSq_eq_euclidean_norm_sq {n : ℕ} (x : Fin n → ℝ) :
       radiusSq x = ‖(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin n))‖^2 := by
   …

   Mentions: OAI.MahlerStokes.radiusSq

2. theorem OAI.MahlerStokes.coordBall_eq_euclidean_ball line 16
3. theorem OAI.MahlerStokes.coordClosedBall_eq_euclidean_closedBall line 24