Skip to content

Commit ac48e6a

Browse files
kebekuskebekus
committed
feat: behaviour of Nevanlinna functions under multiplication (#30494)
Establish the behavior of Nevanlinna functions under multiplication. This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. The formula established here is part of a larger package discussing the behavior of the Nenvanlinna height under algebraic manipulations of the functions.
1 parent ede1a9b commit ac48e6a

File tree

5 files changed

+246
-1
lines changed

5 files changed

+246
-1
lines changed

‎Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,4 +62,56 @@ lemma characteristic_sub_characteristic_eq_proximity_sub_proximity (h : Meromorp
6262
characteristic f ⊤ - characteristic (f · - a₀) ⊤ = proximity f ⊤ - proximity (f · - a₀) ⊤ := by
6363
simp [← Pi.sub_def, characteristic, logCounting_sub_const h]
6464

65+
/-!
66+
## Behaviour under Arithmetic Operations
67+
-/
68+
69+
/--
70+
For `1 ≤ r`, the characteristic function of `f * g` at zero is less than or
71+
equal to the sum of the characteristic functions of `f` and `g`, respectively.
72+
-/
73+
theorem characteristic_zero_mul_le {f₁ f₂ : ℂ → ℂ} {r : ℝ} (hr : 1 ≤ r)
74+
(h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
75+
(h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
76+
characteristic (f₁ * f₂) 0 r ≤ (characteristic f₁ 0 + characteristic f₂ 0) r := by
77+
simp only [characteristic, Pi.add_apply]
78+
rw [add_add_add_comm]
79+
apply add_le_add (proximity_zero_mul_le h₁f₁ h₁f₂ r)
80+
(logCounting_zero_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂)
81+
82+
/--
83+
Asymptotically, the characteristic function of `f * g` at zero is less than or
84+
equal to the sum of the characteristic functions of `f` and `g`, respectively.
85+
-/
86+
theorem characteristic_zero_mul_eventually_le {f₁ f₂ : ℂ → ℂ}
87+
(h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
88+
(h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
89+
characteristic (f₁ * f₂) 0 ≤ᶠ[Filter.atTop] characteristic f₁ 0 + characteristic f₂ 0 := by
90+
filter_upwards [Filter.eventually_ge_atTop 1]
91+
exact fun _ hr ↦ characteristic_zero_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
92+
93+
/--
94+
For `1 ≤ r`, the characteristic function of `f * g` at `⊤` is less than or equal
95+
to the sum of the characteristic functions of `f` and `g`, respectively.
96+
-/
97+
theorem characteristic_top_mul_le {f₁ f₂ : ℂ → ℂ} {r : ℝ} (hr : 1 ≤ r)
98+
(h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
99+
(h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
100+
characteristic (f₁ * f₂) ⊤ r ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) r := by
101+
simp only [characteristic, Pi.add_apply]
102+
rw [add_add_add_comm]
103+
apply add_le_add (proximity_top_mul_le h₁f₁ h₁f₂ r)
104+
(logCounting_top_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂)
105+
106+
/--
107+
Asymptotically, the characteristic function of `f * g` at `⊤` is less than or
108+
equal to the sum of the characteristic functions of `f` and `g`, respectively.
109+
-/
110+
theorem characteristic_top_mul_eventually_le {f₁ f₂ : ℂ → ℂ}
111+
(h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
112+
(h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
113+
characteristic (f₁ * f₂) ⊤ ≤ᶠ[Filter.atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ := by
114+
filter_upwards [Filter.eventually_ge_atTop 1]
115+
exact fun _ hr ↦ characteristic_top_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
116+
65117
end ValueDistribution

‎Mathlib/Analysis/Complex/ValueDistribution/CountingFunction.lean‎

Lines changed: 112 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,15 +47,24 @@ open MeromorphicOn Metric Real Set
4747

4848
namespace Function.locallyFinsuppWithin
4949

50+
variable {E : Type*} [NormedAddCommGroup E]
51+
5052
/--
5153
Shorthand notation for the restriction of a function with locally finite support within `Set.univ`
5254
to the closed unit ball of radius `r`.
5355
-/
54-
noncomputable def toClosedBall {E : Type*} [NormedAddCommGroup E] (r : ℝ) :
56+
noncomputable def toClosedBall (r : ℝ) :
5557
locallyFinsuppWithin (univ : Set E) ℤ →+ locallyFinsuppWithin (closedBall (0 : E) |r|) ℤ := by
5658
apply restrictMonoidHom
5759
tauto
5860

61+
@[simp]
62+
lemma toClosedBall_eval_within {r : ℝ} {z : E} (f : locallyFinsuppWithin (univ : Set E) ℤ)
63+
(ha : z ∈ closedBall 0 |r|) :
64+
toClosedBall r f z = f z := by
65+
unfold toClosedBall
66+
simp_all [restrict_apply]
67+
5968
/-!
6069
## The Logarithmic Counting Function of a Function with Locally Finite Support
6170
-/
@@ -104,6 +113,42 @@ Evaluation of the logarithmic counting function at zero yields zero.
104113
logCounting D 0 = 0 := by
105114
simp [logCounting]
106115

116+
/--
117+
For `1 ≤ r`, the counting function is non-negative.
118+
-/
119+
theorem logCounting_nonneg {E : Type*} [NormedAddCommGroup E] [ProperSpace E]
120+
{f : locallyFinsuppWithin (univ : Set E) ℤ} {r : ℝ} (h : 0 ≤ f) (hr : 1 ≤ r) :
121+
0 ≤ logCounting f r := by
122+
have h₃r : 0 < r := by linarith
123+
suffices ∀ z, 0 ≤ (((toClosedBall r) f) z) * log (r * ‖z‖⁻¹) from
124+
add_nonneg (finsum_nonneg this) <| mul_nonneg (by simpa using h 0) (log_nonneg hr)
125+
intro a
126+
by_cases h₁a : a = 0
127+
· simp_all
128+
by_cases h₂a : a ∈ closedBall 0 |r|
129+
· refine mul_nonneg ?_ <| log_nonneg ?_
130+
· simpa [h₂a] using h a
131+
· simpa [mul_comm r, one_le_inv_mul₀ (norm_pos_iff.mpr h₁a), abs_of_pos h₃r] using h₂a
132+
· simp [apply_eq_zero_of_notMem ((toClosedBall r) _) h₂a]
133+
134+
/--
135+
For `1 ≤ r`, the counting function respects the `≤` relation.
136+
-/
137+
theorem logCounting_le {E : Type*} [NormedAddCommGroup E] [ProperSpace E]
138+
{f₁ f₂ : locallyFinsuppWithin (univ : Set E) ℤ} {r : ℝ} (h : f₁ ≤ f₂) (hr : 1 ≤ r) :
139+
logCounting f₁ r ≤ logCounting f₂ r := by
140+
rw [← sub_nonneg] at h ⊢
141+
simpa using logCounting_nonneg h hr
142+
143+
/--
144+
The counting function respects the `≤` relation asymptotically.
145+
-/
146+
theorem logCounting_eventually_le {E : Type*} [NormedAddCommGroup E] [ProperSpace E]
147+
{f₁ f₂ : locallyFinsuppWithin (univ : Set E) ℤ} (h : f₁ ≤ f₂) :
148+
logCounting f₁ ≤ᶠ[Filter.atTop] logCounting f₂ := by
149+
filter_upwards [Filter.eventually_ge_atTop 1]
150+
exact fun _ hr ↦ logCounting_le h hr
151+
107152
end Function.locallyFinsuppWithin
108153

109154
/-!
@@ -212,4 +257,70 @@ function counting poles.
212257
logCounting (f - fun _ ↦ a₀) ⊤ = logCounting f ⊤ := by
213258
simpa [sub_eq_add_neg] using logCounting_add_const hf
214259

260+
/-!
261+
## Behaviour under Arithmetic Operations
262+
-/
263+
264+
/--
265+
For `1 ≤ r`, the counting function counting zeros of `f * g` is less than or equal to the sum of the
266+
counting functions counting zeros of `f` and `g`, respectively.
267+
268+
Note: The statement proven here is found at the top of page 169 of [Lang: Introduction to Complex
269+
Hyperbolic Spaces](https://link.springer.com/book/10.1007/978-1-4757-1945-1) where it is written as
270+
an inequality between functions. This could be interpreted as claiming that the inequality holds for
271+
ALL values of `r`, which is not true. For a counterexample, take `f₁ : z → z` and `f₂ : z → z⁻¹`.
272+
Then,
273+
274+
- `logCounting f₁ 0 = log`
275+
- `logCounting f₂ 0 = 0`
276+
- `logCounting (f₁ * f₂) 0 = 0`
277+
278+
But `log r` is negative for small `r`.
279+
-/
280+
theorem logCounting_zero_mul_le {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 ≤ r)
281+
(h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
282+
(h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
283+
logCounting (f₁ * f₂) 0 r ≤ (logCounting f₁ 0 + logCounting f₂ 0) r := by
284+
simp only [logCounting, WithTop.zero_ne_top, reduceDIte, WithTop.untop₀_zero, sub_zero]
285+
rw [divisor_mul h₁f₁ h₁f₂ (fun z _ ↦ h₂f₁ z) (fun z _ ↦ h₂f₂ z),
286+
← Function.locallyFinsuppWithin.logCounting.map_add]
287+
apply Function.locallyFinsuppWithin.logCounting_le _ hr
288+
apply Function.locallyFinsuppWithin.posPart_add
289+
290+
/--
291+
Asymptotically, the counting function counting zeros of `f * g` is less than or equal to the sum of
292+
the counting functions counting zeros of `f` and `g`, respectively.
293+
-/
294+
theorem logCounting_zero_mul_eventually_le {f₁ f₂ : 𝕜 → 𝕜}
295+
(h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
296+
(h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
297+
logCounting (f₁ * f₂) 0 ≤ᶠ[Filter.atTop] logCounting f₁ 0 + logCounting f₂ 0 := by
298+
filter_upwards [Filter.eventually_ge_atTop 1]
299+
exact fun _ hr ↦ logCounting_zero_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
300+
301+
/--
302+
For `1 ≤ r`, the counting function counting poles of `f * g` is less than or equal to the sum of the
303+
counting functions counting poles of `f` and `g`, respectively.
304+
-/
305+
theorem logCounting_top_mul_le {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ} (hr : 1 ≤ r)
306+
(h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
307+
(h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
308+
logCounting (f₁ * f₂) ⊤ r ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) r := by
309+
simp only [logCounting, reduceDIte]
310+
rw [divisor_mul h₁f₁ h₁f₂ (fun z _ ↦ h₂f₁ z) (fun z _ ↦ h₂f₂ z),
311+
← Function.locallyFinsuppWithin.logCounting.map_add]
312+
apply Function.locallyFinsuppWithin.logCounting_le _ hr
313+
apply Function.locallyFinsuppWithin.negPart_add
314+
315+
/--
316+
Asymptotically, the counting function counting zeros of `f * g` is less than or equal to the sum of
317+
the counting functions counting zeros of `f` and `g`, respectively.
318+
-/
319+
theorem logCounting_top_mul_eventually_le {f₁ f₂ : 𝕜 → 𝕜}
320+
(h₁f₁ : MeromorphicOn f₁ Set.univ) (h₂f₁ : ∀ z, meromorphicOrderAt f₁ z ≠ ⊤)
321+
(h₁f₂ : MeromorphicOn f₂ Set.univ) (h₂f₂ : ∀ z, meromorphicOrderAt f₂ z ≠ ⊤) :
322+
logCounting (f₁ * f₂) ⊤ ≤ᶠ[Filter.atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤ := by
323+
filter_upwards [Filter.eventually_ge_atTop 1]
324+
exact fun _ hr ↦ logCounting_top_mul_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
325+
215326
end ValueDistribution

‎Mathlib/Analysis/Complex/ValueDistribution/ProximityFunction.lean‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,4 +106,48 @@ theorem proximity_sub_proximity_inv_eq_circleAverage {f : ℂ → ℂ} (h₁f :
106106
· simp_rw [← norm_inv]
107107
apply circleIntegrable_posLog_norm_meromorphicOn (h₁f.inv.mono_set (by tauto))
108108

109+
/-!
110+
## Behaviour under Arithmetic Operations
111+
-/
112+
113+
/--
114+
The proximity function `f * g` at `⊤` is less than or equal to the sum of the
115+
proximity functions of `f` and `g`, respectively.
116+
-/
117+
theorem proximity_top_mul_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : MeromorphicOn f₁ Set.univ)
118+
(h₁f₂ : MeromorphicOn f₂ Set.univ) :
119+
proximity (f₁ * f₂) ⊤ ≤ (proximity f₁ ⊤) + (proximity f₂ ⊤) := by
120+
calc proximity (f₁ * f₂) ⊤
121+
_ = circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 := by
122+
simp [proximity]
123+
_ ≤ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 := by
124+
intro r
125+
apply circleAverage_mono
126+
· simp_rw [← norm_mul]
127+
apply circleIntegrable_posLog_norm_meromorphicOn
128+
exact MeromorphicOn.fun_mul (fun x a ↦ h₁f₁ x trivial) fun x a ↦ h₁f₂ x trivial
129+
· apply (circleIntegrable_posLog_norm_meromorphicOn (fun x a ↦ h₁f₁ x trivial)).add
130+
(circleIntegrable_posLog_norm_meromorphicOn (fun x a ↦ h₁f₂ x trivial))
131+
· exact fun _ _ ↦ posLog_mul
132+
_ = circleAverage (log⁺ ‖f₁ ·‖) 0 + circleAverage (log⁺ ‖f₂ ·‖) 0:= by
133+
ext r
134+
apply circleAverage_add
135+
· exact circleIntegrable_posLog_norm_meromorphicOn (fun x a ↦ h₁f₁ x trivial)
136+
· exact circleIntegrable_posLog_norm_meromorphicOn (fun x a ↦ h₁f₂ x trivial)
137+
_ = (proximity f₁ ⊤) + (proximity f₂ ⊤) := rfl
138+
139+
/--
140+
The proximity function `f * g` at `0` is less than or equal to the sum of the
141+
proximity functions of `f` and `g`, respectively.
142+
-/
143+
theorem proximity_zero_mul_le {f₁ f₂ : ℂ → ℂ} (h₁f₁ : MeromorphicOn f₁ Set.univ)
144+
(h₁f₂ : MeromorphicOn f₂ Set.univ) :
145+
proximity (f₁ * f₂) 0 ≤ (proximity f₁ 0) + (proximity f₂ 0) := by
146+
calc proximity (f₁ * f₂) 0
147+
_ ≤ (proximity f₁⁻¹ ⊤) + (proximity f₂⁻¹ ⊤) := by
148+
rw [← proximity_inv, mul_inv]
149+
apply proximity_top_mul_le (MeromorphicOn.inv_iff.mpr h₁f₁) (MeromorphicOn.inv_iff.mpr h₁f₂)
150+
_ = (proximity f₁ 0) + (proximity f₂ 0) := by
151+
rw [proximity_inv, proximity_inv]
152+
109153
end ValueDistribution

‎Mathlib/MeasureTheory/Integral/CircleAverage.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,17 @@ theorem circleAverage_const_on_circle [CompleteSpace E] {a : E}
202202
## Inequalities
203203
-/
204204

205+
/--
206+
Circle averages respect the `≤` relation.
207+
-/
208+
@[gcongr]
209+
theorem circleAverage_mono {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → ℝ} (hf₁ : CircleIntegrable f₁ c R)
210+
(hf₂ : CircleIntegrable f₂ c R) (h : ∀ x ∈ Metric.sphere c |R|, f₁ x ≤ f₂ x) :
211+
circleAverage f₁ c R ≤ circleAverage f₂ c R := by
212+
apply (mul_le_mul_iff_of_pos_left (by simp [pi_pos])).2
213+
apply intervalIntegral.integral_mono_on_of_le_Ioo (le_of_lt two_pi_pos) hf₁ hf₂
214+
exact fun x _ ↦ by simp [h (circleMap c R x)]
215+
205216
/--
206217
If `f x` is smaller than `a` on for every point of the circle, then the circle average of `f` is
207218
smaller than `a`.

‎Mathlib/Topology/LocallyFinsupp.lean‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -340,6 +340,33 @@ Functions with locally finite support within `U` form an ordered commutative gro
340340
instance : IsOrderedAddMonoid (locallyFinsuppWithin U Y) where
341341
add_le_add_left := fun _ _ _ _ ↦ by simpa [le_def]
342342

343+
/--
344+
The positive part of a sum is less than or equal to the sum of the positive parts.
345+
-/
346+
theorem posPart_add (f₁ f₂ : Function.locallyFinsuppWithin U Y) :
347+
(f₁ + f₂)⁺ ≤ f₁⁺ + f₂⁺ := by
348+
repeat rw [posPart_def]
349+
intro x
350+
simp only [Function.locallyFinsuppWithin.max_apply, Function.locallyFinsuppWithin.coe_add,
351+
Pi.add_apply, Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, sup_le_iff]
352+
constructor
353+
· simp [add_le_add]
354+
· simp [add_nonneg]
355+
356+
/--
357+
The negative part of a sum is less than or equal to the sum of the negative parts.
358+
-/
359+
theorem negPart_add (f₁ f₂ : Function.locallyFinsuppWithin U Y) :
360+
(f₁ + f₂)⁻ ≤ f₁⁻ + f₂⁻ := by
361+
repeat rw [negPart_def]
362+
intro x
363+
simp only [neg_add_rev, Function.locallyFinsuppWithin.max_apply,
364+
Function.locallyFinsuppWithin.coe_add, Function.locallyFinsuppWithin.coe_neg, Pi.add_apply,
365+
Pi.neg_apply, Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, sup_le_iff]
366+
constructor
367+
· simp [add_comm, add_le_add]
368+
· simp [add_nonneg]
369+
343370
/--
344371
Taking the positive part of a function with locally finite support commutes with
345372
scalar multiplication by a natural number.

0 commit comments

Comments
 (0)