bump to nightly-2024-02-06-08

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Analysis/Analytic/Basic.lean

@@ -336,7 +336,7 @@ theorem summable_norm_apply (p : FormalMultilinearSeries 𝕜 E F) {x : E}
   by
   rw [mem_emetric_ball_zero_iff] at hx 
   refine'
-    Summable.of_nonneg_of_le (fun _ => norm_nonneg _) (fun n => ((p n).le_op_norm _).trans_eq _)
+    Summable.of_nonneg_of_le (fun _ => norm_nonneg _) (fun n => ((p n).le_opNorm _).trans_eq _)
       (p.summable_norm_mul_pow hx)
   simp
 #align formal_multilinear_series.summable_norm_apply FormalMultilinearSeries.summable_norm_apply
@@ -820,7 +820,7 @@ theorem HasFPowerSeriesOnBall.uniform_geometric_approx' {r' : ℝ≥0}
   apply norm_sub_le_of_geometric_bound_of_hasSum (ya.trans_lt ha.2) _ (hf.has_sum this)
   intro n
   calc
-    ‖(p n) fun i : Fin n => y‖ ≤ ‖p n‖ * ∏ i : Fin n, ‖y‖ := ContinuousMultilinearMap.le_op_norm _ _
+    ‖(p n) fun i : Fin n => y‖ ≤ ‖p n‖ * ∏ i : Fin n, ‖y‖ := ContinuousMultilinearMap.le_opNorm _ _
     _ = ‖p n‖ * r' ^ n * (‖y‖ / r') ^ n := by field_simp [hr'0.ne', mul_right_comm]
     _ ≤ C * a ^ n * (‖y‖ / r') ^ n :=
       (mul_le_mul_of_nonneg_right (hp n) (pow_nonneg (div_nonneg (norm_nonneg _) r'.coe_nonneg) _))
@@ -1331,8 +1331,8 @@ theorem nnnorm_changeOriginSeriesTerm_apply_le (k l : ℕ) (s : Finset (Fin (k +
       ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k :=
   by
   rw [← p.nnnorm_change_origin_series_term k l s hs, ← Fin.prod_const, ← Fin.prod_const]
-  apply ContinuousMultilinearMap.le_of_op_nnnorm_le
-  apply ContinuousMultilinearMap.le_op_nnnorm
+  apply ContinuousMultilinearMap.le_of_opNNNorm_le
+  apply ContinuousMultilinearMap.le_opNNNorm
 #align formal_multilinear_series.nnnorm_change_origin_series_term_apply_le FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le
 -/
 
@@ -1361,8 +1361,7 @@ theorem nnnorm_changeOriginSeries_apply_le_tsum (k l : ℕ) (x : E) :
       ∑' s : { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + l)‖₊ * ‖x‖₊ ^ l :=
   by
   rw [NNReal.tsum_mul_right, ← Fin.prod_const]
-  exact
-    (p.change_origin_series k l).le_of_op_nnnorm_le _ (p.nnnorm_change_origin_series_le_tsum _ _)
+  exact (p.change_origin_series k l).le_of_opNNNorm_le _ (p.nnnorm_change_origin_series_le_tsum _ _)
 #align formal_multilinear_series.nnnorm_change_origin_series_apply_le_tsum FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum
 -/
 
@@ -1557,7 +1556,7 @@ theorem changeOrigin_eval (h : (‖x‖₊ + ‖y‖₊ : ℝ≥0∞) < p.radius
           Summable.of_nnnorm_bounded _
             (p.change_origin_series_summable_aux₂ (mem_emetric_ball_zero_iff.1 x_mem_ball) k)
             fun s => _
-        refine' (ContinuousMultilinearMap.le_op_nnnorm _ _).trans_eq _
+        refine' (ContinuousMultilinearMap.le_opNNNorm _ _).trans_eq _
         simp
   refine' hf.unique (change_origin_index_equiv.symm.has_sum_iff.1 _)
   refine'

Mathbin/Analysis/Analytic/Composition.lean

@@ -370,12 +370,12 @@ theorem compAlongComposition_bound {n : ℕ} (p : FormalMultilinearSeries 𝕜 E
     ‖f.compAlongComposition p c v‖ ≤ (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) * ∏ i : Fin n, ‖v i‖ :=
   calc
     ‖f.compAlongComposition p c v‖ = ‖f (p.applyComposition c v)‖ := rfl
-    _ ≤ ‖f‖ * ∏ i, ‖p.applyComposition c v i‖ := (ContinuousMultilinearMap.le_op_norm _ _)
+    _ ≤ ‖f‖ * ∏ i, ‖p.applyComposition c v i‖ := (ContinuousMultilinearMap.le_opNorm _ _)
     _ ≤ ‖f‖ * ∏ i, ‖p (c.blocksFun i)‖ * ∏ j : Fin (c.blocksFun i), ‖(v ∘ c.Embedding i) j‖ :=
       by
       apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
       refine' Finset.prod_le_prod (fun i hi => norm_nonneg _) fun i hi => _
-      apply ContinuousMultilinearMap.le_op_norm
+      apply ContinuousMultilinearMap.le_opNorm
     _ =
         (‖f‖ * ∏ i, ‖p (c.blocksFun i)‖) *
           ∏ (i) (j : Fin (c.blocksFun i)), ‖(v ∘ c.Embedding i) j‖ :=
@@ -393,7 +393,7 @@ the norms of the relevant bits of `q` and `p`. -/
 theorem compAlongComposition_norm {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
     (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) :
     ‖q.compAlongComposition p c‖ ≤ ‖q c.length‖ * ∏ i, ‖p (c.blocksFun i)‖ :=
-  ContinuousMultilinearMap.op_norm_le_bound _
+  ContinuousMultilinearMap.opNorm_le_bound _
     (mul_nonneg (norm_nonneg _) (Finset.prod_nonneg fun i hi => norm_nonneg _))
     (compAlongComposition_bound _ _ _)
 #align formal_multilinear_series.comp_along_composition_norm FormalMultilinearSeries.compAlongComposition_norm
@@ -950,7 +950,7 @@ theorem HasFPowerSeriesAt.comp {g : F → G} {f : E → F} {q : FormalMultilinea
       calc
         ‖(comp_along_composition q p c) fun j : Fin n => y‖ ≤
             ‖comp_along_composition q p c‖ * ∏ j : Fin n, ‖y‖ :=
-          by apply ContinuousMultilinearMap.le_op_norm
+          by apply ContinuousMultilinearMap.le_opNorm
         _ ≤ ‖comp_along_composition q p c‖ * (r : ℝ) ^ n :=
           by
           apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)

Mathbin/Analysis/Calculus/ContDiff.lean

@@ -2960,7 +2960,7 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {Du Eu
   induction' n with n IH generalizing Eu Fu Gu
   · simp only [← mul_assoc, norm_iteratedFDerivWithin_zero, Finset.range_one, Finset.sum_singleton,
       Nat.choose_self, algebraMap.coe_one, one_mul]
-    apply ((B (f x)).le_op_norm (g x)).trans
+    apply ((B (f x)).le_opNorm (g x)).trans
     apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)
     exact B.le_op_norm (f x)
   · have In : (n : ℕ∞) + 1 ≤ n.succ := by simp only [Nat.cast_succ, le_refl]
@@ -3087,15 +3087,15 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear (B : E →L
   -- All norms are preserved by the lifting process.
   have Bu_le : ‖Bu‖ ≤ ‖B‖ :=
     by
-    refine' ContinuousLinearMap.op_norm_le_bound _ (norm_nonneg _) fun y => _
-    refine' ContinuousLinearMap.op_norm_le_bound _ (by positivity) fun x => _
+    refine' ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun y => _
+    refine' ContinuousLinearMap.opNorm_le_bound _ (by positivity) fun x => _
     simp only [Bu, ContinuousLinearMap.compL_apply, ContinuousLinearMap.coe_comp',
       Function.comp_apply, LinearIsometryEquiv.coe_coe'', ContinuousLinearMap.flip_apply,
       LinearIsometryEquiv.norm_map]
     calc
-      ‖B (isoE y) (isoF x)‖ ≤ ‖B (isoE y)‖ * ‖isoF x‖ := ContinuousLinearMap.le_op_norm _ _
+      ‖B (isoE y) (isoF x)‖ ≤ ‖B (isoE y)‖ * ‖isoF x‖ := ContinuousLinearMap.le_opNorm _ _
       _ ≤ ‖B‖ * ‖isoE y‖ * ‖isoF x‖ :=
-        (mul_le_mul_of_nonneg_right (ContinuousLinearMap.le_op_norm _ _) (norm_nonneg _))
+        (mul_le_mul_of_nonneg_right (ContinuousLinearMap.le_opNorm _ _) (norm_nonneg _))
       _ = ‖B‖ * ‖y‖ * ‖x‖ := by simp only [LinearIsometryEquiv.norm_map]
   let su := isoD ⁻¹' s
   have hsu : UniqueDiffOn 𝕜 su := isoD.to_continuous_linear_equiv.unique_diff_on_preimage_iff.2 hs
@@ -3214,7 +3214,7 @@ theorem norm_iteratedFDerivWithin_smul_le {f : E → 𝕜'} {g : E → F} {N : 
           ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
   (ContinuousLinearMap.lsmul 𝕜 𝕜' :
         𝕜' →L[𝕜] F →L[𝕜] F).norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
-    hf hg hs hx hn ContinuousLinearMap.op_norm_lsmul_le
+    hf hg hs hx hn ContinuousLinearMap.opNorm_lsmul_le
 #align norm_iterated_fderiv_within_smul_le norm_iteratedFDerivWithin_smul_le
 -/
 
@@ -3225,7 +3225,7 @@ theorem norm_iteratedFDeriv_smul_le {f : E → 𝕜'} {g : E → F} {N : ℕ∞}
       ∑ i in Finset.range (n + 1),
         (n.choose i : ℝ) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖ :=
   (ContinuousLinearMap.lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] F →L[𝕜] F).norm_iteratedFDeriv_le_of_bilinear_of_le_one
-    hf hg x hn ContinuousLinearMap.op_norm_lsmul_le
+    hf hg x hn ContinuousLinearMap.opNorm_lsmul_le
 #align norm_iterated_fderiv_smul_le norm_iteratedFDeriv_smul_le
 -/
 
@@ -3245,7 +3245,7 @@ theorem norm_iteratedFDerivWithin_mul_le {f : E → A} {g : E → A} {N : ℕ∞
           ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ :=
   (ContinuousLinearMap.mul 𝕜 A :
         A →L[𝕜] A →L[𝕜] A).norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
-    hf hg hs hx hn (ContinuousLinearMap.op_norm_mul_le _ _)
+    hf hg hs hx hn (ContinuousLinearMap.opNorm_mul_le _ _)
 #align norm_iterated_fderiv_within_mul_le norm_iteratedFDerivWithin_mul_le
 -/
 
@@ -3494,8 +3494,8 @@ theorem norm_iteratedFDerivWithin_clm_apply {f : E → F →L[𝕜] G} {g : E 
   let B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := ContinuousLinearMap.flip (ContinuousLinearMap.apply 𝕜 G)
   have hB : ‖B‖ ≤ 1 :=
     by
-    simp only [ContinuousLinearMap.op_norm_flip, ContinuousLinearMap.apply]
-    refine' ContinuousLinearMap.op_norm_le_bound _ zero_le_one fun f => _
+    simp only [ContinuousLinearMap.opNorm_flip, ContinuousLinearMap.apply]
+    refine' ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun f => _
     simp only [ContinuousLinearMap.coe_id', id.def, one_mul]
   exact B.norm_iterated_fderiv_within_le_of_bilinear_of_le_one hf hg hs hx hn hB
 #align norm_iterated_fderiv_within_clm_apply norm_iteratedFDerivWithin_clm_apply

Mathbin/Analysis/Calculus/FderivSymmetric.lean

@@ -157,7 +157,7 @@ theorem Convex.taylor_approx_two_segment {v w : E} (hv : x + v ∈ interior s)
           ContinuousLinearMap.add_apply, Pi.smul_apply, smul_sub, smul_add, smul_smul, ← sub_sub,
           ContinuousLinearMap.coe_smul', Pi.sub_apply, ContinuousLinearMap.map_smul, this]
       _ ≤ ‖f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)‖ * ‖h • w‖ :=
-        (ContinuousLinearMap.le_op_norm _ _)
+        (ContinuousLinearMap.le_opNorm _ _)
       _ ≤ ε * ‖h • v + (t * h) • w‖ * ‖h • w‖ :=
         by
         apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)

Mathbin/Analysis/Calculus/ParametricIntegral.lean

@@ -146,7 +146,7 @@ theorem hasFDerivAt_integral_of_dominated_loc_of_lip' {F : H → α → E} {F' :
       _ ≤ ‖x - x₀‖⁻¹ * (b a * ‖x - x₀‖) + ‖x - x₀‖⁻¹ * (‖F' a‖ * ‖x - x₀‖) := (add_le_add _ _)
       _ ≤ b a + ‖F' a‖ := _
     exact mul_le_mul_of_nonneg_left ha_bound (nneg _)
-    apply mul_le_mul_of_nonneg_left ((F' a).le_op_norm _) (nneg _)
+    apply mul_le_mul_of_nonneg_left ((F' a).le_opNorm _) (nneg _)
     by_cases h : ‖x - x₀‖ = 0
     · simpa [h] using add_nonneg (b_nonneg a) (norm_nonneg (F' a))
     · field_simp [h]

Mathbin/Analysis/Calculus/UniformLimitsDeriv.lean

@@ -414,7 +414,7 @@ theorem hasFDerivAt_of_tendstoUniformlyOnFilter [NeBot l]
     rw [inv_mul_le_iff hnx, mul_comm]
     simp only [Function.comp_apply, Prod_map]
     rw [norm_sub_rev]
-    exact (f' n.1 x - g' x).le_op_norm (n.2 - x)
+    exact (f' n.1 x - g' x).le_opNorm (n.2 - x)
 #align has_fderiv_at_of_tendsto_uniformly_on_filter hasFDerivAt_of_tendstoUniformlyOnFilter
 -/
 
@@ -505,7 +505,7 @@ theorem UniformCauchySeqOnFilter.one_smulRight {l' : Filter 𝕜}
   intro n hn
   refine' lt_of_le_of_lt _ hq'
   simp only [dist_eq_norm, Pi.zero_apply, zero_sub, norm_neg] at hn ⊢
-  refine' ContinuousLinearMap.op_norm_le_bound _ hq.le _
+  refine' ContinuousLinearMap.opNorm_le_bound _ hq.le _
   intro z
   simp only [ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.smulRight_apply,
     ContinuousLinearMap.one_apply]
@@ -564,7 +564,7 @@ theorem hasDerivAt_of_tendstoUniformlyOnFilter [NeBot l]
     intro n hn
     refine' lt_of_le_of_lt _ hq'
     simp only [F', G', dist_eq_norm] at hn ⊢
-    refine' ContinuousLinearMap.op_norm_le_bound _ hq.le _
+    refine' ContinuousLinearMap.opNorm_le_bound _ hq.le _
     intro z
     simp only [ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.smulRight_apply,
       ContinuousLinearMap.one_apply]

Mathbin/Analysis/Complex/OperatorNorm.lean

@@ -47,7 +47,7 @@ theorem reCLM_norm : ‖reCLM‖ = 1 :=
   le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _) <|
     calc
       1 = ‖reCLM 1‖ := by simp
-      _ ≤ ‖reCLM‖ := unit_le_op_norm _ _ (by simp)
+      _ ≤ ‖reCLM‖ := unit_le_opNorm _ _ (by simp)
 #align complex.re_clm_norm Complex.reCLM_norm
 -/
 
@@ -64,7 +64,7 @@ theorem imCLM_norm : ‖imCLM‖ = 1 :=
   le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _) <|
     calc
       1 = ‖imCLM I‖ := by simp
-      _ ≤ ‖imCLM‖ := unit_le_op_norm _ _ (by simp)
+      _ ≤ ‖imCLM‖ := unit_le_opNorm _ _ (by simp)
 #align complex.im_clm_norm Complex.imCLM_norm
 -/
 

Mathbin/Analysis/Convolution.lean

@@ -1077,7 +1077,7 @@ theorem dist_convolution_le' {x₀ : G} {R ε : ℝ} {z₀ : E'} (hε : 0 ≤ ε
       rw [mem_ball_zero_iff] at h2t 
       specialize hg (x₀ - t)
       rw [sub_eq_add_neg, add_mem_ball_iff_norm, norm_neg, ← sub_eq_add_neg] at hg 
-      refine' ((L (f t)).dist_le_op_norm _ _).trans _
+      refine' ((L (f t)).dist_le_opNorm _ _).trans _
       exact mul_le_mul_of_nonneg_left (hg h2t) (norm_nonneg _)
     · rw [nmem_support] at ht 
       simp_rw [ht, L.map_zero₂, L.map_zero, norm_zero, MulZeroClass.zero_mul, dist_self]

Mathbin/Analysis/InnerProductSpace/Adjoint.lean

@@ -114,11 +114,11 @@ theorem adjointAux_adjointAux (A : E →L[𝕜] F) : adjointAux (adjointAux A) =
 theorem adjointAux_norm (A : E →L[𝕜] F) : ‖adjointAux A‖ = ‖A‖ :=
   by
   refine' le_antisymm _ _
-  · refine' ContinuousLinearMap.op_norm_le_bound _ (norm_nonneg _) fun x => _
+  · refine' ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => _
     rw [adjoint_aux_apply, LinearIsometryEquiv.norm_map]
     exact to_sesq_form_apply_norm_le
   · nth_rw_lhs 1 [← adjoint_aux_adjoint_aux A]
-    refine' ContinuousLinearMap.op_norm_le_bound _ (norm_nonneg _) fun x => _
+    refine' ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => _
     rw [adjoint_aux_apply, LinearIsometryEquiv.norm_map]
     exact to_sesq_form_apply_norm_le
 #align continuous_linear_map.adjoint_aux_norm ContinuousLinearMap.adjointAux_norm