chore(analysis/inner_product_space/basic): explicit 𝕜 argument for innerₛₗ and innerSL (#18613)

A reasonable fraction of the uses of these functions required either `@` or a type annotation before this change.

Author: eric-wieser

src/analysis/convex/cone/basic.lean

@@ -764,7 +764,7 @@ lemma pointed_inner_dual_cone : s.inner_dual_cone.pointed :=
 /-- The inner dual cone of a singleton is given by the preimage of the positive cone under the
 linear map `λ y, ⟪x, y⟫`. -/
 lemma inner_dual_cone_singleton (x : H) :
-  ({x} : set H).inner_dual_cone = (convex_cone.positive ℝ ℝ).comap (innerₛₗ x) :=
+  ({x} : set H).inner_dual_cone = (convex_cone.positive ℝ ℝ).comap (innerₛₗ ℝ x) :=
 convex_cone.ext $ λ i, forall_eq
 
 lemma inner_dual_cone_union (s t : set H) :

src/analysis/inner_product_space/basic.lean

@@ -1695,31 +1695,33 @@ by simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right,
             h₁, h₂, zero_mul, mul_zero, finset.sum_const_zero, zero_add, zero_sub, finset.mul_sum,
             neg_div, finset.sum_div, mul_div_assoc, mul_assoc]
 
+variables (𝕜)
+
 /-- The inner product as a sesquilinear map. -/
 def innerₛₗ : E →ₗ⋆[𝕜] E →ₗ[𝕜] 𝕜 :=
 linear_map.mk₂'ₛₗ _ _ (λ v w, ⟪v, w⟫) inner_add_left (λ _ _ _, inner_smul_left _ _ _)
   inner_add_right (λ _ _ _, inner_smul_right _ _ _)
 
-@[simp] lemma innerₛₗ_apply_coe (v : E) : (innerₛₗ v : E → 𝕜) = λ w, ⟪v, w⟫ := rfl
+@[simp] lemma innerₛₗ_apply_coe (v : E) : ⇑(innerₛₗ 𝕜 v) = λ w, ⟪v, w⟫ := rfl
 
-@[simp] lemma innerₛₗ_apply (v w : E) : innerₛₗ v w = ⟪v, w⟫ := rfl
+@[simp] lemma innerₛₗ_apply (v w : E) : innerₛₗ 𝕜 v w = ⟪v, w⟫ := rfl
 
 /-- The inner product as a continuous sesquilinear map. Note that `to_dual_map` (resp. `to_dual`)
 in `inner_product_space.dual` is a version of this given as a linear isometry (resp. linear
 isometric equivalence). -/
 def innerSL : E →L⋆[𝕜] E →L[𝕜] 𝕜 :=
-linear_map.mk_continuous₂ innerₛₗ 1
+linear_map.mk_continuous₂ (innerₛₗ 𝕜) 1
 (λ x y, by simp only [norm_inner_le_norm, one_mul, innerₛₗ_apply])
 
-@[simp] lemma innerSL_apply_coe (v : E) : (innerSL v : E → 𝕜) = λ w, ⟪v, w⟫ := rfl
+@[simp] lemma innerSL_apply_coe (v : E) : ⇑(innerSL 𝕜 v) = λ w, ⟪v, w⟫ := rfl
 
-@[simp] lemma innerSL_apply (v w : E) : innerSL v w = ⟪v, w⟫ := rfl
+@[simp] lemma innerSL_apply (v w : E) : innerSL 𝕜 v w = ⟪v, w⟫ := rfl
 
 /-- `innerSL` is an isometry. Note that the associated `linear_isometry` is defined in
 `inner_product_space.dual` as `to_dual_map`.  -/
-@[simp] lemma innerSL_apply_norm {x : E} : ‖(innerSL x : E →L[𝕜] 𝕜)‖ = ‖x‖ :=
+@[simp] lemma innerSL_apply_norm (x : E) : ‖innerSL 𝕜 x‖ = ‖x‖ :=
 begin
-  refine le_antisymm ((innerSL x : E →L[𝕜] 𝕜).op_norm_le_bound (norm_nonneg _)
+  refine le_antisymm ((innerSL 𝕜 x).op_norm_le_bound (norm_nonneg _)
     (λ y, norm_inner_le_norm _ _)) _,
   cases eq_or_lt_of_le (norm_nonneg x) with h h,
   { have : x = 0 := norm_eq_zero.mp (eq.symm h),
@@ -1728,16 +1730,18 @@ begin
     calc ‖x‖ * ‖x‖ = ‖x‖ ^ 2 : by ring
     ... = re ⟪x, x⟫ : norm_sq_eq_inner _
     ... ≤ abs ⟪x, x⟫ : re_le_abs _
-    ... = ‖innerSL x x‖ : by { rw [←is_R_or_C.norm_eq_abs], refl }
-    ... ≤ ‖innerSL x‖ * ‖x‖ : (innerSL x : E →L[𝕜] 𝕜).le_op_norm _ }
+    ... = ‖⟪x, x⟫‖ : by rw [←is_R_or_C.norm_eq_abs]
+    ... ≤ ‖innerSL 𝕜 x‖ * ‖x‖ : (innerSL 𝕜 x).le_op_norm _ }
 end
 
 /-- The inner product as a continuous sesquilinear map, with the two arguments flipped. -/
 def innerSL_flip : E →L[𝕜] E →L⋆[𝕜] 𝕜 :=
 @continuous_linear_map.flipₗᵢ' 𝕜 𝕜 𝕜 E E 𝕜 _ _ _ _ _ _ _ _ _ (ring_hom.id 𝕜) (star_ring_end 𝕜) _ _
-  innerSL
+  (innerSL 𝕜)
+
+@[simp] lemma innerSL_flip_apply (x y : E) : innerSL_flip 𝕜 x y = ⟪y, x⟫ := rfl
 
-@[simp] lemma innerSL_flip_apply (x y : E) : innerSL_flip x y = ⟪y, x⟫ := rfl
+variables {𝕜}
 
 namespace continuous_linear_map
 
@@ -1748,10 +1752,10 @@ as a continuous linear map. -/
 def to_sesq_form : (E →L[𝕜] E') →L[𝕜] E' →L⋆[𝕜] E →L[𝕜] 𝕜 :=
 ↑((continuous_linear_map.flipₗᵢ' E E' 𝕜
   (star_ring_end 𝕜) (ring_hom.id 𝕜)).to_continuous_linear_equiv) ∘L
-(continuous_linear_map.compSL E E' (E' →L⋆[𝕜] 𝕜) (ring_hom.id 𝕜) (ring_hom.id 𝕜) innerSL_flip)
+(continuous_linear_map.compSL E E' (E' →L⋆[𝕜] 𝕜) (ring_hom.id 𝕜) (ring_hom.id 𝕜) (innerSL_flip 𝕜))
 
 @[simp] lemma to_sesq_form_apply_coe (f : E →L[𝕜] E') (x : E') :
-  to_sesq_form f x = (innerSL x).comp f := rfl
+  to_sesq_form f x = (innerSL 𝕜 x).comp f := rfl
 
 lemma to_sesq_form_apply_norm_le {f : E →L[𝕜] E'} {v : E'} : ‖to_sesq_form f v‖ ≤ ‖f‖ * ‖v‖ :=
 begin
@@ -2287,7 +2291,7 @@ by simp [disjoint_iff, K.inf_orthogonal_eq_bot]
 
 /-- `Kᗮ` can be characterized as the intersection of the kernels of the operations of
 inner product with each of the elements of `K`. -/
-lemma orthogonal_eq_inter : Kᗮ = ⨅ v : K, linear_map.ker (innerSL (v:E) : E →L[𝕜] 𝕜) :=
+lemma orthogonal_eq_inter : Kᗮ = ⨅ v : K, linear_map.ker (innerSL 𝕜 (v : E)) :=
 begin
   apply le_antisymm,
   { rw le_infi_iff,
@@ -2302,7 +2306,7 @@ end
 lemma submodule.is_closed_orthogonal : is_closed (Kᗮ : set E) :=
 begin
   rw orthogonal_eq_inter K,
-  have := λ v : K, continuous_linear_map.is_closed_ker (innerSL (v:E) : E →L[𝕜] 𝕜),
+  have := λ v : K, continuous_linear_map.is_closed_ker (innerSL 𝕜 (v : E)),
   convert is_closed_Inter this,
   simp only [submodule.infi_coe],
 end
@@ -2397,7 +2401,7 @@ protected lemma continuous_inner :
   continuous (uncurry inner : completion E × completion E → 𝕜) :=
 begin
   let inner' : E →+ E →+ 𝕜 :=
-  { to_fun := λ x, (innerₛₗ x).to_add_monoid_hom,
+  { to_fun := λ x, (innerₛₗ 𝕜 x).to_add_monoid_hom,
     map_zero' := by ext x; exact inner_zero_left _,
     map_add' := λ x y, by ext z; exact inner_add_left _ _ _ },
   have : continuous (λ p : E × E, inner' p.1 p.2) := continuous_inner,

src/analysis/inner_product_space/calculus.lean

@@ -191,7 +191,7 @@ cont_diff_iff_cont_diff_at.2 $
 
 omit 𝕜
 lemma has_strict_fderiv_at_norm_sq (x : F) :
-  has_strict_fderiv_at (λ x, ‖x‖ ^ 2) (bit0 (innerSL x : F →L[ℝ] ℝ)) x :=
+  has_strict_fderiv_at (λ x, ‖x‖ ^ 2) (bit0 (innerSL ℝ x)) x :=
 begin
   simp only [sq, ← inner_self_eq_norm_mul_norm],
   convert (has_strict_fderiv_at_id x).inner (has_strict_fderiv_at_id x),

src/analysis/inner_product_space/dual.lean

@@ -54,14 +54,14 @@ If `E` is complete, this operation is surjective, hence a conjugate-linear isome
 see `to_dual`.
 -/
 def to_dual_map : E →ₗᵢ⋆[𝕜] normed_space.dual 𝕜 E :=
-{ norm_map' := λ _, innerSL_apply_norm,
- ..innerSL }
+{ norm_map' := innerSL_apply_norm _,
+ ..innerSL 𝕜 }
 
 variables {E}
 
 @[simp] lemma to_dual_map_apply {x y : E} : to_dual_map 𝕜 E x y = ⟪x, y⟫ := rfl
 
-lemma innerSL_norm [nontrivial E] : ‖(innerSL : E →L⋆[𝕜] E →L[𝕜] 𝕜)‖ = 1 :=
+lemma innerSL_norm [nontrivial E] : ‖(innerSL 𝕜 : E →L⋆[𝕜] E →L[𝕜] 𝕜)‖ = 1 :=
 show ‖(to_dual_map 𝕜 E).to_continuous_linear_map‖ = 1,
   from linear_isometry.norm_to_continuous_linear_map _
 

src/analysis/inner_product_space/l2_space.lean

@@ -454,7 +454,7 @@ end
 protected lemma has_sum_inner_mul_inner (b : hilbert_basis ι 𝕜 E) (x y : E) :
   has_sum (λ i, ⟪x, b i⟫ * ⟪b i, y⟫) ⟪x, y⟫ :=
 begin
-  convert (b.has_sum_repr y).mapL (innerSL x),
+  convert (b.has_sum_repr y).mapL (innerSL _ x),
   ext i,
   rw [innerSL_apply, b.repr_apply_apply, inner_smul_right, mul_comm]
 end

src/analysis/inner_product_space/pi_L2.lean

@@ -329,7 +329,7 @@ by { simpa using (b.to_basis.equiv_fun_symm_apply v).symm }
 protected lemma sum_inner_mul_inner (b : orthonormal_basis ι 𝕜 E) (x y : E) :
   ∑ i, ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, y⟫ :=
 begin
-  have := congr_arg (@innerSL 𝕜 _ _ _ x) (b.sum_repr y),
+  have := congr_arg (innerSL 𝕜 x) (b.sum_repr y),
   rw map_sum at this,
   convert this,
   ext i,

src/analysis/inner_product_space/rayleigh.lean

@@ -93,7 +93,7 @@ variables {F : Type*} [inner_product_space ℝ F]
 
 lemma _root_.linear_map.is_symmetric.has_strict_fderiv_at_re_apply_inner_self
   {T : F →L[ℝ] F} (hT : (T : F →ₗ[ℝ] F).is_symmetric) (x₀ : F) :
-  has_strict_fderiv_at T.re_apply_inner_self (_root_.bit0 (innerSL (T x₀) : F →L[ℝ] ℝ)) x₀ :=
+  has_strict_fderiv_at T.re_apply_inner_self (_root_.bit0 (innerSL ℝ (T x₀))) x₀ :=
 begin
   convert T.has_strict_fderiv_at.inner (has_strict_fderiv_at_id x₀),
   ext y,
@@ -120,7 +120,7 @@ begin
   refine ⟨a, b, h₁, _⟩,
   apply (inner_product_space.to_dual_map ℝ F).injective,
   simp only [linear_isometry.map_add, linear_isometry.map_smul, linear_isometry.map_zero],
-  change a • innerSL x₀ + b • innerSL (T x₀) = 0,
+  change a • innerSL _ x₀ + b • innerSL _ (T x₀) = 0,
   apply smul_right_injective (F →L[ℝ] ℝ) (two_ne_zero : (2:ℝ) ≠ 0),
   simpa only [_root_.bit0, add_smul, smul_add, one_smul, add_zero] using h₂
 end

src/analysis/inner_product_space/two_dim.lean

@@ -369,7 +369,7 @@ coe_basis_of_linear_independent_of_card_eq_finrank _ _
 /-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫`. (See
 `orientation.inner_mul_inner_add_area_form_mul_area_form` for the "applied" form.)-/
 lemma inner_mul_inner_add_area_form_mul_area_form' (a x : E) :
-  ⟪a, x⟫ • @innerₛₗ ℝ _ _ _ a + ω a x • ω a = ‖a‖ ^ 2 • @innerₛₗ ℝ _ _ _ x :=
+  ⟪a, x⟫ • innerₛₗ ℝ a + ω a x • ω a = ‖a‖ ^ 2 • innerₛₗ ℝ x :=
 begin
   by_cases ha : a = 0,
   { simp [ha] },
@@ -399,7 +399,7 @@ by simpa [sq, real_inner_self_eq_norm_sq] using o.inner_mul_inner_add_area_form_
 /-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y`. (See
 `orientation.inner_mul_area_form_sub` for the "applied" form.) -/
 lemma inner_mul_area_form_sub' (a x : E) :
-  ⟪a, x⟫ • ω a - ω a x • @innerₛₗ ℝ _ _ _ a = ‖a‖ ^ 2 • ω x :=
+  ⟪a, x⟫ • ω a - ω a x • innerₛₗ ℝ a = ‖a‖ ^ 2 • ω x :=
 begin
   by_cases ha : a = 0,
   { simp [ha] },
@@ -456,7 +456,7 @@ real part is the inner product and its imaginary part is `orientation.area_form`
 
 On `ℂ` with the standard orientation, `kahler w z = conj w * z`; see `complex.kahler`. -/
 def kahler : E →ₗ[ℝ] E →ₗ[ℝ] ℂ :=
-(linear_map.llcomp ℝ E ℝ ℂ complex.of_real_clm) ∘ₗ (@innerₛₗ ℝ E _ _)
+(linear_map.llcomp ℝ E ℝ ℂ complex.of_real_clm) ∘ₗ innerₛₗ ℝ
 + (linear_map.llcomp ℝ E ℝ ℂ ((linear_map.lsmul ℝ ℂ).flip complex.I)) ∘ₗ ω
 
 lemma kahler_apply_apply (x y : E) : o.kahler x y = ⟪x, y⟫ + ω x y • complex.I := rfl

src/geometry/manifold/instances/sphere.lean

@@ -74,27 +74,27 @@ the orthogonal complement of an element `v` of `E`. It is smooth away from the a
 through `v` parallel to the orthogonal complement.  It restricts on the sphere to the stereographic
 projection. -/
 def stereo_to_fun [complete_space E] (x : E) : (ℝ ∙ v)ᗮ :=
-(2 / ((1:ℝ) - innerSL v x)) • orthogonal_projection (ℝ ∙ v)ᗮ x
+(2 / ((1:ℝ) - innerSL _ v x)) • orthogonal_projection (ℝ ∙ v)ᗮ x
 
 variables {v}
 
 @[simp] lemma stereo_to_fun_apply [complete_space E] (x : E) :
-  stereo_to_fun v x = (2 / ((1:ℝ) - innerSL v x)) • orthogonal_projection (ℝ ∙ v)ᗮ x :=
+  stereo_to_fun v x = (2 / ((1:ℝ) - innerSL _ v x)) • orthogonal_projection (ℝ ∙ v)ᗮ x :=
 rfl
 
 lemma cont_diff_on_stereo_to_fun [complete_space E] :
-  cont_diff_on ℝ ⊤ (stereo_to_fun v) {x : E | innerSL v x ≠ (1:ℝ)} :=
+  cont_diff_on ℝ ⊤ (stereo_to_fun v) {x : E | innerSL _ v x ≠ (1:ℝ)} :=
 begin
   refine cont_diff_on.smul _
     (orthogonal_projection ((ℝ ∙ v)ᗮ)).cont_diff.cont_diff_on,
   refine cont_diff_const.cont_diff_on.div _ _,
-  { exact (cont_diff_const.sub (innerSL v : E →L[ℝ] ℝ).cont_diff).cont_diff_on },
+  { exact (cont_diff_const.sub (innerSL ℝ v).cont_diff).cont_diff_on },
   { intros x h h',
     exact h (sub_eq_zero.mp h').symm }
 end
 
 lemma continuous_on_stereo_to_fun [complete_space E] :
-  continuous_on (stereo_to_fun v) {x : E | innerSL v x ≠ (1:ℝ)} :=
+  continuous_on (stereo_to_fun v) {x : E | innerSL _ v x ≠ (1:ℝ)} :=
 (@cont_diff_on_stereo_to_fun E _ v _).continuous_on
 
 variables (v)
@@ -208,7 +208,7 @@ begin
   ext,
   simp only [stereo_to_fun_apply, stereo_inv_fun_apply, smul_add],
   -- name two frequently-occuring quantities and write down their basic properties
-  set a : ℝ := innerSL v x,
+  set a : ℝ := innerSL _ v x,
   set y := orthogonal_projection (ℝ ∙ v)ᗮ x,
   have split : ↑x = a • v + ↑y,
   { convert eq_sum_orthogonal_projection_self_orthogonal_complement (ℝ ∙ v) x,
@@ -262,8 +262,8 @@ begin
       orthogonal_projection_orthogonal_complement_singleton_eq_zero v,
     have h₂ : orthogonal_projection (ℝ ∙ v)ᗮ w = w :=
       orthogonal_projection_mem_subspace_eq_self w,
-    have h₃ : innerSL v w = (0:ℝ) := submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2,
-    have h₄ : innerSL v v = (1:ℝ) := by simp [real_inner_self_eq_norm_mul_norm, hv],
+    have h₃ : innerSL _ v w = (0:ℝ) := submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2,
+    have h₄ : innerSL _ v v = (1:ℝ) := by simp [real_inner_self_eq_norm_mul_norm, hv],
     simp [h₁, h₂, h₃, h₄, continuous_linear_map.map_add, continuous_linear_map.map_smul,
       mul_smul] },
   { simp }

src/measure_theory/integral/set_integral.lean

@@ -1132,7 +1132,7 @@ local notation `⟪`x`, `y`⟫` := @inner 𝕜 E' _ x y
 
 lemma integral_inner {f : α → E'} (hf : integrable f μ) (c : E') :
   ∫ x, ⟪c, f x⟫ ∂μ = ⟪c, ∫ x, f x ∂μ⟫ :=
-((@innerSL 𝕜 E' _ _ c).restrict_scalars ℝ).integral_comp_comm hf
+((innerSL 𝕜 c).restrict_scalars ℝ).integral_comp_comm hf
 
 lemma integral_eq_zero_of_forall_integral_inner_eq_zero (f : α → E') (hf : integrable f μ)
   (hf_int : ∀ (c : E'), ∫ x, ⟪c, f x⟫ ∂μ = 0) :