bump to nightly-2024-01-27-06

mathlib commit leanprover-community/mathlib@65a1391

Counterexamples/Phillips.lean

@@ -454,16 +454,16 @@ def ContinuousLinearMap.toBoundedAdditiveMeasure [TopologicalSpace α] [Discrete
 #align continuous_linear_map.to_bounded_additive_measure ContinuousLinearMap.toBoundedAdditiveMeasure
 
 @[simp]
-theorem continuousPart_evalClm_eq_zero [TopologicalSpace α] [DiscreteTopology α] (s : Set α)
-    (x : α) : (evalClm ℝ x).toBoundedAdditiveMeasure.continuousPart s = 0 :=
-  let f := (evalClm ℝ x).toBoundedAdditiveMeasure
+theorem continuousPart_evalCLM_eq_zero [TopologicalSpace α] [DiscreteTopology α] (s : Set α)
+    (x : α) : (evalCLM ℝ x).toBoundedAdditiveMeasure.continuousPart s = 0 :=
+  let f := (evalCLM ℝ x).toBoundedAdditiveMeasure
   calc
     f.continuousPart s = f.continuousPart (s \ {x}) :=
       (continuousPart_apply_diff _ _ _ (countable_singleton x)).symm
     _ = f (univ \ f.discreteSupport ∩ (s \ {x})) := rfl
     _ = indicator (univ \ f.discreteSupport ∩ (s \ {x})) 1 x := rfl
     _ = 0 := by simp
-#align counterexample.phillips_1940.continuous_part_eval_clm_eq_zero Counterexample.Phillips1940.continuousPart_evalClm_eq_zero
+#align counterexample.phillips_1940.continuous_part_eval_clm_eq_zero Counterexample.Phillips1940.continuousPart_evalCLM_eq_zero
 
 theorem to_functions_to_measure [MeasurableSpace α] (μ : Measure α) [IsFiniteMeasure μ] (s : Set α)
     (hs : MeasurableSet s) :

Mathbin/Analysis/Complex/Basic.lean

@@ -301,17 +301,17 @@ theorem uniformEmbedding_equivRealProd : UniformEmbedding equivRealProd :=
 instance : CompleteSpace ℂ :=
   (completeSpace_congr uniformEmbedding_equivRealProd).mpr inferInstance
 
-#print Complex.equivRealProdClm /-
+#print Complex.equivRealProdCLM /-
 /-- The natural `continuous_linear_equiv` from `ℂ` to `ℝ × ℝ`. -/
 @[simps (config := { simpRhs := true }) apply symm_apply_re symm_apply_im]
-def equivRealProdClm : ℂ ≃L[ℝ] ℝ × ℝ :=
+def equivRealProdCLM : ℂ ≃L[ℝ] ℝ × ℝ :=
   equivRealProdLm.toContinuousLinearEquivOfBounds 1 (Real.sqrt 2) equivRealProd_apply_le' fun p =>
     abs_le_sqrt_two_mul_max (equivRealProd.symm p)
-#align complex.equiv_real_prod_clm Complex.equivRealProdClm
+#align complex.equiv_real_prod_clm Complex.equivRealProdCLM
 -/
 
 instance : ProperSpace ℂ :=
-  (id lipschitz_equivRealProd : LipschitzWith 1 equivRealProdClm.toHomeomorph).ProperSpace
+  (id lipschitz_equivRealProd : LipschitzWith 1 equivRealProdCLM.toHomeomorph).ProperSpace
 
 #print Complex.tendsto_abs_cocompact_atTop /-
 /-- The `abs` function on `ℂ` is proper. -/
@@ -331,66 +331,66 @@ theorem tendsto_normSq_cocompact_atTop : Filter.Tendsto normSq (Filter.cocompact
 
 open ContinuousLinearMap
 
-#print Complex.reClm /-
+#print Complex.reCLM /-
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
-def reClm : ℂ →L[ℝ] ℝ :=
+def reCLM : ℂ →L[ℝ] ℝ :=
   reLm.mkContinuous 1 fun x => by simp [abs_re_le_abs]
-#align complex.re_clm Complex.reClm
+#align complex.re_clm Complex.reCLM
 -/
 
 #print Complex.continuous_re /-
 @[continuity]
 theorem continuous_re : Continuous re :=
-  reClm.Continuous
+  reCLM.Continuous
 #align complex.continuous_re Complex.continuous_re
 -/
 
-#print Complex.reClm_coe /-
+#print Complex.reCLM_coe /-
 @[simp]
-theorem reClm_coe : (coe reClm : ℂ →ₗ[ℝ] ℝ) = reLm :=
+theorem reCLM_coe : (coe reCLM : ℂ →ₗ[ℝ] ℝ) = reLm :=
   rfl
-#align complex.re_clm_coe Complex.reClm_coe
+#align complex.re_clm_coe Complex.reCLM_coe
 -/
 
-#print Complex.reClm_apply /-
+#print Complex.reCLM_apply /-
 @[simp]
-theorem reClm_apply (z : ℂ) : (reClm : ℂ → ℝ) z = z.re :=
+theorem reCLM_apply (z : ℂ) : (reCLM : ℂ → ℝ) z = z.re :=
   rfl
-#align complex.re_clm_apply Complex.reClm_apply
+#align complex.re_clm_apply Complex.reCLM_apply
 -/
 
-#print Complex.imClm /-
+#print Complex.imCLM /-
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
-def imClm : ℂ →L[ℝ] ℝ :=
+def imCLM : ℂ →L[ℝ] ℝ :=
   imLm.mkContinuous 1 fun x => by simp [abs_im_le_abs]
-#align complex.im_clm Complex.imClm
+#align complex.im_clm Complex.imCLM
 -/
 
 #print Complex.continuous_im /-
 @[continuity]
 theorem continuous_im : Continuous im :=
-  imClm.Continuous
+  imCLM.Continuous
 #align complex.continuous_im Complex.continuous_im
 -/
 
-#print Complex.imClm_coe /-
+#print Complex.imCLM_coe /-
 @[simp]
-theorem imClm_coe : (coe imClm : ℂ →ₗ[ℝ] ℝ) = imLm :=
+theorem imCLM_coe : (coe imCLM : ℂ →ₗ[ℝ] ℝ) = imLm :=
   rfl
-#align complex.im_clm_coe Complex.imClm_coe
+#align complex.im_clm_coe Complex.imCLM_coe
 -/
 
-#print Complex.imClm_apply /-
+#print Complex.imCLM_apply /-
 @[simp]
-theorem imClm_apply (z : ℂ) : (imClm : ℂ → ℝ) z = z.im :=
+theorem imCLM_apply (z : ℂ) : (imCLM : ℂ → ℝ) z = z.im :=
   rfl
-#align complex.im_clm_apply Complex.imClm_apply
+#align complex.im_clm_apply Complex.imCLM_apply
 -/
 
 #print Complex.restrictScalars_one_smulRight' /-
 theorem restrictScalars_one_smulRight' (x : E) :
     ContinuousLinearMap.restrictScalars ℝ ((1 : ℂ →L[ℂ] ℂ).smul_right x : ℂ →L[ℂ] E) =
-      reClm.smul_right x + I • imClm.smul_right x :=
+      reCLM.smul_right x + I • imCLM.smul_right x :=
   by ext ⟨a, b⟩; simp [mk_eq_add_mul_I, add_smul, mul_smul, smul_comm I]
 #align complex.restrict_scalars_one_smul_right' Complex.restrictScalars_one_smulRight'
 -/
@@ -402,30 +402,30 @@ theorem restrictScalars_one_smulRight (x : ℂ) :
 #align complex.restrict_scalars_one_smul_right Complex.restrictScalars_one_smulRight
 -/
 
-#print Complex.conjLie /-
+#print Complex.conjLIE /-
 /-- The complex-conjugation function from `ℂ` to itself is an isometric linear equivalence. -/
-def conjLie : ℂ ≃ₗᵢ[ℝ] ℂ :=
+def conjLIE : ℂ ≃ₗᵢ[ℝ] ℂ :=
   ⟨conjAe.toLinearEquiv, abs_conj⟩
-#align complex.conj_lie Complex.conjLie
+#align complex.conj_lie Complex.conjLIE
 -/
 
-#print Complex.conjLie_apply /-
+#print Complex.conjLIE_apply /-
 @[simp]
-theorem conjLie_apply (z : ℂ) : conjLie z = conj z :=
+theorem conjLIE_apply (z : ℂ) : conjLIE z = conj z :=
   rfl
-#align complex.conj_lie_apply Complex.conjLie_apply
+#align complex.conj_lie_apply Complex.conjLIE_apply
 -/
 
-#print Complex.conjLie_symm /-
+#print Complex.conjLIE_symm /-
 @[simp]
-theorem conjLie_symm : conjLie.symm = conjLie :=
+theorem conjLIE_symm : conjLIE.symm = conjLIE :=
   rfl
-#align complex.conj_lie_symm Complex.conjLie_symm
+#align complex.conj_lie_symm Complex.conjLIE_symm
 -/
 
 #print Complex.isometry_conj /-
 theorem isometry_conj : Isometry (conj : ℂ → ℂ) :=
-  conjLie.Isometry
+  conjLIE.Isometry
 #align complex.isometry_conj Complex.isometry_conj
 -/
 
@@ -456,7 +456,7 @@ theorem nndist_conj_comm (z w : ℂ) : nndist (conj z) w = nndist z (conj w) :=
 -/
 
 instance : ContinuousStar ℂ :=
-  ⟨conjLie.Continuous⟩
+  ⟨conjLIE.Continuous⟩
 
 #print Complex.continuous_conj /-
 @[continuity]
@@ -477,44 +477,44 @@ theorem ringHom_eq_id_or_conj_of_continuous {f : ℂ →+* ℂ} (hf : Continuous
 #align complex.ring_hom_eq_id_or_conj_of_continuous Complex.ringHom_eq_id_or_conj_of_continuous
 -/
 
-#print Complex.conjCle /-
+#print Complex.conjCLE /-
 /-- Continuous linear equiv version of the conj function, from `ℂ` to `ℂ`. -/
-def conjCle : ℂ ≃L[ℝ] ℂ :=
-  conjLie
-#align complex.conj_cle Complex.conjCle
+def conjCLE : ℂ ≃L[ℝ] ℂ :=
+  conjLIE
+#align complex.conj_cle Complex.conjCLE
 -/
 
-#print Complex.conjCle_coe /-
+#print Complex.conjCLE_coe /-
 @[simp]
-theorem conjCle_coe : conjCle.toLinearEquiv = conjAe.toLinearEquiv :=
+theorem conjCLE_coe : conjCLE.toLinearEquiv = conjAe.toLinearEquiv :=
   rfl
-#align complex.conj_cle_coe Complex.conjCle_coe
+#align complex.conj_cle_coe Complex.conjCLE_coe
 -/
 
-#print Complex.conjCle_apply /-
+#print Complex.conjCLE_apply /-
 @[simp]
-theorem conjCle_apply (z : ℂ) : conjCle z = conj z :=
+theorem conjCLE_apply (z : ℂ) : conjCLE z = conj z :=
   rfl
-#align complex.conj_cle_apply Complex.conjCle_apply
+#align complex.conj_cle_apply Complex.conjCLE_apply
 -/
 
-#print Complex.ofRealLi /-
+#print Complex.ofRealLI /-
 /-- Linear isometry version of the canonical embedding of `ℝ` in `ℂ`. -/
-def ofRealLi : ℝ →ₗᵢ[ℝ] ℂ :=
+def ofRealLI : ℝ →ₗᵢ[ℝ] ℂ :=
   ⟨ofRealAm.toLinearMap, norm_real⟩
-#align complex.of_real_li Complex.ofRealLi
+#align complex.of_real_li Complex.ofRealLI
 -/
 
 #print Complex.isometry_ofReal /-
 theorem isometry_ofReal : Isometry (coe : ℝ → ℂ) :=
-  ofRealLi.Isometry
+  ofRealLI.Isometry
 #align complex.isometry_of_real Complex.isometry_ofReal
 -/
 
 #print Complex.continuous_ofReal /-
 @[continuity]
 theorem continuous_ofReal : Continuous (coe : ℝ → ℂ) :=
-  ofRealLi.Continuous
+  ofRealLI.Continuous
 #align complex.continuous_of_real Complex.continuous_ofReal
 -/
 
@@ -529,25 +529,25 @@ theorem ringHom_eq_ofReal_of_continuous {f : ℝ →+* ℂ} (h : Continuous f) :
 #align complex.ring_hom_eq_of_real_of_continuous Complex.ringHom_eq_ofReal_of_continuous
 -/
 
-#print Complex.ofRealClm /-
+#print Complex.ofRealCLM /-
 /-- Continuous linear map version of the canonical embedding of `ℝ` in `ℂ`. -/
-def ofRealClm : ℝ →L[ℝ] ℂ :=
-  ofRealLi.toContinuousLinearMap
-#align complex.of_real_clm Complex.ofRealClm
+def ofRealCLM : ℝ →L[ℝ] ℂ :=
+  ofRealLI.toContinuousLinearMap
+#align complex.of_real_clm Complex.ofRealCLM
 -/
 
-#print Complex.ofRealClm_coe /-
+#print Complex.ofRealCLM_coe /-
 @[simp]
-theorem ofRealClm_coe : (ofRealClm : ℝ →ₗ[ℝ] ℂ) = ofRealAm.toLinearMap :=
+theorem ofRealCLM_coe : (ofRealCLM : ℝ →ₗ[ℝ] ℂ) = ofRealAm.toLinearMap :=
   rfl
-#align complex.of_real_clm_coe Complex.ofRealClm_coe
+#align complex.of_real_clm_coe Complex.ofRealCLM_coe
 -/
 
-#print Complex.ofRealClm_apply /-
+#print Complex.ofRealCLM_apply /-
 @[simp]
-theorem ofRealClm_apply (x : ℝ) : ofRealClm x = x :=
+theorem ofRealCLM_apply (x : ℝ) : ofRealCLM x = x :=
   rfl
-#align complex.of_real_clm_apply Complex.ofRealClm_apply
+#align complex.of_real_clm_apply Complex.ofRealCLM_apply
 -/
 
 noncomputable instance : IsROrC ℂ
@@ -649,13 +649,13 @@ variable {α : Type _} (𝕜 : Type _) [IsROrC 𝕜]
 #print IsROrC.hasSum_conj /-
 @[simp]
 theorem hasSum_conj {f : α → 𝕜} {x : 𝕜} : HasSum (fun x => conj (f x)) x ↔ HasSum f (conj x) :=
-  conjCle.HasSum
+  conjCLE.HasSum
 #align is_R_or_C.has_sum_conj IsROrC.hasSum_conj
 -/
 
 #print IsROrC.hasSum_conj' /-
 theorem hasSum_conj' {f : α → 𝕜} {x : 𝕜} : HasSum (fun x => conj (f x)) (conj x) ↔ HasSum f x :=
-  conjCle.hasSum'
+  conjCLE.hasSum'
 #align is_R_or_C.has_sum_conj' IsROrC.hasSum_conj'
 -/
 
@@ -679,16 +679,16 @@ variable (𝕜)
 #print IsROrC.hasSum_ofReal /-
 @[simp, norm_cast]
 theorem hasSum_ofReal {f : α → ℝ} {x : ℝ} : HasSum (fun x => (f x : 𝕜)) x ↔ HasSum f x :=
-  ⟨fun h => by simpa only [IsROrC.reClm_apply, IsROrC.ofReal_re] using re_clm.has_sum h,
-    ofRealClm.HasSum⟩
+  ⟨fun h => by simpa only [IsROrC.reCLM_apply, IsROrC.ofReal_re] using re_clm.has_sum h,
+    ofRealCLM.HasSum⟩
 #align is_R_or_C.has_sum_of_real IsROrC.hasSum_ofReal
 -/
 
 #print IsROrC.summable_ofReal /-
 @[simp, norm_cast]
 theorem summable_ofReal {f : α → ℝ} : (Summable fun x => (f x : 𝕜)) ↔ Summable f :=
-  ⟨fun h => by simpa only [IsROrC.reClm_apply, IsROrC.ofReal_re] using re_clm.summable h,
-    ofRealClm.Summable⟩
+  ⟨fun h => by simpa only [IsROrC.reCLM_apply, IsROrC.ofReal_re] using re_clm.summable h,
+    ofRealCLM.Summable⟩
 #align is_R_or_C.summable_of_real IsROrC.summable_ofReal
 -/
 
@@ -706,25 +706,25 @@ theorem ofReal_tsum (f : α → ℝ) : (↑(∑' a, f a) : 𝕜) = ∑' a, f a :
 
 #print IsROrC.hasSum_re /-
 theorem hasSum_re {f : α → 𝕜} {x : 𝕜} (h : HasSum f x) : HasSum (fun x => re (f x)) (re x) :=
-  reClm.HasSum h
+  reCLM.HasSum h
 #align is_R_or_C.has_sum_re IsROrC.hasSum_re
 -/
 
 #print IsROrC.hasSum_im /-
 theorem hasSum_im {f : α → 𝕜} {x : 𝕜} (h : HasSum f x) : HasSum (fun x => im (f x)) (im x) :=
-  imClm.HasSum h
+  imCLM.HasSum h
 #align is_R_or_C.has_sum_im IsROrC.hasSum_im
 -/
 
 #print IsROrC.re_tsum /-
 theorem re_tsum {f : α → 𝕜} (h : Summable f) : re (∑' a, f a) = ∑' a, re (f a) :=
-  reClm.map_tsum h
+  reCLM.map_tsum h
 #align is_R_or_C.re_tsum IsROrC.re_tsum
 -/
 
 #print IsROrC.im_tsum /-
 theorem im_tsum {f : α → 𝕜} (h : Summable f) : im (∑' a, f a) = ∑' a, im (f a) :=
-  imClm.map_tsum h
+  imCLM.map_tsum h
 #align is_R_or_C.im_tsum IsROrC.im_tsum
 -/
 

Mathbin/Analysis/Complex/Conformal.lean

@@ -43,8 +43,8 @@ open Complex ContinuousLinearMap
 open scoped ComplexConjugate
 
 #print isConformalMap_conj /-
-theorem isConformalMap_conj : IsConformalMap (conjLie : ℂ →L[ℝ] ℂ) :=
-  conjLie.toLinearIsometry.IsConformalMap
+theorem isConformalMap_conj : IsConformalMap (conjLIE : ℂ →L[ℝ] ℂ) :=
+  conjLIE.toLinearIsometry.IsConformalMap
 #align is_conformal_map_conj isConformalMap_conj
 -/
 
@@ -76,7 +76,7 @@ theorem isConformalMap_complex_linear {map : ℂ →L[ℂ] E} (nonzero : map ≠
 
 #print isConformalMap_complex_linear_conj /-
 theorem isConformalMap_complex_linear_conj {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) :
-    IsConformalMap ((map.restrictScalars ℝ).comp (conjCle : ℂ →L[ℝ] ℂ)) :=
+    IsConformalMap ((map.restrictScalars ℝ).comp (conjCLE : ℂ →L[ℝ] ℂ)) :=
   (isConformalMap_complex_linear nonzero).comp isConformalMap_conj
 #align is_conformal_map_complex_linear_conj isConformalMap_complex_linear_conj
 -/
@@ -92,7 +92,7 @@ variable {f : ℂ → ℂ} {z : ℂ} {g : ℂ →L[ℝ] ℂ}
 #print IsConformalMap.is_complex_or_conj_linear /-
 theorem IsConformalMap.is_complex_or_conj_linear (h : IsConformalMap g) :
     (∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g) ∨
-      ∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g ∘L ↑conjCle :=
+      ∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g ∘L ↑conjCLE :=
   by
   rcases h with ⟨c, hc, li, rfl⟩
   obtain ⟨li, rfl⟩ : ∃ li' : ℂ ≃ₗᵢ[ℝ] ℂ, li'.toLinearIsometry = li
@@ -118,7 +118,7 @@ theorem IsConformalMap.is_complex_or_conj_linear (h : IsConformalMap g) :
 theorem isConformalMap_iff_is_complex_or_conj_linear :
     IsConformalMap g ↔
       ((∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g) ∨
-          ∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g ∘L ↑conjCle) ∧
+          ∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g ∘L ↑conjCLE) ∧
         g ≠ 0 :=
   by
   constructor