chore: rename theorems to comply with mathlib standards (#36026)

On a suggestion of `urkud`, rename two theorems, in order to comply with mathlib standards.

Author: kebekus

Mathlib/Analysis/Complex/Harmonic/Analytic.lean

@@ -71,7 +71,8 @@ set_option backward.isDefEq.respectTransparency false in
 If a function `f : ℂ → ℝ` is harmonic on an open ball, then `f` is the real part of a function
 `F : ℂ → ℂ` that is holomorphic on the ball.
 -/
-theorem harmonic_is_realOfHolomorphic {z : ℂ} {R : ℝ} (hf : HarmonicOnNhd f (ball z R)) :
+theorem InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq {z : ℂ} {R : ℝ}
+    (hf : HarmonicOnNhd f (ball z R)) :
     ∃ F : ℂ → ℂ, (AnalyticOnNhd ℂ F (ball z R)) ∧ ((ball z R).EqOn (fun z ↦ (F z).re) f) := by
   by_cases hR : R ≤ 0
   · simp [ball_eq_empty.2 hR]
@@ -102,11 +103,15 @@ theorem harmonic_is_realOfHolomorphic {z : ℂ} {R : ℝ} (hf : HarmonicOnNhd f
     simp [HasDerivAt.deriv (hF.2 y hy), g]
   all_goals simp_all
 
+@[deprecated (since := "2026-03-03")]
+alias harmonic_is_realOfHolomorphic :=
+  InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq
+
 set_option backward.isDefEq.respectTransparency false in
 /--
 If a function `f : ℂ → ℝ` is harmonic, then `f` is the real part of a holomorphic function.
 -/
-theorem InnerProductSpace.harmonic_is_realOfHolomorphic_univ {f : ℂ → ℝ}
+theorem InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq {f : ℂ → ℝ}
     (hf : HarmonicOnNhd f univ) :
     ∃ F : ℂ → ℂ, (AnalyticOnNhd ℂ F univ) ∧ ((fun z ↦ (F z).re) = f) := by
   let g := ofRealCLM ∘ (fderiv ℝ f · 1) - I • ofRealCLM ∘ (fderiv ℝ f · I)
@@ -132,13 +137,18 @@ theorem InnerProductSpace.harmonic_is_realOfHolomorphic_univ {f : ℂ → ℝ}
     · simp
   all_goals simp_all
 
+@[deprecated (since := "2026-03-03")]
+alias InnerProductSpace.harmonic_is_realOfHolomorphic_univ :=
+  InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq
+
 set_option backward.isDefEq.respectTransparency false in
 /-
 Harmonic functions are real analytic.
 TODO: Prove this for harmonic functions on an arbitrary f.d. inner product space (not just on `ℂ`).
 -/
 theorem HarmonicAt.analyticAt (hf : HarmonicAt f x) : AnalyticAt ℝ f x := by
   obtain ⟨ε, h₁ε, h₂ε⟩ := isOpen_iff.1 (isOpen_setOf_harmonicAt (f := f)) x hf
-  obtain ⟨F, h₁F, h₂F⟩ := harmonic_is_realOfHolomorphic (fun _ hy ↦ h₂ε hy)
+  obtain ⟨F, h₁F, h₂F⟩ := InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq
+    (fun _ hy ↦ h₂ε hy)
   rw [analyticAt_congr (Filter.eventually_of_mem (ball_mem_nhds x h₁ε) (fun y hy ↦ h₂F.symm hy))]
   exact (reCLM.analyticAt (F x)).comp (h₁F x (mem_ball_self h₁ε)).restrictScalars

Mathlib/Analysis/Complex/Harmonic/Liouville.lean

@@ -29,7 +29,7 @@ theorem InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant (f : ℂ
     (h_harm : HarmonicOnNhd f univ) (h_bound : Bornology.IsBounded (range f)) :
     ∀ z w, f z = f w := by
   -- By assumption, there exists a holomorphic function $f$ such that $\Re(f) = u$.
-  obtain ⟨F, hF_diff, hF_re⟩ := harmonic_is_realOfHolomorphic_univ h_harm
+  obtain ⟨F, hF_diff, hF_re⟩ := h_harm.exists_analyticOnNhd_univ_re_eq
   -- Since $g(z)$ is bounded, by Liouville's theorem, $g(z)$ is constant.
   suffices ∀ z w, Complex.exp (F z) = Complex.exp (F w) by grind
   apply Differentiable.apply_eq_apply_of_bounded

Mathlib/Analysis/Complex/Harmonic/MeanValue.lean

@@ -29,7 +29,7 @@ theorem HarmonicOnNhd.circleAverage_eq (hf : HarmonicOnNhd f (closedBall c |R|))
   obtain ⟨e, h₁e, h₂e⟩ := (isCompact_closedBall c |R|).exists_thickening_subset_open
     (isOpen_setOf_harmonicAt f) hf
   rw [thickening_closedBall h₁e (abs_nonneg R)] at h₂e
-  obtain ⟨F, h₁F, h₂F⟩ := harmonic_is_realOfHolomorphic h₂e
+  obtain ⟨F, h₁F, h₂F⟩ := InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq h₂e
   have h₃F : DifferentiableOn ℂ F (closure (ball c |R|)) := by
     intro x hx
     apply (h₁F x _).differentiableWithinAt