feat(topology/instances/real_vector_space): add an is_scalar_tower instance (#10490)

There is at most one topological real vector space structure on a topological additive group, so `[is_scalar_tower real A E]` holds automatically as long as `A` is a topological real algebra and `E` is a topological module over `A`.

Author: urkud

src/analysis/calculus/mean_value.lean

@@ -469,14 +469,11 @@ end
 
 Theorems in this section work both for real and complex differentiable functions. We use assumptions
 `[is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 G]` to achieve this result. For the domain `E` we
-also assume `[normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E]` to have a notion of a `convex` set. In both
-interesting cases `𝕜 = ℝ` and `𝕜 = ℂ` the assumption `[is_scalar_tower ℝ 𝕜 E]` is satisfied
-automatically. -/
+also assume `[normed_space ℝ E]` to have a notion of a `convex` set. -/
 
 section
 
-variables {𝕜 G : Type*} [is_R_or_C 𝕜] [normed_space 𝕜 E] [is_scalar_tower ℝ 𝕜 E]
-  [normed_group G] [normed_space 𝕜 G]
+variables {𝕜 G : Type*} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_group G] [normed_space 𝕜 G]
 
 namespace convex
 
@@ -489,7 +486,6 @@ theorem norm_image_sub_le_of_norm_has_fderiv_within_le
   (hs : convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) : ∥f y - f x∥ ≤ C * ∥y - x∥ :=
 begin
   letI : normed_space ℝ G := restrict_scalars.normed_space ℝ 𝕜 G,
-  letI : is_scalar_tower ℝ 𝕜 G := restrict_scalars.is_scalar_tower _ _ _,
   /- By composition with `t ↦ x + t • (y-x)`, we reduce to a statement for functions defined
   on `[0,1]`, for which it is proved in `norm_image_sub_le_of_norm_deriv_le_segment`.
   We just have to check the differentiability of the composition and bounds on its derivative,
@@ -1283,7 +1279,6 @@ begin
   { intros x' H', rw ← dist_eq_norm, exact le_of_lt (hε H').2 },
 -- apply mean value theorem
   letI : normed_space ℝ G := restrict_scalars.normed_space ℝ 𝕜 G,
-  letI : is_scalar_tower ℝ 𝕜 G := restrict_scalars.is_scalar_tower _ _ _,
   refine (convex_ball _ _).norm_image_sub_le_of_norm_has_fderiv_within_le' _ hf' h.2 h.1,
   exact λ y hy, (hε hy).1.has_fderiv_within_at
 end

src/analysis/calculus/parametric_integral.lean

@@ -57,8 +57,7 @@ open topological_space measure_theory filter metric
 open_locale topological_space filter
 
 variables {α : Type*} [measurable_space α] {μ : measure α} {𝕜 : Type*} [is_R_or_C 𝕜]
-          {E : Type*} [normed_group E] [normed_space ℝ E]
-          [normed_space 𝕜 E] [is_scalar_tower ℝ 𝕜 E]
+          {E : Type*} [normed_group E] [normed_space ℝ E] [normed_space 𝕜 E]
           [complete_space E] [second_countable_topology E]
           [measurable_space E] [borel_space E]
           {H : Type*} [normed_group H] [normed_space 𝕜 H] [second_countable_topology $ H →L[𝕜] E]
@@ -193,7 +192,6 @@ lemma has_fderiv_at_integral_of_dominated_of_fderiv_le {F : H → α → E} {F'
   has_fderiv_at (λ x, ∫ a, F x a ∂μ) (∫ a, F' x₀ a ∂μ) x₀ :=
 begin
   letI : normed_space ℝ H := normed_space.restrict_scalars ℝ 𝕜 H,
-  haveI : is_scalar_tower ℝ 𝕜 H := restrict_scalars.is_scalar_tower ℝ 𝕜 H,
   have x₀_in : x₀ ∈ ball x₀ ε := mem_ball_self ε_pos,
   have diff_x₀ : ∀ᵐ a ∂μ, has_fderiv_at (λ x, F x a) (F' x₀ a) x₀ :=
     h_diff.mono (λ a ha, ha x₀ x₀_in),

src/analysis/calculus/parametric_interval_integral.lean

@@ -18,8 +18,7 @@ open_locale topological_space filter interval
 
 variables {α 𝕜 : Type*} [measurable_space α] [linear_order α] [topological_space α]
           [order_topology α] [opens_measurable_space α] {μ : measure α} [is_R_or_C 𝕜]
-          {E : Type*} [normed_group E] [normed_space ℝ E]
-          [normed_space 𝕜 E] [is_scalar_tower ℝ 𝕜 E]
+          {E : Type*} [normed_group E] [normed_space ℝ E] [normed_space 𝕜 E]
           [complete_space E] [second_countable_topology E]
           [measurable_space E] [borel_space E]
           {H : Type*} [normed_group H] [normed_space 𝕜 H] [second_countable_topology $ H →L[𝕜] E]

src/analysis/complex/conformal.lean

@@ -40,7 +40,7 @@ conj_lie.to_linear_isometry.is_conformal_map
 section conformal_into_complex_normed
 
 variables {E : Type*} [normed_group E] [normed_space ℝ E] [normed_space ℂ E]
-  [is_scalar_tower ℝ ℂ E] {z : ℂ} {g : ℂ →L[ℝ] E} {f : ℂ → E}
+  {z : ℂ} {g : ℂ →L[ℝ] E} {f : ℂ → E}
 
 lemma is_conformal_map_complex_linear
   {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) : is_conformal_map (map.restrict_scalars ℝ) :=

src/analysis/complex/real_deriv.lean

@@ -129,7 +129,7 @@ variables
     This is a version of the Cauchy-Riemann equations. -/
 lemma differentiable_at.conformal_at {E : Type*}
   [normed_group E] [normed_space ℝ E] [normed_space ℂ E]
-  [is_scalar_tower ℝ ℂ E] {z : ℂ} {f : ℂ → E}
+  {z : ℂ} {f : ℂ → E}
   (hf' : fderiv ℝ f z ≠ 0) (h : differentiable_at ℂ f z) :
   conformal_at f z :=
 begin

src/analysis/inner_product_space/basic.lean

@@ -1403,10 +1403,9 @@ product satisfies `is_bounded_bilinear_map`.
 In order to state these results, we need a `normed_space ℝ E` instance. We will later establish
 such an instance by restriction-of-scalars, `inner_product_space.is_R_or_C_to_real 𝕜 E`, but this
 instance may be not definitionally equal to some other “natural” instance. So, we assume
-`[normed_space ℝ E]` and `[is_scalar_tower ℝ 𝕜 E]`. In both interesting cases `𝕜 = ℝ` and `𝕜 = ℂ`
-we have these instances.
+`[normed_space ℝ E]`.
 -/
-lemma is_bounded_bilinear_map_inner [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] :
+lemma is_bounded_bilinear_map_inner [normed_space ℝ E] :
   is_bounded_bilinear_map ℝ (λ p : E × E, ⟪p.1, p.2⟫) :=
 { add_left := λ _ _ _, inner_add_left,
   smul_left := λ r x y,
@@ -1651,7 +1650,6 @@ section continuous
 lemma continuous_inner : continuous (λ p : E × E, ⟪p.1, p.2⟫) :=
 begin
   letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜 E,
-  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
   exact is_bounded_bilinear_map_inner.continuous
 end
 

src/analysis/inner_product_space/calculus.lean

@@ -12,9 +12,7 @@ import analysis.special_functions.sqrt
 In this file we prove that the inner product and square of the norm in an inner space are
 infinitely `ℝ`-smooth. In order to state these results, we need a `normed_space ℝ E`
 instance. Though we can deduce this structure from `inner_product_space 𝕜 E`, this instance may be
-not definitionally equal to some other “natural” instance. So, we assume `[normed_space ℝ E]` and
-`[is_scalar_tower ℝ 𝕜 E]`. In both interesting cases `𝕜 = ℝ` and `𝕜 = ℂ` we have these instances.
-
+not definitionally equal to some other “natural” instance. So, we assume `[normed_space ℝ E]`.
 -/
 
 noncomputable theory
@@ -26,7 +24,7 @@ variables {𝕜 E F : Type*} [is_R_or_C 𝕜]
 variables [inner_product_space 𝕜 E] [inner_product_space ℝ F]
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 
-variables [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E]
+variables [normed_space ℝ E]
 
 /-- Derivative of the inner product. -/
 def fderiv_inner_clm (p : E × E) : E × E →L[ℝ] 𝕜 := is_bounded_bilinear_map_inner.deriv p

src/analysis/inner_product_space/projection.lean

@@ -271,7 +271,6 @@ theorem exists_norm_eq_infi_of_complete_subspace
 begin
   letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜 E,
   letI : module ℝ E := restrict_scalars.module ℝ 𝕜 E,
-  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
   let K' : submodule ℝ E := submodule.restrict_scalars ℝ K,
   exact exists_norm_eq_infi_of_complete_convex ⟨0, K'.zero_mem⟩ h K'.convex
 end
@@ -330,7 +329,6 @@ theorem norm_eq_infi_iff_inner_eq_zero {u : E} {v : E}
 begin
   letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜 E,
   letI : module ℝ E := restrict_scalars.module ℝ 𝕜 E,
-  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
   let K' : submodule ℝ E := K.restrict_scalars ℝ,
   split,
   { assume H,

src/analysis/inner_product_space/rayleigh.lean

@@ -156,7 +156,6 @@ lemma eq_smul_self_of_is_local_extr_on (hT : is_self_adjoint (T : E →ₗ[𝕜]
   T x₀ = (↑(rayleigh_quotient x₀) : 𝕜) • x₀ :=
 begin
   letI := inner_product_space.is_R_or_C_to_real 𝕜 E,
-  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
   let S : E →L[ℝ] E :=
     @continuous_linear_map.restrict_scalars 𝕜 E E _ _ _ _ _ _ _ ℝ _ _ _ _ T,
   have hSA : is_self_adjoint (S : E →ₗ[ℝ] E) := λ x y, by

src/data/complex/is_R_or_C.lean

@@ -639,7 +639,6 @@ This is not an instance because it would cause a search for `finite_dimensional
 lemma proper_is_R_or_C [finite_dimensional K E] : proper_space E :=
 begin
   letI : normed_space ℝ E := restrict_scalars.normed_space ℝ K E,
-  letI : is_scalar_tower ℝ K E := restrict_scalars.is_scalar_tower _ _ _,
   letI : finite_dimensional ℝ E := finite_dimensional.trans ℝ K E,
   apply_instance
 end