Merge master into nightly-testing

Author: leanprover-community-mathlib4-bot

Mathlib.lean

@@ -1472,6 +1472,7 @@ import Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
 import Mathlib.Analysis.Complex.UpperHalfPlane.Metric
 import Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
 import Mathlib.Analysis.Complex.UpperHalfPlane.Topology
+import Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
 import Mathlib.Analysis.Complex.ValueDistribution.CountingFunction
 import Mathlib.Analysis.Complex.ValueDistribution.ProximityFunction
 import Mathlib.Analysis.ConstantSpeed

Mathlib/Analysis/Analytic/IteratedFDeriv.lean

@@ -247,6 +247,12 @@ theorem AnalyticOn.iteratedFDerivWithin_comp_perm
   conv_rhs => rw [← Equiv.sum_comp (Equiv.mulLeft σ)]
   simp only [coe_mulLeft, Perm.coe_mul, Function.comp_apply]
 
+theorem AnalyticOn.domDomCongr_iteratedFDerivWithin
+    (h : AnalyticOn 𝕜 f s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (σ : Perm (Fin n)) :
+    (iteratedFDerivWithin 𝕜 n f s x).domDomCongr σ = iteratedFDerivWithin 𝕜 n f s x := by
+  ext
+  exact h.iteratedFDerivWithin_comp_perm hs hx _ _
+
 /-- The `n`-th iterated derivative of an analytic function on a set is symmetric. -/
 theorem ContDiffWithinAt.iteratedFDerivWithin_comp_perm
     (h : ContDiffWithinAt 𝕜 ω f s x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (v : Fin n → E)
@@ -259,16 +265,33 @@ theorem ContDiffWithinAt.iteratedFDerivWithin_comp_perm
   rw [← this]
   exact AnalyticOn.iteratedFDerivWithin_comp_perm hu.analyticOn (hs.inter u_open) ⟨hx, xu⟩ _ _
 
+theorem ContDiffWithinAt.domDomCongr_iteratedFDerivWithin
+    (h : ContDiffWithinAt 𝕜 ω f s x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ}
+    (σ : Perm (Fin n)) :
+    (iteratedFDerivWithin 𝕜 n f s x).domDomCongr σ = iteratedFDerivWithin 𝕜 n f s x := by
+  ext
+  exact h.iteratedFDerivWithin_comp_perm hs hx _ _
+
 /-- The `n`-th iterated derivative of an analytic function is symmetric. -/
 theorem AnalyticOn.iteratedFDeriv_comp_perm
     (h : AnalyticOn 𝕜 f univ) {n : ℕ} (v : Fin n → E) (σ : Perm (Fin n)) :
     iteratedFDeriv 𝕜 n f x (v ∘ σ) = iteratedFDeriv 𝕜 n f x v := by
   rw [← iteratedFDerivWithin_univ]
   exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _
 
+theorem AnalyticOn.domDomCongr_iteratedFDeriv (h : AnalyticOn 𝕜 f univ) {n : ℕ} (σ : Perm (Fin n)) :
+    (iteratedFDeriv 𝕜 n f x).domDomCongr σ = iteratedFDeriv 𝕜 n f x := by
+  rw [← iteratedFDerivWithin_univ]
+  exact h.domDomCongr_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ x) _
+
 /-- The `n`-th iterated derivative of an analytic function is symmetric. -/
 theorem ContDiffAt.iteratedFDeriv_comp_perm
     (h : ContDiffAt 𝕜 ω f x) {n : ℕ} (v : Fin n → E) (σ : Perm (Fin n)) :
     iteratedFDeriv 𝕜 n f x (v ∘ σ) = iteratedFDeriv 𝕜 n f x v := by
   rw [← iteratedFDerivWithin_univ]
   exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _
+
+theorem ContDiffAt.domDomCongr_iteratedFDeriv (h : ContDiffAt 𝕜 ω f x) {n : ℕ} (σ : Perm (Fin n)) :
+    (iteratedFDeriv 𝕜 n f x).domDomCongr σ = iteratedFDeriv 𝕜 n f x := by
+  rw [← iteratedFDerivWithin_univ]
+  exact h.domDomCongr_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ x) _

Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2025 Stefan Kebekus. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
+-/
+import Mathlib.Analysis.Complex.ValueDistribution.CountingFunction
+import Mathlib.Analysis.Complex.ValueDistribution.ProximityFunction
+
+/-!
+# The Characteristic Function of Value Distribution Theory
+
+This file defines the "characteristic function" attached to a meromorphic function defined on the
+complex plane.  Also known as "Nevanlinna Height", this is one of the three main functions used in
+Value Distribution Theory.
+
+The characteristic function plays a role analogous to the height function in number theory: both
+measure the "complexity" of objects. For rational functions, the characteristic function grows like
+the degree times the logarithm, much like the logarithmic height in number theory reflects the
+degree of an algebraic number.
+
+See Section~VI.2 of [Lang, *Introduction to Complex Hyperbolic Spaces*][MR886677] or Section~1.1 of
+[Noguchi-Winkelmann, *Nevanlinna Theory in Several Complex Variables and Diophantine
+Approximation*][MR3156076] for a detailed discussion.
+
+### TODO
+
+- Characterize rational functions in terms of the growth rate of their characteristic function, as
+  discussed in Theorem 2.6 on p. 170 of [Lang, *Introduction to Complex Hyperbolic
+  Spaces*][MR886677].
+-/
+
+open Metric Real Set
+
+namespace ValueDistribution
+
+variable
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
+  {f : ℂ → E} {a : WithTop E}
+
+variable (f a) in
+/--
+The Characteristic Function of Value Distribution Theory
+
+If `f : ℂ → E` is meromorphic and `a : WithTop E` is any value, the characteristic function of `f`
+is defined as the sum of two terms: the proximity function, which quantifies how close `f` gets to
+`a` on the circle `∣z∣ = r`, and the counting function, which counts the number times that `f`
+attains the value `a` inside the disk `∣z∣ ≤ r`, weighted by multiplicity.
+-/
+noncomputable def characteristic : ℝ → ℝ := proximity f a + logCounting f a
+
+/-!
+## Elementary Properties
+-/
+
+/--
+The difference between the characteristic functions of `f` and `f - const` simplifies to the
+difference between the proximity functions.
+-/
+@[simp]
+lemma characteristic_sub_characteristic_eq_proximity_sub_proximity (h : MeromorphicOn f ⊤)
+    (a₀ : E) :
+    characteristic f ⊤ - characteristic (f · - a₀) ⊤ = proximity f ⊤ - proximity (f · - a₀) ⊤ := by
+  rw [(by rfl : (f · - a₀) = f - fun _ ↦ a₀)]
+  simp [characteristic, logCounting_sub_const h]
+
+end ValueDistribution

Mathlib/GroupTheory/Perm/Fin.lean

@@ -256,6 +256,29 @@ theorem cycleRange_symm_succ {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
     i.cycleRange.symm j.succ = i.succAbove j :=
   i.cycleRange.injective (by simp)
 
+@[simp]
+theorem insertNth_apply_cycleRange_symm {n : ℕ} {α : Type*} (p : Fin (n + 1)) (a : α)
+    (x : Fin n → α) (j : Fin (n + 1)) :
+    (p.insertNth a x : _ → α) (p.cycleRange.symm j) = (Fin.cons a x : _ → α) j := by
+  cases j using Fin.cases <;> simp
+
+@[simp]
+theorem insertNth_comp_cycleRange_symm {n : ℕ} {α : Type*} (p : Fin (n + 1)) (a : α)
+    (x : Fin n → α) : (p.insertNth a x ∘ p.cycleRange.symm : _ → α) = Fin.cons a x := by
+  ext j
+  simp
+
+@[simp]
+theorem cons_apply_cycleRange {n : ℕ} {α : Type*} (a : α) (x : Fin n → α)
+    (p : Fin (n + 1)) (j : Fin (n + 1)) :
+    (Fin.cons a x : _ → α) (p.cycleRange j) = (p.insertNth a x : _ → α) j := by
+  rw [← insertNth_apply_cycleRange_symm, Equiv.symm_apply_apply]
+
+@[simp]
+theorem cons_comp_cycleRange {n : ℕ} {α : Type*} (a : α) (x : Fin n → α) (p : Fin (n + 1)) :
+    (Fin.cons a x : _ → α) ∘ p.cycleRange = p.insertNth a x := by
+  ext; simp
+
 theorem isCycle_cycleRange {n : ℕ} [NeZero n] {i : Fin n} (h0 : i ≠ 0) :
     IsCycle (cycleRange i) := by
   obtain ⟨i, hi⟩ := i