feat: generalize Liouville's theorem for harmonic functions (leanprover-community#36049)

On a suggestion of @urkud, generalize Liouville's theorem for harmonic functions, removing the restriction that the functions are real-valued. Further generalization will come in a separate PR.

Author: kebekus

Mathlib/Analysis/Complex/Harmonic/Liouville.lean

@@ -18,14 +18,15 @@ TODO: Prove this result for harmonic functions with values in vector spaces.
 
 public section
 
-open Complex Real Set
+open Bornology Complex Real Set
+
+variable
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
 
 set_option backward.isDefEq.respectTransparency false in
-/-
-**Liouville's theorem for harmonic functions on the complex plane** A real-valued, bounded harmonic
-function on the complex plane is constant.
--/
-theorem InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant (f : ℂ → ℝ)
+-- Auxiliary version of Liouville's theorem, for real-valued harmonic functions on the complex
+-- plane.
+private theorem InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant_aux (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$.
@@ -41,3 +42,19 @@ theorem InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant (f : ℂ
     norm_exp, exp_le_exp]
   rw [← hF_re] at hM
   grind
+
+set_option backward.isDefEq.respectTransparency false in
+/--
+**Liouville's theorem for harmonic functions on the complex plane** A real-valued, bounded harmonic
+function on the complex plane is constant.
+-/
+theorem InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant (f : ℂ → E)
+    (h_harm : HarmonicOnNhd f univ) (h_bound : IsBounded (range f)) :
+    ∀ z w, f z = f w := by
+  intro z w
+  obtain ⟨ℓ, h₁ℓ, h₂ℓ⟩ := exists_dual_vector'' ℝ (f z - f w)
+  rw [map_sub, RCLike.ofReal_real_eq_id, id_eq] at h₂ℓ
+  have η₁ : Bornology.IsBounded (range (ℓ ∘ f)) := by
+    simpa [range_comp] using IsBounded.image ℓ h_bound
+  rw [← sub_eq_zero, ← norm_eq_zero, ← h₂ℓ]
+  grind [bounded_harmonic_on_complex_plane_is_constant_aux (ℓ ∘ f) (h_harm.comp_CLM ℓ) η₁]

Mathlib/Analysis/Normed/Operator/Basic.lean

@@ -262,6 +262,24 @@ theorem ratio_le_opNorm : ‖f x‖ / ‖x‖ ≤ ‖f‖ :=
 theorem unit_le_opNorm : ‖x‖ ≤ 1 → ‖f x‖ ≤ ‖f‖ :=
   mul_one ‖f‖ ▸ f.le_opNorm_of_le
 
+/--
+Continuous linear maps are locally bounded. In other words, they map bounded sets to bounded sets.
+-/
+instance : LocallyBoundedMapClass (E →SL[σ₁₂] F) E F where
+  comap_cobounded_le := by
+    intro ℓ
+    rw [Bornology.comap_cobounded_le_iff]
+    intro s hs
+    obtain ⟨M, hM⟩ := hs.exists_norm_le
+    rw [isBounded_iff_forall_norm_le]
+    use ‖ℓ‖ * M
+    intro y hy
+    obtain ⟨σ, hσ⟩ := (mem_image _ _ _).1 hy
+    calc ‖y‖
+      _ ≤ ‖ℓ σ‖ := by rw [hσ.2]
+      _ ≤ ‖ℓ‖ * ‖σ‖ := ContinuousLinearMap.le_opNorm ℓ σ
+      _ ≤ ‖ℓ‖ * M := mul_le_mul (by rfl) (hM σ hσ.1) (norm_nonneg σ) (opNorm_nonneg ℓ)
+
 theorem opNorm_le_of_shell {f : E →SL[σ₁₂] F} {ε C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) {c : 𝕜}
     (hc : 1 < ‖c‖) (hf : ∀ x, ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C :=
   f.opNorm_le_bound' hC fun _ hx => SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc hf hx