[Merged by Bors] - chore(linear_algebra/affine_space): introduce notation for affine_map

src/analysis/convex/basic.lean

@@ -221,15 +221,15 @@ lemma convex.combo_to_vadd {a b : ℝ} {x y : E} (h : a + b = 1) :
 Applying an affine map to an affine combination of two points yields
 an affine combination of the images.
  -/
-lemma convex.combo_affine_apply {a b : ℝ} {x y : E} {f : affine_map ℝ E F} (h : a + b = 1) :
+lemma convex.combo_affine_apply {a b : ℝ} {x y : E} {f : E →ᵃ[ℝ] F} (h : a + b = 1) :
   f (a • x + b • y) = a • f x + b • f y :=
 begin
   simp only [convex.combo_to_vadd h, ← vsub_eq_sub],
   exact f.apply_line_map _ _ _,
 end
 
 /-- The preimage of a convex set under an affine map is convex. -/
-lemma convex.affine_preimage (f : affine_map ℝ E F) {s : set F} (hs : convex s) :
+lemma convex.affine_preimage (f : E →ᵃ[ℝ] F) {s : set F} (hs : convex s) :
   convex (f ⁻¹' s) :=
 begin
   intros x y xs ys a b ha hb hab,
@@ -238,7 +238,7 @@ begin
 end
 
 /-- The image of a convex set under an affine map is convex. -/
-lemma convex.affine_image (f : affine_map ℝ E F) {s : set E} (hs : convex s) :
+lemma convex.affine_image (f : E →ᵃ[ℝ] F) {s : set E} (hs : convex s) :
   convex (f '' s) :=
 begin
   rintros x y ⟨x', ⟨hx', hx'f⟩⟩ ⟨y', ⟨hy', hy'f⟩⟩ a b ha hb hab,
@@ -830,7 +830,7 @@ lemma concave_on_iff_convex_hypograph {γ : Type*} [ordered_add_comm_group γ] [
 @convex_on_iff_convex_epigraph _ _ _ _ (order_dual γ) _ _ f
 
 /-- If a function is convex on s, it remains convex when precomposed by an affine map -/
-lemma convex_on.comp_affine_map {f : F → β} (g : affine_map ℝ E F) {s : set F}
+lemma convex_on.comp_affine_map {f : F → β} (g : E →ᵃ[ℝ] F) {s : set F}
   (hf : convex_on s f) : convex_on (g ⁻¹' s) (f ∘ g) :=
 begin
   refine ⟨hf.1.affine_preimage  _,_⟩,
@@ -843,7 +843,7 @@ begin
 end
 
 /-- If a function is concave on s, it remains concave when precomposed by an affine map -/
-lemma concave_on.comp_affine_map {f : F → β} (g : affine_map ℝ E F) {s : set F}
+lemma concave_on.comp_affine_map {f : F → β} (g : E →ᵃ[ℝ] F) {s : set F}
   (hf : concave_on s f) : concave_on (g ⁻¹' s) (f ∘ g) :=
 @convex_on.comp_affine_map _ _ _ _ _ _ (order_dual β) _ _ f g s hf
 

src/analysis/convex/extrema.lean

@@ -66,7 +66,7 @@ begin
   by_contradiction H_cont,
   push_neg at H_cont,
   rcases H_cont with ⟨x, ⟨x_in_s, fx_lt_fa⟩⟩,
-  let g : affine_map ℝ ℝ E := affine_map.line_map a x,
+  let g : ℝ →ᵃ[ℝ] E := affine_map.line_map a x,
   have hg0 : g 0 = a := affine_map.line_map_apply_zero a x,
   have hg1 : g 1 = x := affine_map.line_map_apply_one a x,
   have fg_local_min_on : is_local_min_on (f ∘ g) (g ⁻¹' s) 0,

src/analysis/normed_space/mazur_ulam.lean

@@ -18,7 +18,7 @@ We formalize it in two definitions:
   returns `E ≃L[ℝ] F` with the same `to_fun` and `inv_fun`;
 * `isometric.to_real_linear_equiv` : given `f : E ≃ᵢ F`,
   returns `g : E ≃L[ℝ] F` with `g x = f x - f 0`.
-* `isometric.to_affine_map` : given `PE ≃ᵢ PF`, returns `g : affine_map ℝ E PE F PF` with the same
+* `isometric.to_affine_map` : given `PE ≃ᵢ PF`, returns `g : PE →ᵃ[ℝ] PF` with the same
   `to_fun`.
 
 The formalization is based on [Jussi Väisälä, *A Proof of the Mazur-Ulam Theorem*][Vaisala_2003].
@@ -134,7 +134,7 @@ variables {E F} {PE : Type*} {PF : Type*} [metric_space PE] [normed_add_torsor E
 include E F
 
 /-- Convert an isometric equivalence between two affine spaces to an `affine_map`. -/
-def to_affine_map (f : PE ≃ᵢ PF) : affine_map ℝ PE PF :=
+def to_affine_map (f : PE ≃ᵢ PF) : PE →ᵃ[ℝ] PF :=
 affine_map.mk' f
  ((vadd_const (classical.choice $ add_torsor.nonempty : PE)).trans $ f.trans
    (vadd_const (f $ classical.choice $ add_torsor.nonempty : PF)).symm).to_real_linear_equiv

src/geometry/euclidean/basic.lean

@@ -602,7 +602,7 @@ subspace being projected onto. For most purposes,
 `is_complete` hypotheses and is the identity map when either of those
 hypotheses fails, should be used instead. -/
 def orthogonal_projection_of_nonempty_of_complete {s : affine_subspace ℝ P}
-  (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) : affine_map ℝ P P :=
+  (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) : P →ᵃ[ℝ] P :=
 { to_fun := orthogonal_projection_fn hn hc,
   linear := orthogonal_projection s.direction,
   map_vadd' := λ p v, begin
@@ -633,7 +633,7 @@ of two points whose difference is that vector) is the
 direction of the affine subspace being projected onto.  If the
 subspace is empty or not complete, this uses the identity map
 instead. -/
-def orthogonal_projection (s : affine_subspace ℝ P) : affine_map ℝ P P :=
+def orthogonal_projection (s : affine_subspace ℝ P) : P →ᵃ[ℝ] P :=
 if h : (s : set P).nonempty ∧ is_complete (s.direction : set V) then
   orthogonal_projection_of_nonempty_of_complete h.1 h.2 else affine_map.id ℝ P